for n being Nat
for U being Subspace of n -VectSp_over F_Real
for W being Subspace of TOP-REAL n
for LU being Linear_Combination of U
for LW being Linear_Combination of W st LU = LW holds
( Carrier LU = Carrier LW & Sum LU = Sum LW )