theorem Th61: :: RUSUB_1:61

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 )