for D being non empty set
for g being BinOp of D st g is having_a_unity holds
g "**" (<*> D) = the_unity_wrt g by Lm3;