for X being set
for n being Nat holds
( X is Linear_Combination of REAL-NS n iff X is Linear_Combination of n -VectSp_over F_Real )