:: deftheorem defdecom defines Zdecom ZMODUL07:def 6 :
for V, W being Z_Module
for T being linear-transformation of V,W
for b₄ being linear-transformation of (Z_ModuleQuot (V,(ker T))),(im T) holds
( b₄ = Zdecom T iff ( b₄ is bijective & ( for v being Element of V holds b₄ . ((ZQMorph (V,(ker T))) . v) = T . v ) ) );