let X be set ; :: thesis: for n being Nat holds
( X is Linear_Combination of n -VectSp_over F_Real iff X is Linear_Combination of TOP-REAL n )
let n be Nat; :: thesis: ( X is Linear_Combination of n -VectSp_over F_Real iff X is Linear_Combination of TOP-REAL n )
set V = n -VectSp_over F_Real;
set T = TOP-REAL n;

hereby :: thesis: ( X is Linear_Combination of TOP-REAL n implies X is Linear_Combination of n -VectSp_over F_Real )

assume X is Linear_Combination of n -VectSp_over F_Real ; :: thesis: X is Linear_Combination of TOP-REAL n
then reconsider L = X as Linear_Combination of n -VectSp_over F_Real ;
consider S being finite Subset of (n -VectSp_over F_Real) such that
A1: for v being Element of (n -VectSp_over F_Real) st not v in S holds
L . v = 0. F_Real by VECTSP_6:def 1;

A2: now :: thesis: for v being Element of (TOP-REAL n) st not v in S holds
0 = L . v

let v be Element of (TOP-REAL n); :: thesis: ( not v in S implies 0 = L . v )
assume A3: not v in S ; :: thesis: 0 = L . v
v is Element of (n -VectSp_over F_Real) by Lm1;
hence 0 = L . v by A1, A3; :: thesis: verum

end;

( L is Element of Funcs ( the carrier of (TOP-REAL n),REAL) & S is finite Subset of (TOP-REAL n) ) by Lm1;
hence X is Linear_Combination of TOP-REAL n by A2, RLVECT_2:def 3; :: thesis: verum

end;

assume X is Linear_Combination of TOP-REAL n ; :: thesis: X is Linear_Combination of n -VectSp_over F_Real
then reconsider L = X as Linear_Combination of TOP-REAL n ;
consider S being finite Subset of (TOP-REAL n) such that
A4: for v being Element of (TOP-REAL n) st not v in S holds
L . v = 0 by RLVECT_2:def 3;

A5: now :: thesis: for v being Element of (n -VectSp_over F_Real) st not v in S holds
0. F_Real = L . v

let v be Element of (n -VectSp_over F_Real); :: thesis: ( not v in S implies 0. F_Real = L . v )
assume A6: not v in S ; :: thesis: 0. F_Real = L . v
v is Element of (TOP-REAL n) by Lm1;
hence 0. F_Real = L . v by A4, A6; :: thesis: verum

end;

( L is Element of Funcs ( the carrier of (n -VectSp_over F_Real), the carrier of F_Real) & S is finite Subset of (n -VectSp_over F_Real) ) by Lm1;
hence X is Linear_Combination of n -VectSp_over F_Real by A5, VECTSP_6:def 1; :: thesis: verum