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 holds PolyHom (g * f) = (PolyHom g) * (PolyHom f)
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 holds PolyHom (g * f) = (PolyHom g) * (PolyHom f)
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 holds PolyHom (g * f) = (PolyHom g) * (PolyHom f)
let f be additive Function of R,S; :: thesis: for g being additive Function of S,T holds PolyHom (g * f) = (PolyHom g) * (PolyHom f)
let g be additive Function of S,T; :: thesis: PolyHom (g * f) = (PolyHom g) * (PolyHom f)

now :: thesis: for o being object st o in the carrier of (Polynom-Ring R) holds
(PolyHom (g * f)) . o = ((PolyHom g) * (PolyHom f)) . o

let o be object ; :: thesis: ( o in the carrier of (Polynom-Ring R) implies (PolyHom (g * f)) . o = ((PolyHom g) * (PolyHom f)) . o )
assume o in the carrier of (Polynom-Ring R) ; :: thesis: (PolyHom (g * f)) . 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 = (((PolyHom g) * (PolyHom f)) . p) . i

let i be Nat; :: thesis: ((PolyHom (g * f)) . p) . i = (((PolyHom g) * (PolyHom f)) . p) . i
A: dom f = the carrier of R by FUNCT_2:def 1;
C: dom (PolyHom f) = the carrier of (Polynom-Ring R) by FUNCT_2:def 1;
thus ((PolyHom (g * f)) . p) . i = (g * f) . (p . i) by FIELD_1:def 2
.= g . (f . (p . i)) by A, FUNCT_1:13
.= g . (((PolyHom f) . p) . i) by FIELD_1:def 2
.= ((PolyHom g) . ((PolyHom f) . p)) . i by FIELD_1:def 2
.= (((PolyHom g) * (PolyHom f)) . p) . i by C, FUNCT_1:13 ; :: thesis: verum

end;

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

end;

hence PolyHom (g * f) = (PolyHom g) * (PolyHom f) ; :: thesis: verum