:: deftheorem Def2 defines im RANKNULL:def 2 :
for F being Ring
for V, W being VectSp of F
for T being linear-transformation of V,W
for b₅ being strict Subspace of W holds
( b₅ = im T iff [#] b₅ = T .: ([#] V) );