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

hereby :: thesis: ( X is Linear_Combination of TOP-REAL n implies X is Linear_Combination of RealVectSpace (Seg n) )

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

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 (RealVectSpace (Seg n)) 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 RealVectSpace (Seg n)
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 (RealVectSpace (Seg n)) st not v in S holds
0 = L . v

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

end;

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