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) * (PolyHom 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) * (PolyHom 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) * (PolyHom 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) * (PolyHom f) = id (Polynom-Ring R)
let g be additive Function of S,T; :: thesis: ( g * f = id R implies (PolyHom g) * (PolyHom f) = id (Polynom-Ring R) )
assume AS: g * f = id R ; :: thesis: (PolyHom g) * (PolyHom f) = id (Polynom-Ring R)
A: dom ((PolyHom g) * (PolyHom f)) = the carrier of (Polynom-Ring R) by FUNCT_2:def 1;

now :: thesis: for o being object st o in dom ((PolyHom g) * (PolyHom f)) holds
o = ((PolyHom g) * (PolyHom f)) . o

let o be object ; :: thesis: ( o in dom ((PolyHom g) * (PolyHom f)) implies o = ((PolyHom g) * (PolyHom f)) . o )
assume o in dom ((PolyHom g) * (PolyHom f)) ; :: thesis: o = ((PolyHom g) * (PolyHom f)) . o
then reconsider p = o as Element of the carrier of (Polynom-Ring R) ;

now :: thesis: for i being Nat holds ((PolyHom (g * f)) . p) . i = p . i

let i be Nat; :: thesis: ((PolyHom (g * f)) . p) . i = p . i
thus ((PolyHom (g * f)) . p) . i = (g * f) . (p . i) by FIELD_1:def 2
.= p . i by AS ; :: thesis: verum

end;

then (PolyHom (g * f)) . p = p ;
hence o = ((PolyHom g) * (PolyHom f)) . o by ll; :: thesis: verum

end;

hence (PolyHom g) * (PolyHom f) = id (Polynom-Ring R) by A; :: thesis: verum