:: deftheorem defMorph defines MorphsZQ ZMODUL04:def 6 :
for V being Z_Module st V is Mult-cancelable holds
for b₂ being Function of V,(Z_MQ_VectSp V) holds
( b₂ = MorphsZQ V iff ( b₂ is one-to-one & ( for v being Element of V holds b₂ . v = Class ((EQRZM V),[v,1]) ) & ( for v, w being Element of V holds b₂ . (v + w) = (b₂ . v) + (b₂ . w) ) & ( for v being Element of V
for i being Element of INT.Ring
for q being Element of F_Rat st i = q holds
b₂ . (i * v) = q * (b₂ . v) ) & b₂ . (0. V) = 0. (Z_MQ_VectSp V) ) );