theorem :: FIELD_12:36

for R being Ring
for S being b₁ -homomorphic Ring
for T being b₁ -homomorphic b₂ -homomorphic Ring
for f being additive Function of R,S
for g being additive Function of S,T st g * f = id R holds
PolyHom (g * f) = id (Polynom-Ring R)