theorem :: ZMODUL05:23
for V, W being Z_Module
for T being linear-transformation of V,W
for y being Element of W holds
( y in im T iff ex x being Element of V st y = T . x ) by RANKNULL:13;