let D be non empty set ; :: thesis: for d1, d2 being Element of D
for F being BinOp of D st F is having_a_unity & F is associative & F is having_an_inverseOp & F . (d1,d2) = the_unity_wrt F holds
( d1 = (the_inverseOp_wrt F) . d2 & (the_inverseOp_wrt F) . d1 = d2 )
let d1, d2 be Element of D; :: thesis: for F being BinOp of D st F is having_a_unity & F is associative & F is having_an_inverseOp & F . (d1,d2) = the_unity_wrt F holds
( d1 = (the_inverseOp_wrt F) . d2 & (the_inverseOp_wrt F) . d1 = d2 )
let F be BinOp of D; :: thesis: ( F is having_a_unity & F is associative & F is having_an_inverseOp & F . (d1,d2) = the_unity_wrt F implies ( d1 = (the_inverseOp_wrt F) . d2 & (the_inverseOp_wrt F) . d1 = d2 ) )
assume that
A1: F is having_a_unity and
A2: F is associative and
A3: F is having_an_inverseOp and
A4: F . (d1,d2) = the_unity_wrt F ; :: thesis: ( d1 = (the_inverseOp_wrt F) . d2 & (the_inverseOp_wrt F) . d1 = d2 )
set e = the_unity_wrt F;
set d3 = (the_inverseOp_wrt F) . d2;
F . ((F . (d1,d2)),((the_inverseOp_wrt F) . d2)) = (the_inverseOp_wrt F) . d2 by A1, A4, SETWISEO:15;
then F . (d1,(F . (d2,((the_inverseOp_wrt F) . d2)))) = (the_inverseOp_wrt F) . d2 by A2;
then F . (d1,(the_unity_wrt F)) = (the_inverseOp_wrt F) . d2 by A1, A2, A3, Th59;
hence d1 = (the_inverseOp_wrt F) . d2 by A1, SETWISEO:15; :: thesis: (the_inverseOp_wrt F) . d1 = d2
set d3 = (the_inverseOp_wrt F) . d1;
F . (((the_inverseOp_wrt F) . d1),(F . (d1,d2))) = (the_inverseOp_wrt F) . d1 by A1, A4, SETWISEO:15;
then F . ((F . (((the_inverseOp_wrt F) . d1),d1)),d2) = (the_inverseOp_wrt F) . d1 by A2;
then F . ((the_unity_wrt F),d2) = (the_inverseOp_wrt F) . d1 by A1, A2, A3, Th59;
hence (the_inverseOp_wrt F) . d1 = d2 by A1, SETWISEO:15; :: thesis: verum