for D being non empty set
for d1, d2 being Element of D
for F, G being BinOp of D
for u being UnOp of D st F is having_a_unity & F is associative & F is having_an_inverseOp & u = the_inverseOp_wrt F & G is_distributive_wrt F holds
( u . (G . (d1,d2)) = G . ((u . d1),d2) & u . (G . (d1,d2)) = G . (d1,(u . d2)) )