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:15
.= F . ((F . (((the_inverseOp_wrt F) . d),d)),d1) by A1, A2, A3, Th59
.= F . (((the_inverseOp_wrt F) . d),(F . (d,d2))) by A2, A5
.= F . ((F . (((the_inverseOp_wrt F) . d),d)),d2) by A2
.= F . ((the_unity_wrt F),d2) by A1, A2, A3, Th59
.= d2 by A1, SETWISEO:15 ; :: 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:15
.= F . (d1,(F . (d,((the_inverseOp_wrt F) . d)))) by A1, A2, A3, Th59
.= F . ((F . (d2,d)),((the_inverseOp_wrt F) . d)) by A2, A6
.= F . (d2,(F . (d,((the_inverseOp_wrt F) . d)))) by A2
.= F . (d2,(the_unity_wrt F)) by A1, A2, A3, Th59
.= d2 by A1, SETWISEO:15 ; :: thesis: verum

end;

end;