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;

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;

hence X is Linear_Combination of RealVectSpace (Seg n) by A5, RLVECT_2:def 3; :: thesis: verum

( 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 TOP-REAL n
; :: thesis: 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;

hence X is Linear_Combination of TOP-REAL n by A2, RLVECT_2:def 3; :: thesis: verum

end;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

( L is Element of Funcs ( the carrier of (TOP-REAL n),REAL) & S is finite Subset of (TOP-REAL n) )
by Lm1;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;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

hence X is Linear_Combination of TOP-REAL n by A2, RLVECT_2:def 3; :: thesis: verum

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

( L is Element of Funcs ( the carrier of (RealVectSpace (Seg n)),REAL) & S is finite Subset of (RealVectSpace (Seg n)) )
by Lm1;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;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

hence X is Linear_Combination of RealVectSpace (Seg n) by A5, RLVECT_2:def 3; :: thesis: verum