theorem Th7: :: RUSUB_1:7

for V being RealUnitarySpace
for W being Subspace of V
for v being VECTOR of V
for w being VECTOR of W
for a being Real st w = v holds
a * w = a * v