for D being non empty set
for d being Element of D
for F, G being BinOp of D st F is associative & F is having_a_unity & F is having_an_inverseOp & G is_distributive_wrt F holds
(G [:] ((id D),d)) . (the_unity_wrt F) = the_unity_wrt F