let F be Ring; :: thesis: for V, W being VectSp of F

for T being linear-transformation of V,W

for X being Subset of V holds T .: X is Subset of (im T)

let V, W be VectSp of F; :: thesis: for T being linear-transformation of V,W

for X being Subset of V holds T .: X is Subset of (im T)

let T be linear-transformation of V,W; :: thesis: for X being Subset of V holds T .: X is Subset of (im T)

let X be Subset of V; :: thesis: T .: X is Subset of (im T)

[#] (im T) = T .: ([#] V) by Def2;

hence T .: X is Subset of (im T) by RELAT_1:123; :: thesis: verum

for T being linear-transformation of V,W

for X being Subset of V holds T .: X is Subset of (im T)

let V, W be VectSp of F; :: thesis: for T being linear-transformation of V,W

for X being Subset of V holds T .: X is Subset of (im T)

let T be linear-transformation of V,W; :: thesis: for X being Subset of V holds T .: X is Subset of (im T)

let X be Subset of V; :: thesis: T .: X is Subset of (im T)

[#] (im T) = T .: ([#] V) by Def2;

hence T .: X is Subset of (im T) by RELAT_1:123; :: thesis: verum