let n be Nat; :: thesis: for Af being Subset of (RealVectSpace (Seg n))
for Ar being Subset of () st Af = Ar holds
( Af is linearly-independent iff Ar is linearly-independent )

set V = RealVectSpace (Seg n);
let AV be Subset of (RealVectSpace (Seg n)); :: thesis: for Ar being Subset of () st AV = Ar holds
( AV is linearly-independent iff Ar is linearly-independent )

set T = TOP-REAL n;
let AR be Subset of (); :: thesis: ( AV = AR implies ( AV is linearly-independent iff AR is linearly-independent ) )
assume A1: AV = AR ; :: thesis: ( AV is linearly-independent iff AR is linearly-independent )
hereby :: thesis: ( AR is linearly-independent implies AV is linearly-independent )
assume A2: AV is linearly-independent ; :: thesis:
now :: thesis: for L being Linear_Combination of AR st Sum L = 0. () holds
Carrier L = {}
let L be Linear_Combination of AR; :: thesis: ( Sum L = 0. () implies Carrier L = {} )
reconsider L1 = L as Linear_Combination of RealVectSpace (Seg n) by Th17;
assume Sum L = 0. () ; :: thesis:
then A3: 0. (RealVectSpace (Seg n)) = Sum L by Lm2
.= Sum L1 by Th20 ;
Carrier L c= AR by RLVECT_2:def 6;
then L1 is Linear_Combination of AV by ;
hence Carrier L = {} by ; :: thesis: verum
end;
hence AR is linearly-independent by RLVECT_3:def 1; :: thesis: verum
end;
assume A4: AR is linearly-independent ; :: thesis:
now :: thesis: for L being Linear_Combination of AV st Sum L = 0. (RealVectSpace (Seg n)) holds
Carrier L = {}
let L be Linear_Combination of AV; :: thesis: ( Sum L = 0. (RealVectSpace (Seg n)) implies Carrier L = {} )
reconsider L1 = L as Linear_Combination of TOP-REAL n by Th17;
Carrier L c= AV by RLVECT_2:def 6;
then reconsider L1 = L1 as Linear_Combination of AR by ;
assume Sum L = 0. (RealVectSpace (Seg n)) ; :: thesis:
then 0. () = Sum L by Lm2
.= Sum L1 by Th20 ;
hence Carrier L = {} by ; :: thesis: verum
end;
hence AV is linearly-independent by RLVECT_3:def 1; :: thesis: verum