theorem Th71: :: FINSEQOP:71

for C, D being non empty set
for f being Function of C,D
for F being BinOp of D st F is having_a_unity & F is associative & F is having_an_inverseOp holds
( F .: (f,((the_inverseOp_wrt F) * f)) = C --> (the_unity_wrt F) & F .: (((the_inverseOp_wrt F) * f),f) = C --> (the_unity_wrt F) )