theorem :: RLVECT_4:2

for V being RealLinearSpace
for v1, v2, w being VECTOR of V st v1 - w = v2 - w holds
v1 = v2