:: deftheorem defdecom defines Zdecom ZMODUL07:def 6 :
for R being Ring
for V, W being LeftMod of R
for T being linear-transformation of V,W
for b₅ being linear-transformation of (VectQuot (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 ) ) );