let D, C be non empty set ; :: thesis: for f, f' 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,f' = C --> (the_unity_wrt F) holds
( f = (the_inverseOp_wrt F) * f' & (the_inverseOp_wrt F) * f = f' )
let f, f' be Function of C,D; :: thesis: for F being BinOp of D st F is associative & F is having_an_inverseOp & F is having_a_unity & F .: f,f' = C --> (the_unity_wrt F) holds
( f = (the_inverseOp_wrt F) * f' & (the_inverseOp_wrt F) * f = f' )
let F be BinOp of D; :: thesis: ( F is associative & F is having_an_inverseOp & F is having_a_unity & F .: f,f' = C --> (the_unity_wrt F) implies ( f = (the_inverseOp_wrt F) * f' & (the_inverseOp_wrt F) * f = f' ) )
assume that
A1: ( F is associative & F is having_an_inverseOp & F is having_a_unity ) and
A2: F .: f,f' = C --> (the_unity_wrt F) ; :: thesis: ( f = (the_inverseOp_wrt F) * f' & (the_inverseOp_wrt F) * f = f' )
set e = the_unity_wrt F;
reconsider g = C --> (the_unity_wrt F) as Function of C,D ;
set u = the_inverseOp_wrt F;

now

let c be Element of C; :: thesis: f . c = ((the_inverseOp_wrt F) * f') . c
F . (f . c),(f' . c) = g . c by A2, FUNCOP_1:48
.= the_unity_wrt F by FUNCOP_1:13 ;
hence f . c = (the_inverseOp_wrt F) . (f' . c) by A1, Th64
.= ((the_inverseOp_wrt F) * f') . c by FUNCT_2:21 ;
:: thesis: verum

end;

hence f = (the_inverseOp_wrt F) * f' by FUNCT_2:113; :: thesis: (the_inverseOp_wrt F) * f = f'

now

let c be Element of C; :: thesis: ((the_inverseOp_wrt F) * f) . c = f' . c
F . (f . c),(f' . c) = g . c by A2, FUNCOP_1:48
.= the_unity_wrt F by FUNCOP_1:13 ;
then f' . c = (the_inverseOp_wrt F) . (f . c) by A1, Th64;
hence ((the_inverseOp_wrt F) * f) . c = f' . c by FUNCT_2:21; :: thesis: verum

end;

hence (the_inverseOp_wrt F) * f = f' by FUNCT_2:113; :: thesis: verum