let X be set ; :: thesis: for n being Nat holds
( X is Linear_Combination of REAL-NS n iff X is Linear_Combination of n -VectSp_over F_Real )
let n be Nat; :: thesis: ( X is Linear_Combination of REAL-NS n iff X is Linear_Combination of n -VectSp_over F_Real )
( X is Linear_Combination of REAL-NS n iff X is Linear_Combination of TOP-REAL n ) by Th11;
hence ( X is Linear_Combination of REAL-NS n iff X is Linear_Combination of n -VectSp_over F_Real ) by MATRTOP2:1; :: thesis: verum