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:23;
then F . d1,(F . d2,((the_inverseOp_wrt F) . d2)) = (the_inverseOp_wrt F) . d2 by A2, BINOP_1:def 3;
then F . d1,(the_unity_wrt F) = (the_inverseOp_wrt F) . d2 by A1, A2, A3, Th63;
hence d1 = (the_inverseOp_wrt F) . d2 by A1, SETWISEO:23; :: 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:23;
then F . (F . ((the_inverseOp_wrt F) . d1),d1),d2 = (the_inverseOp_wrt F) . d1 by A2, BINOP_1:def 3;
then F . (the_unity_wrt F),d2 = (the_inverseOp_wrt F) . d1 by A1, A2, A3, Th63;
hence (the_inverseOp_wrt F) . d1 = d2 by A1, SETWISEO:23; :: thesis: verum