let C, D be 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 )
let f, f9 be 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 )
let F be BinOp of D; ( F is associative & F is having_an_inverseOp & F is having_a_unity & F .: (f,f9) = C --> (the_unity_wrt F) implies ( f = (the_inverseOp_wrt F) * f9 & (the_inverseOp_wrt F) * f = f9 ) )
assume that
A1:
( F is associative & F is having_an_inverseOp & F is having_a_unity )
and
A2:
F .: (f,f9) = C --> (the_unity_wrt F)
; ( f = (the_inverseOp_wrt F) * f9 & (the_inverseOp_wrt F) * f = f9 )
set u = the_inverseOp_wrt F;
set e = the_unity_wrt F;
reconsider g = C --> (the_unity_wrt F) as Function of C,D ;
hence
f = (the_inverseOp_wrt F) * f9
by FUNCT_2:63; (the_inverseOp_wrt F) * f = f9
hence
(the_inverseOp_wrt F) * f = f9
by FUNCT_2:63; verum