Proof of mset_for_functionality_wrt_bsubmset