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