for D being non empty set
for F being BinOp of D st F is having_a_unity & F is associative & F is commutative & F is having_an_inverseOp holds
the_inverseOp_wrt F is_distributive_wrt F