let F be Field; :: thesis: for X, Y being VectSp of F
for T being linear-transformation of X,Y
for A being Subset of X st T is bijective & A is Basis of X holds
T .: A is Basis of Y
let X, Y be VectSp of F; :: thesis: for T being linear-transformation of X,Y
for A being Subset of X st T is bijective & A is Basis of X holds
T .: A is Basis of Y
let T be linear-transformation of X,Y; :: thesis: for A being Subset of X st T is bijective & A is Basis of X holds
T .: A is Basis of Y
let A be Subset of X; :: thesis: ( T is bijective & A is Basis of X implies T .: A is Basis of Y )
assume AS1: T is bijective ; :: thesis: ( not A is Basis of X or T .: A is Basis of Y )
assume A is Basis of X ; :: thesis: T .: A is Basis of Y
then P1: ( A is linearly-independent & Lin A = ModuleStr(# the carrier of X, the addF of X, the ZeroF of X, the lmult of X #) ) by VECTSP_7:def 3;
D1: dom T = the carrier of X by FUNCT_2:def 1;
R1: rng T = the carrier of Y by FUNCT_2:def 3, AS1;
P2: T .: A is linearly-independent by ZMODUL06:45, AS1, P1;
P6: Lin (T .: A) is strict Subspace of (Omega). Y by ZMODUL06:47;
the carrier of (Lin (T .: A)) = T .: the carrier of ModuleStr(# the carrier of X, the addF of X, the ZeroF of X, the lmult of X #) by P1, AS1, ZMODUL06:46
.= the carrier of ((Omega). Y) by D1, R1, RELAT_1:113 ;
hence T .: A is Basis of Y by P2, VECTSP_7:def 3, P6, VECTSP_4:31; :: thesis: verum