let D be non empty set ; :: thesis: for d, 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 . d,d1 = F . d,d2 or F . d1,d = F . d2,d ) holds
d1 = d2
let d, 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 . d,d1 = F . d,d2 or F . d1,d = F . d2,d ) holds
d1 = d2
let F be BinOp of D; :: thesis: ( F is having_a_unity & F is associative & F is having_an_inverseOp & ( F . d,d1 = F . d,d2 or F . d1,d = F . d2,d ) implies 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 . d,d1 = F . d,d2 or F . d1,d = F . d2,d ) ; :: thesis: d1 = d2
set e = the_unity_wrt F;
set u = the_inverseOp_wrt F;

per cases ( F . d,d1 = F . d,d2 or F . d1,d = F . d2,d ) by A4;

suppose A5: F . d,d1 = F . d,d2 ; :: thesis: d1 = d2

thus d1 = F . (the_unity_wrt F),d1 by A1, SETWISEO:23
.= F . (F . ((the_inverseOp_wrt F) . d),d),d1 by A1, A2, A3, Th63
.= F . ((the_inverseOp_wrt F) . d),(F . d,d2) by A2, A5, BINOP_1:def 3
.= F . (F . ((the_inverseOp_wrt F) . d),d),d2 by A2, BINOP_1:def 3
.= F . (the_unity_wrt F),d2 by A1, A2, A3, Th63
.= d2 by A1, SETWISEO:23 ; :: thesis: verum

end;

suppose A6: F . d1,d = F . d2,d ; :: thesis: d1 = d2

thus d1 = F . d1,(the_unity_wrt F) by A1, SETWISEO:23
.= F . d1,(F . d,((the_inverseOp_wrt F) . d)) by A1, A2, A3, Th63
.= F . (F . d2,d),((the_inverseOp_wrt F) . d) by A2, A6, BINOP_1:def 3
.= F . d2,(F . d,((the_inverseOp_wrt F) . d)) by A2, BINOP_1:def 3
.= F . d2,(the_unity_wrt F) by A1, A2, A3, Th63
.= d2 by A1, SETWISEO:23 ; :: thesis: verum

end;

end;