let n be Nat; :: thesis:
set V = RealVectSpace (Seg n);
let AV be Subset of (RealVectSpace (Seg n)); :: thesis:
set T = TOP-REAL n;
let AR be Subset of (TOP-REAL n); :: thesis:
assume A1: AV = AR ; :: thesis:

hereby :: thesis:

assume A2: AV is linearly-independent ; :: thesis:

now :: thesis:

let L be Linear_Combination of AR; :: thesis:
reconsider L1 = L as Linear_Combination of RealVectSpace (Seg n) by Th17;
assume Sum L = 0. (TOP-REAL n) ; :: 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 A1, RLVECT_2:def 6;
hence Carrier L = {} by A2, A3, RLVECT_3:def 1; :: thesis:

end;

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

end;

assume A4: AR is linearly-independent ; :: thesis:

now :: thesis:

let L be Linear_Combination of AV; :: thesis:
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 A1, RLVECT_2:def 6;
assume Sum L = 0. (RealVectSpace (Seg n)) ; :: thesis:
then 0. (TOP-REAL n) = Sum L by Lm2
.= Sum L1 by Th20 ;
hence Carrier L = {} by A4, RLVECT_3:def 1; :: thesis:

end;

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