let R be Ring; :: thesis: for V, W being LeftMod of R
for T being linear-transformation of V,W
for A being Subset of V holds T .: the carrier of (Lin A) c= the carrier of (Lin (T .: A))
let V, W be LeftMod of R; :: thesis: for T being linear-transformation of V,W
for A being Subset of V holds T .: the carrier of (Lin A) c= the carrier of (Lin (T .: A))
let T be linear-transformation of V,W; :: thesis: for A being Subset of V holds T .: the carrier of (Lin A) c= the carrier of (Lin (T .: A))
let A be Subset of V; :: thesis: T .: the carrier of (Lin A) c= the carrier of (Lin (T .: A))
for y being object st y in T .: the carrier of (Lin A) holds
y in the carrier of (Lin (T .: A))
proof
let y be object ; :: thesis: ( y in T .: the carrier of (Lin A) implies y in the carrier of (Lin (T .: A)) )
assume y in T .: the carrier of (Lin A) ; :: thesis: y in the carrier of (Lin (T .: A))
then consider x being Element of V such that
A2: ( x in the carrier of (Lin A) & y = T . x ) by FUNCT_2:65;
x in Lin A by A2;
then consider l being Linear_Combination of A such that
A3: x = Sum l by MOD_3:4;
reconsider l = l as Linear_Combination of V ;
reconsider Tl = T @* l as Linear_Combination of T .: (Carrier l) by ZMODUL05:44;
Sum Tl = T . (Sum l) by ZMODUL05:46;
then A5: y in Lin (T .: (Carrier l)) by A2, A3, MOD_3:4;
T .: (Carrier l) c= T .: A by RELAT_1:123, VECTSP_6:def 4;
then Lin (T .: (Carrier l)) is Subspace of Lin (T .: A) by MOD_3:10;
then the carrier of (Lin (T .: (Carrier l))) c= the carrier of (Lin (T .: A)) by VECTSP_4:def 2;
hence y in the carrier of (Lin (T .: A)) by A5; :: thesis: verum
end;
hence T .: the carrier of (Lin A) c= the carrier of (Lin (T .: A)) ; :: thesis: verum