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;

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;

end;

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;.= 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

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;.= 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