Proof of grp_op_ap2_functionality_wrt_massoc