let W be RealLinearSpace; :: thesis: for X being set holds
( X is Basis of (RLSp2RVSp W) iff X is Basis of W )
let X be set ; :: thesis: ( X is Basis of (RLSp2RVSp W) iff X is Basis of W )
set V = RLSp2RVSp W;
hereby :: thesis: ( X is Basis of W implies X is Basis of (RLSp2RVSp W) )
assume X is Basis of (RLSp2RVSp W) ; :: thesis: X is Basis of W
then reconsider A = X as Basis of (RLSp2RVSp W) ;
reconsider B = A as Subset of W ;
( A is linearly-independent & Lin A = ModuleStr(# the carrier of (RLSp2RVSp W), the addF of (RLSp2RVSp W), the ZeroF of (RLSp2RVSp W), the lmult of (RLSp2RVSp W) #) ) by VECTSP_7:def 3;
then A1: B is linearly-independent by Th78;
set W0 = Lin B;
A2: ( the carrier of (Lin B) c= the carrier of W & 0. (Lin B) = 0. W & the addF of (Lin B) = the addF of W || the carrier of (Lin B) & the Mult of (Lin B) = the Mult of W | [:REAL, the carrier of (Lin B):] ) by RLSUB_1:def 2;
A3: the carrier of (Lin B) = [#] (Lin B)
.= [#] (Lin A) by Th77
.= the carrier of W by VECTSP_7:def 3 ;
thus X is Basis of W by A2, A3, A1, RLVECT_3:def 3; :: thesis: verum
end;
assume X is Basis of W ; :: thesis: X is Basis of (RLSp2RVSp W)
then reconsider A = X as Basis of W ;
reconsider B = A as Subset of (RLSp2RVSp W) ;
A4: ( A is linearly-independent & Lin A = RLSStruct(# the carrier of W, the ZeroF of W, the addF of W, the Mult of W #) ) by RLVECT_3:def 3;
then A5: B is linearly-independent by Th78;
set V0 = Lin B;
A6: ( the carrier of (Lin B) c= the carrier of (RLSp2RVSp W) & 0. (Lin B) = 0. (RLSp2RVSp W) & the addF of (Lin B) = the addF of (RLSp2RVSp W) || the carrier of (Lin B) & the lmult of (Lin B) = the lmult of (RLSp2RVSp W) | [: 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 Th77
.= the carrier of (RLSp2RVSp W) by A4 ;
hence X is Basis of (RLSp2RVSp W) by A5, A6, VECTSP_7:def 3; :: thesis: verum