for D being non empty set
for d being Element of D
for F being BinOp of D st F is associative & F is having_a_unity & F is having_an_inverseOp holds
(F * ((id D),(the_inverseOp_wrt F))) . (d,(the_unity_wrt F)) = d