Proof of permr_upto_functionality_wrt_permr_upto