let X, Y be free Z_Module; :: 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 HM6, AS1, P1;
P6: Lin (T .: A) is strict Subspace of (Omega). Y by HM8;
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, HM7
.= 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, ZMODUL01:47; :: thesis: verum