theorem Th60: :: RUSUB_1:60

for V being RealUnitarySpace
for W being Subspace of V
for u, v being VECTOR of V st v + W = u + W holds
ex v1 being VECTOR of V st
( v1 in W & v + v1 = u )