let n be Nat; :: thesis: for Af being Subset of (n -VectSp_over F_Real)
for Ar being Subset of (TOP-REAL n) st Af = Ar holds
( Af is linearly-independent iff Ar is linearly-independent )
set V = n -VectSp_over F_Real;
let AV be Subset of (n -VectSp_over F_Real); :: thesis: for Ar being Subset of (TOP-REAL n) st AV = Ar holds
( AV is linearly-independent iff Ar is linearly-independent )
set T = TOP-REAL n;
let AR be Subset of (TOP-REAL n); :: 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: AR is linearly-independent

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

let L be Linear_Combination of AR; :: thesis: ( Sum L = 0. (TOP-REAL n) implies Carrier L = {} )
reconsider L1 = L as Linear_Combination of n -VectSp_over F_Real by Th1;
A3: Carrier L1 = Carrier L by Th2;
assume Sum L = 0. (TOP-REAL n) ; :: thesis: Carrier L = {}
then A4: 0. (n -VectSp_over F_Real) = Sum L by Lm2
.= Sum L1 by Th5 ;
Carrier L c= AR by RLVECT_2:def 6;
then L1 is Linear_Combination of AV by A1, A3, VECTSP_6:def 4;
hence Carrier L = {} by A2, A3, A4, VECTSP_7:def 1; :: thesis: verum

end;

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

end;

assume A5: AR is linearly-independent ; :: thesis: AV is linearly-independent

now :: thesis: for L being Linear_Combination of AV st Sum L = 0. (n -VectSp_over F_Real) holds
Carrier L = {}

let L be Linear_Combination of AV; :: thesis: ( Sum L = 0. (n -VectSp_over F_Real) implies Carrier L = {} )
reconsider L1 = L as Linear_Combination of TOP-REAL n by Th1;
A6: Carrier L1 = Carrier L by Th2;
Carrier L c= AV by VECTSP_6:def 4;
then reconsider L1 = L1 as Linear_Combination of AR by A1, A6, RLVECT_2:def 6;
assume Sum L = 0. (n -VectSp_over F_Real) ; :: thesis: Carrier L = {}
then 0. (TOP-REAL n) = Sum L by Lm2
.= Sum L1 by Th5 ;
hence Carrier L = {} by A5, A6, RLVECT_3:def 1; :: thesis: verum

end;

hence AV is linearly-independent by VECTSP_7:def 1; :: thesis: verum