let n be Nat; :: thesis: for Af being Subset of (RealVectSpace (Seg n))

for Ar being Subset of (TOP-REAL n) 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 (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 )

for Ar being Subset of (TOP-REAL n) 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 (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 A4:
AR is linearly-independent
; :: thesis: AV is linearly-independent assume A2:
AV is linearly-independent
; :: thesis: AR is linearly-independent

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

Carrier L = {}

hence
AR is linearly-independent
by RLVECT_3:def 1; :: thesis: verumCarrier 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 RealVectSpace (Seg n) by Th17;

assume Sum L = 0. (TOP-REAL n) ; :: thesis: Carrier L = {}

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: verum

end;reconsider L1 = L as Linear_Combination of RealVectSpace (Seg n) by Th17;

assume Sum L = 0. (TOP-REAL n) ; :: thesis: Carrier L = {}

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: verum

now :: thesis: for L being Linear_Combination of AV st Sum L = 0. (RealVectSpace (Seg n)) holds

Carrier L = {}

hence
AV is linearly-independent
by RLVECT_3:def 1; :: thesis: verumCarrier 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 A1, RLVECT_2:def 6;

assume Sum L = 0. (RealVectSpace (Seg n)) ; :: thesis: Carrier L = {}

then 0. (TOP-REAL n) = Sum L by Lm2

.= Sum L1 by Th20 ;

hence Carrier L = {} by A4, RLVECT_3:def 1; :: thesis: verum

end;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: Carrier L = {}

then 0. (TOP-REAL n) = Sum L by Lm2

.= Sum L1 by Th20 ;

hence Carrier L = {} by A4, RLVECT_3:def 1; :: thesis: verum