theorem :: REAL_NS2:31

for n being Nat
for X being set
for U being Subspace of REAL-NS n
for W being Subspace of n -VectSp_over F_Real st [#] U = [#] W holds
( X is Linear_Combination of U iff X is Linear_Combination of W )