:: deftheorem defines rank ZMODUL07:def 4 :
for W being free finite-rank Z_Module
for V being Z_Module
for T being linear-transformation of V,W holds rank T = rank (im T);