let n be Nat; :: thesis: for X being set holds
( X is Basis of (n -VectSp_over F_Real) iff X is Basis of TOP-REAL n )
let X be set ; :: thesis: ( X is Basis of (n -VectSp_over F_Real) iff X is Basis of TOP-REAL n )
set V = n -VectSp_over F_Real;
set W = TOP-REAL n;
hereby :: thesis: ( X is Basis of TOP-REAL n implies X is Basis of (n -VectSp_over F_Real) )
assume X is Basis of (n -VectSp_over F_Real) ; :: thesis: X is Basis of TOP-REAL n
then reconsider A = X as Basis of (n -VectSp_over F_Real) ;
reconsider B = A as Subset of (TOP-REAL n) by Lm1;
( A is linearly-independent & Lin A = ModuleStr(# the carrier of (n -VectSp_over F_Real), the addF of (n -VectSp_over F_Real), the ZeroF of (n -VectSp_over F_Real), the lmult of (n -VectSp_over F_Real) #) ) by VECTSP_7:def 3;
then A1: B is linearly-independent by MATRTOP2:7;
set W0 = Lin B;
A2: ( the carrier of (Lin B) c= the carrier of (TOP-REAL n) & 0. (Lin B) = 0. (TOP-REAL n) & the addF of (Lin B) = the addF of (TOP-REAL n) || the carrier of (Lin B) & the Mult of (Lin B) = the Mult of (TOP-REAL n) | [:REAL, the carrier of (Lin B):] ) by RLSUB_1:def 2;
the carrier of (Lin B) = [#] (Lin B)
.= [#] (Lin A) by MATRTOP2:6
.= the carrier of (n -VectSp_over F_Real) by VECTSP_7:def 3
.= the carrier of (TOP-REAL n) by Lm1 ;
hence X is Basis of TOP-REAL n by A2, A1, RLVECT_3:def 3; :: thesis: verum
end;
assume X is Basis of TOP-REAL n ; :: thesis: X is Basis of (n -VectSp_over F_Real)
then reconsider A = X as Basis of TOP-REAL n ;
reconsider B = A as Subset of (n -VectSp_over F_Real) by Lm1;
A3: ( A is linearly-independent & Lin A = RLSStruct(# the carrier of (TOP-REAL n), the ZeroF of (TOP-REAL n), the addF of (TOP-REAL n), the Mult of (TOP-REAL n) #) ) by RLVECT_3:def 3;
then A4: B is linearly-independent by MATRTOP2:7;
set V0 = Lin B;
A5: ( the carrier of (Lin B) c= the carrier of (n -VectSp_over F_Real) & 0. (Lin B) = 0. (n -VectSp_over F_Real) & the addF of (Lin B) = the addF of (n -VectSp_over F_Real) || the carrier of (Lin B) & the lmult of (Lin B) = the lmult of (n -VectSp_over F_Real) | [: the carrier of F_Real, the carrier of (Lin B):] ) by VECTSP_4:def 2;
the carrier of (Lin B) = [#] (Lin B)
.= [#] (Lin A) by MATRTOP2:6
.= the carrier of (n -VectSp_over F_Real) by A3, Lm1 ;
hence X is Basis of (n -VectSp_over F_Real) by A4, A5, VECTSP_7:def 3; :: thesis: verum