let R be Ring; :: thesis: for S being R -homomorphic Ring
for h being Homomorphism of R,S
for a being Element of R holds (PolyHom h) . (a | R) = (h . a) | S
let S be R -homomorphic Ring; :: thesis: for h being Homomorphism of R,S
for a being Element of R holds (PolyHom h) . (a | R) = (h . a) | S
let h be Homomorphism of R,S; :: thesis: for a being Element of R holds (PolyHom h) . (a | R) = (h . a) | S
let a be Element of R; :: thesis: (PolyHom h) . (a | R) = (h . a) | S
reconsider g = a | R as Element of the carrier of (Polynom-Ring R) by POLYNOM3:def 10;

now :: thesis: for i being Element of NAT holds ((PolyHom h) . g) . i = ((h . a) | S) . i

let i be Element of NAT ; :: thesis: ((PolyHom h) . g) . b₁ = ((h . a) | S) . b₁

per cases ( i <> 0 or i = 0 ) ;

suppose A: i <> 0 ; :: thesis: ((PolyHom h) . g) . b₁ = ((h . a) | S) . b₁

thus ((PolyHom h) . g) . i = h . (g . i) by FIELD_1:def 2
.= h . (0. R) by A, poly0
.= 0. S by RING_2:6
.= ((h . a) | S) . i by A, poly0 ; :: thesis: verum

end;

suppose B: i = 0 ; :: thesis: ((PolyHom h) . g) . b₁ = ((h . a) | S) . b₁

thus ((PolyHom h) . g) . i = h . (g . i) by FIELD_1:def 2
.= h . a by B, poly0
.= ((h . a) | S) . i by B, poly0 ; :: thesis: verum

end;

end;

end;

hence (PolyHom h) . (a | R) = (h . a) | S by FUNCT_2:63; :: thesis: verum