theorem Th6: :: RUSUB_1:6

for V being RealUnitarySpace
for W being Subspace of V
for u, v being VECTOR of V
for w1, w2 being VECTOR of W st w1 = v & w2 = u holds
w1 + w2 = v + u