let R be Ring; 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; for T being linear-transformation of V,W holds T = (Zdecom T) * (ZQMorph (V,(ker T)))
let T be linear-transformation of V,W; 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
hence
T = (Zdecom T) * (ZQMorph (V,(ker T)))
by FUNCT_2:def 8; verum