for V being non empty right_complementable add-associative right_zeroed addLoopStr
for v, v1, v2 being Element of V holds
( v = v1 + v2 iff v1 = v - v2 ) by Lm14;