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

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