Proof of permr_functionality_wrt_permr