:: deftheorem Def2 defines im ZMODUL05:def 5 :
for V, W being Z_Module
for T being linear-transformation of V,W
for b₄ being strict Submodule of W holds
( b₄ = im T iff [#] b₄ = T .: ([#] V) );