Proof of massoc_functionality_wrt_massoc