let V be non empty right_complementable add-associative right_zeroed addLoopStr ; for w, u, v1, v2 being Element of V st ( w + v1 = w + v2 or v1 + w = v2 + w ) holds
v1 = v2
let w, u, v1, v2 be Element of V; ( ( w + v1 = w + v2 or v1 + w = v2 + w ) implies v1 = v2 )
A1:
now ( v1 + w = v2 + w implies v1 = v2 )assume A2:
v1 + w = v2 + w
;
v1 = v2thus v1 =
v1 + (0. V)
.=
v1 + (w + (- w))
by Th5
.=
(v1 + w) + (- w)
by Def3
.=
v2 + (w + (- w))
by A2, Def3
.=
v2 + (0. V)
by Th5
.=
v2
;
verum end;
now ( w + v1 = w + v2 implies v1 = v2 )assume A3:
w + v1 = w + v2
;
v1 = v2thus v1 =
(0. V) + v1
.=
((- w) + w) + v1
by Th5
.=
(- w) + (w + v1)
by Def3
.=
((- w) + w) + v2
by A3, Def3
.=
(0. V) + v2
by Th5
.=
v2
;
verum end;
hence
( ( w + v1 = w + v2 or v1 + w = v2 + w ) implies v1 = v2 )
by A1; verum