theorem :: FINSEQOP:86

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,d) = the_unity_wrt F