let R be Ring; :: thesis: for X, Y being LeftMod of R
for T being linear-transformation of X,Y st T is bijective & X is free holds
Y is free
let X, Y be LeftMod of R; :: thesis: for T being linear-transformation of X,Y st T is bijective & X is free holds
Y is free
let T be linear-transformation of X,Y; :: thesis: ( T is bijective & X is free implies Y is free )
assume AS1: T is bijective ; :: thesis: ( not X is free or Y is free )
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;
assume X is free ; :: thesis: Y is free
then consider A being Subset of X such that
p1: A is base ;
P2: T .: A is linearly-independent by HM6, AS1, p1;
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 ;
then Lin (T .: A) = (Omega). Y by VECTSP_4:29
.= ModuleStr(# the carrier of Y, the addF of Y, the ZeroF of Y, the lmult of Y #) ;
then T .: A is base by P2;
hence Y is free ; :: thesis: verum