theorem :: RUSUB_1:5

for V being RealUnitarySpace
for W1, W2 being Subspace of V holds 0. W1 = 0. W2