let R be Ring; :: thesis: for S being R -homomorphic Ring
for T being b₁ -homomorphic Ring
for f being Homomorphism of R,S
for g being Homomorphism of S,T holds ker f c= ker (g * f)
let S be R -homomorphic Ring; :: thesis: for T being S -homomorphic Ring
for f being Homomorphism of R,S
for g being Homomorphism of S,T holds ker f c= ker (g * f)
let T be S -homomorphic Ring; :: thesis: for f being Homomorphism of R,S
for g being Homomorphism of S,T holds ker f c= ker (g * f)
let f be Homomorphism of R,S; :: thesis: for g being Homomorphism of S,T holds ker f c= ker (g * f)
let g be Homomorphism of S,T; :: thesis: ker f c= ker (g * f)

now :: thesis: for x being object st x in ker f holds
x in ker (g * f)

let x be object ; :: thesis: ( x in ker f implies x in ker (g * f) )
assume x in ker f ; :: thesis: x in ker (g * f)
then consider r being Element of R such that
A1: ( x = r & f . r = 0. S ) ;
(g * f) . r = g . (f . r) by FUNCT_2:15
.= 0. T by A1, RING_2:6 ;
hence x in ker (g * f) by A1; :: thesis: verum

end;

hence ker f c= ker (g * f) ; :: thesis: verum