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