let R be Ring; :: thesis: for V, W being LeftMod of R
for T being linear-transformation of V,W holds T = (Zdecom T) * (ZQMorph (V,(ker T)))
let V, W be LeftMod of R; :: thesis: for T being linear-transformation of V,W holds T = (Zdecom T) * (ZQMorph (V,(ker T)))
let T be linear-transformation of V,W; :: thesis: T = (Zdecom T) * (ZQMorph (V,(ker T)))
set g = (Zdecom T) * (ZQMorph (V,(ker T)));
A1: dom ((Zdecom T) * (ZQMorph (V,(ker T)))) = the carrier of V by FUNCT_2:def 1;
the carrier of (im T) c= the carrier of W by VECTSP_4:def 2;
then rng ((Zdecom T) * (ZQMorph (V,(ker T)))) c= the carrier of W ;
then reconsider g = (Zdecom T) * (ZQMorph (V,(ker T))) as Function of V,W by FUNCT_2:2, A1;
for z being Element of V holds T . z = g . z

proof

let z be Element of V; :: thesis: T . z = g . z
thus T . z = (Zdecom T) . ((ZQMorph (V,(ker T))) . z) by defdecom
.= g . z by FUNCT_2:15 ; :: thesis: verum

end;

hence T = (Zdecom T) * (ZQMorph (V,(ker T))) by FUNCT_2:def 8; :: thesis: verum