Proof of mul_functionality_wrt_eq