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
( Ar is linearly-independent iff At is linearly-independent ) )
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
( Ar is linearly-independent iff At is linearly-independent )
let Ar be Subset of RNS2; :: thesis: for At being Subset of RNS1 st Ar = At holds
( Ar is linearly-independent iff At is linearly-independent )
let At be Subset of RNS1; :: thesis: ( Ar = At implies ( Ar is linearly-independent iff At is linearly-independent ) )
assume A2: Ar = At ; :: thesis: ( Ar is linearly-independent iff At is linearly-independent )

hereby :: thesis: ( At is linearly-independent implies Ar is linearly-independent )

assume A3: Ar is linearly-independent ; :: thesis: At is linearly-independent

now :: thesis: for L being Linear_Combination of At st Sum L = 0. RNS1 holds
Carrier L = {}

let L be Linear_Combination of At; :: thesis: ( Sum L = 0. RNS1 implies Carrier L = {} )
reconsider L1 = L as Linear_Combination of RNS2 by Th7, A1;
A4: Carrier L1 = Carrier L ;
assume Sum L = 0. RNS1 ; :: thesis: Carrier L = {}
then A5: 0. RNS2 = Sum L1 by Th14, A1;
L1 is Linear_Combination of Ar by A2, A4, RLVECT_2:def 6;
hence Carrier L = {} by A3, A5, RLVECT_3:def 1; :: thesis: verum

end;

hence At is linearly-independent by RLVECT_3:def 1; :: thesis: verum

end;

assume A6: At is linearly-independent ; :: thesis: Ar is linearly-independent

now :: thesis: for L being Linear_Combination of Ar st Sum L = 0. RNS2 holds
Carrier L = {}

let L be Linear_Combination of Ar; :: thesis: ( Sum L = 0. RNS2 implies Carrier L = {} )
reconsider L1 = L as Linear_Combination of RNS1 by Th7, A1;
Carrier L1 = Carrier L ;
then reconsider L1 = L as Linear_Combination of At by A2, RLVECT_2:def 6;
assume Sum L = 0. RNS2 ; :: thesis: Carrier L = {}
then 0. RNS1 = Sum L1 by Th14, A1;
hence Carrier L = {} by A6, RLVECT_3:def 1; :: thesis: verum

end;

hence Ar is linearly-independent by RLVECT_3:def 1; :: thesis: verum