let RNS1, RNS2 be RealLinearSpace; :: thesis: ( RLSStruct(# the carrier of RNS1, the ZeroF of RNS1, the addF of RNS1, the Mult of RNS1 #) = RLSStruct(# the carrier of RNS2, the ZeroF of RNS2, the addF of RNS2, the Mult of RNS2 #) implies for Ar being Subset of RNS2
for At being Subset of RNS1 st Ar = At holds
for X being object holds
( X is Linear_Combination of Ar iff X is Linear_Combination of At ) )
assume A1: RLSStruct(# the carrier of RNS1, the ZeroF of RNS1, the addF of RNS1, the Mult of RNS1 #) = RLSStruct(# the carrier of RNS2, the ZeroF of RNS2, the addF of RNS2, the Mult of RNS2 #) ; :: thesis: for Ar being Subset of RNS2
for At being Subset of RNS1 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 RNS2; :: thesis: for At being Subset of RNS1 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 RNS1; :: thesis: ( Ar = At implies for X being object holds
( X is Linear_Combination of Ar iff X is Linear_Combination of At ) )
assume A2: 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 RNS1 by Th7, A1;
( Carrier L1 = Carrier L & Carrier L c= Ar ) by RLVECT_2:def 6;
hence X is Linear_Combination of At by A2, 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 RNS2 by Th7, A1;
( Carrier L1 = Carrier L & Carrier L c= At ) by RLVECT_2:def 6;
hence X is Linear_Combination of Ar by A2, RLVECT_2:def 6; :: thesis: verum