let V be non empty right_complementable add-associative right_zeroed addLoopStr ; :: thesis: 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; :: thesis: ( ( w + v1 = w + v2 or v1 + w = v2 + w ) implies v1 = v2 )

A1: now :: thesis: ( v1 + w = v2 + w implies v1 = v2 )

assume A2: v1 + w = v2 + w ; :: thesis: v1 = v2
thus 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 ; :: thesis: verum

end;

now :: thesis: ( w + v1 = w + v2 implies v1 = v2 )

assume A3: w + v1 = w + v2 ; :: thesis: v1 = v2
thus 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 ; :: thesis: verum

end;

hence ( ( w + v1 = w + v2 or v1 + w = v2 + w ) implies v1 = v2 ) by A1; :: thesis: verum