let X be set ; :: thesis: for n being Nat holds
( X is Linear_Combination of REAL-NS n iff X is Linear_Combination of TOP-REAL n )
let n be Nat; :: thesis: ( X is Linear_Combination of REAL-NS n iff X is Linear_Combination of TOP-REAL n )
A1: the carrier of (TOP-REAL n) = the carrier of (REAL-NS n) by Th4;
hereby :: thesis: ( X is Linear_Combination of TOP-REAL n implies X is Linear_Combination of REAL-NS n )
assume X is Linear_Combination of REAL-NS n ; :: thesis: X is Linear_Combination of TOP-REAL n
then reconsider Lr = X as Linear_Combination of REAL-NS n ;
consider T being finite Subset of (REAL-NS n) such that
A2: for v being Element of (REAL-NS n) st not v in T holds
Lr . v = 0 by RLVECT_2:def 3;
thus X is Linear_Combination of TOP-REAL n by A1, A2, RLVECT_2:def 3; :: thesis: verum
end;
assume X is Linear_Combination of TOP-REAL n ; :: thesis: X is Linear_Combination of REAL-NS n
then reconsider Lr = X as Linear_Combination of TOP-REAL n ;
consider T being finite Subset of (TOP-REAL n) such that
A3: for v being Element of (TOP-REAL n) st not v in T holds
Lr . v = 0 by RLVECT_2:def 3;
thus X is Linear_Combination of REAL-NS n by A1, A3, RLVECT_2:def 3; :: thesis: verum