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;