theorem Th62: :: FINSEQOP:62

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