let R be Ring; :: thesis: for X, Y being LeftMod of R
for A being Subset of X
for T being linear-transformation of X,Y st T is bijective holds
T .: the carrier of (Lin A) = the carrier of (Lin (T .: A))
let X, Y be LeftMod of R; :: thesis: for A being Subset of X
for T being linear-transformation of X,Y st T is bijective holds
T .: the carrier of (Lin A) = the carrier of (Lin (T .: A))
let A be Subset of X; :: thesis: for T being linear-transformation of X,Y st T is bijective holds
T .: the carrier of (Lin A) = the carrier of (Lin (T .: A))
let T be linear-transformation of X,Y; :: thesis: ( T is bijective implies T .: the carrier of (Lin A) = the carrier of (Lin (T .: A)) )
assume AS1: T is bijective ; :: thesis: T .: the carrier of (Lin A) = the carrier of (Lin (T .: A))
X1: T .: the carrier of (Lin A) c= the carrier of (Lin (T .: A)) by ThTF3C;
reconsider B = T .: A as Subset of Y ;
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;
consider K being linear-transformation of Y,X such that
AS3: ( K = T " & K is bijective ) by HM1, AS1;
K .: B = A by D1, AS1, AS3, FUNCT_1:107;
then X3: T .: (K .: the carrier of (Lin B)) c= T .: the carrier of (Lin A) by RELAT_1:123, ThTF3C;
X4: the carrier of (Lin B) c= rng T by R1, VECTSP_4:def 2;
T .: (K .: the carrier of (Lin B)) = T .: (T " the carrier of (Lin B)) by FUNCT_1:85, AS1, AS3
.= the carrier of (Lin B) by X4, FUNCT_1:77 ;
hence T .: the carrier of (Lin A) = the carrier of (Lin (T .: A)) by X1, XBOOLE_0:def 10, X3; :: thesis: verum