let R be Ring; :: thesis: for V, U, W being LeftMod of R
for f being linear-transformation of V,U
for g being linear-transformation of U,W holds the carrier of (ker (g * f)) = f " the carrier of (ker g)
let V, U, W be LeftMod of R; :: thesis: for f being linear-transformation of V,U
for g being linear-transformation of U,W holds the carrier of (ker (g * f)) = f " the carrier of (ker g)
let f be linear-transformation of V,U; :: thesis: for g being linear-transformation of U,W holds the carrier of (ker (g * f)) = f " the carrier of (ker g)
let g be linear-transformation of U,W; :: thesis: the carrier of (ker (g * f)) = f " the carrier of (ker g)
thus the carrier of (ker (g * f)) = (g * f) " {(0. W)} by LMFirst2
.= f " (g " {(0. W)}) by RELAT_1:146
.= f " the carrier of (ker g) by LMFirst2 ; :: thesis: verum