let V be non empty right_complementable add-associative right_zeroed addLoopStr ; :: thesis: for w, v1, v2 being Element of V st w - v1 = w - v2 holds
v1 = v2
let w, v1, v2 be Element of V; :: thesis: ( w - v1 = w - v2 implies v1 = v2 )
assume w - v1 = w - v2 ; :: thesis: v1 = v2
then - v1 = - v2 by Th8;
hence v1 = v2 by Th18; :: thesis: verum