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