Proof of connex_functionality_wrt_implies