let n be Nat; :: thesis: for Ar being Subset of (REAL-NS n)
for At being Subset of (TOP-REAL n) st Ar = At holds
for X being object holds
( X is Linear_Combination of Ar iff X is Linear_Combination of At )
let Ar be Subset of (REAL-NS n); :: thesis: for At being Subset of (TOP-REAL n) st Ar = At holds
for X being object holds
( X is Linear_Combination of Ar iff X is Linear_Combination of At )
let At be Subset of (TOP-REAL n); :: thesis: ( Ar = At implies for X being object holds
( X is Linear_Combination of Ar iff X is Linear_Combination of At ) )
assume A1: Ar = At ; :: thesis: for X being object holds
( X is Linear_Combination of Ar iff X is Linear_Combination of At )
let X be object ; :: thesis: ( X is Linear_Combination of Ar iff X is Linear_Combination of At )

hereby :: thesis: ( X is Linear_Combination of At implies X is Linear_Combination of Ar )

assume X is Linear_Combination of Ar ; :: thesis: X is Linear_Combination of At
then reconsider L = X as Linear_Combination of Ar ;
reconsider L1 = L as Linear_Combination of TOP-REAL n by Th11;
( Carrier L1 = Carrier L & Carrier L c= Ar ) by RLVECT_2:def 6;
hence X is Linear_Combination of At by A1, RLVECT_2:def 6; :: thesis: verum

end;

assume X is Linear_Combination of At ; :: thesis: X is Linear_Combination of Ar
then reconsider L = X as Linear_Combination of At ;
reconsider L1 = L as Linear_Combination of REAL-NS n by Th11;
( Carrier L1 = Carrier L & Carrier L c= At ) by RLVECT_2:def 6;
hence X is Linear_Combination of Ar by A1, RLVECT_2:def 6; :: thesis: verum