let R be Ring; :: thesis: for S being R -homomorphic Ring
for T being R -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)
let S be R -homomorphic Ring; :: thesis: for T being R -homomorphic S -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)
let T be R -homomorphic S -homomorphic Ring; :: thesis: 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)
let f be additive Function of R,S; :: thesis: for g being additive Function of S,T st g * f = id R holds
PolyHom (g * f) = id (Polynom-Ring R)
let g be additive Function of S,T; :: thesis: ( g * f = id R implies PolyHom (g * f) = id (Polynom-Ring R) )
assume g * f = id R ; :: thesis: PolyHom (g * f) = id (Polynom-Ring R)
hence id (Polynom-Ring R) = (PolyHom g) * (PolyHom f) by ll2
.= PolyHom (g * f) by ll ;
:: thesis: verum