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
( Ar is linearly-independent iff At is linearly-independent )
let Ar be Subset of (REAL-NS n); :: thesis: for At being Subset of (TOP-REAL n) st Ar = At holds
( Ar is linearly-independent iff At is linearly-independent )
let At be Subset of (TOP-REAL n); :: thesis: ( Ar = At implies ( Ar is linearly-independent iff At is linearly-independent ) )
assume A1: Ar = At ; :: thesis: ( Ar is linearly-independent iff At is linearly-independent )

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

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

now :: thesis: for L being Linear_Combination of At st Sum L = 0. (TOP-REAL n) holds
Carrier L = {}

let L be Linear_Combination of At; :: thesis: ( Sum L = 0. (TOP-REAL n) implies Carrier L = {} )
reconsider L1 = L as Linear_Combination of REAL-NS n by Th11;
A3: Carrier L1 = Carrier L ;
assume Sum L = 0. (TOP-REAL n) ; :: thesis: Carrier L = {}
then A4: 0. (REAL-NS n) = Sum L by Th6
.= Sum L1 by Th23 ;
L1 is Linear_Combination of Ar by A1, A3, RLVECT_2:def 6;
hence Carrier L = {} by A2, A4, RLVECT_3:def 1; :: thesis: verum

end;

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

end;

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

now :: thesis: for L being Linear_Combination of Ar st Sum L = 0. (REAL-NS n) holds
Carrier L = {}

let L be Linear_Combination of Ar; :: thesis: ( Sum L = 0. (REAL-NS n) implies Carrier L = {} )
reconsider L1 = L as Linear_Combination of TOP-REAL n by Th11;
A6: Carrier L1 = Carrier L ;
reconsider L1 = L as Linear_Combination of At by A1, A6, RLVECT_2:def 6;
assume Sum L = 0. (REAL-NS n) ; :: thesis: Carrier L = {}
then 0. (TOP-REAL n) = Sum L by Th6
.= Sum L1 by Th23 ;
hence Carrier L = {} by A5, RLVECT_3:def 1; :: thesis: verum

end;

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