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