let D be non empty set ; 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; 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; ( 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) )
; 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)
;
d1 = d2thus 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
;
verum end; suppose A6:
F . (
d1,
d)
= F . (
d2,
d)
;
d1 = d2thus 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
;
verum end;