let R be Ring; :: thesis: for S being R -homomorphic Ring
for T being b₁ -monomorphic Ring
for f being Homomorphism of R,S
for g being Monomorphism of S,T holds ker f = ker (g * f)
let S be R -homomorphic Ring; :: thesis: for T being S -monomorphic Ring
for f being Homomorphism of R,S
for g being Monomorphism of S,T holds ker f = ker (g * f)
let T be S -monomorphic Ring; :: thesis: for f being Homomorphism of R,S
for g being Monomorphism of S,T holds ker f = ker (g * f)
let f be Homomorphism of R,S; :: thesis: for g being Monomorphism of S,T holds ker f = ker (g * f)
let g be Monomorphism of S,T; :: thesis: ker f = ker (g * f)
A1: ker g = {(0. S)} by RING_2:12;

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

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

end;

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