let F be Field; :: thesis: for W, V being VectSp of
for T being linear-transformation of V,W
for X being Subset of holds T .: X is Subset of
let W, V be VectSp of ; :: thesis: for T being linear-transformation of V,W
for X being Subset of holds T .: X is Subset of
let T be linear-transformation of V,W; :: thesis: for X being Subset of holds T .: X is Subset of
let X be Subset of ; :: thesis: T .: X is Subset of
[#] (im T) = T .: ([#] V) by Def2;
hence T .: X is Subset of by RELAT_1:156; :: thesis: verum