theorem Th57: :: RUSUB_1:57

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