let R be domRing; for S being R -homomorphic domRing
for h being Homomorphism of R,S
for p being Element of the carrier of (Polynom-Ring R)
for b, x being Element of R holds h . (eval ((b * p),x)) = (h . b) * (eval (((PolyHom h) . p),(h . x)))
let S be R -homomorphic domRing; for h being Homomorphism of R,S
for p being Element of the carrier of (Polynom-Ring R)
for b, x being Element of R holds h . (eval ((b * p),x)) = (h . b) * (eval (((PolyHom h) . p),(h . x)))
let h be Homomorphism of R,S; for p being Element of the carrier of (Polynom-Ring R)
for b, x being Element of R holds h . (eval ((b * p),x)) = (h . b) * (eval (((PolyHom h) . p),(h . x)))
let p be Element of the carrier of (Polynom-Ring R); for b, x being Element of R holds h . (eval ((b * p),x)) = (h . b) * (eval (((PolyHom h) . p),(h . x)))
let b, x be Element of R; h . (eval ((b * p),x)) = (h . b) * (eval (((PolyHom h) . p),(h . x)))
reconsider q = b * p as Element of the carrier of (Polynom-Ring R) by POLYNOM3:def 10;
h . (eval ((b * p),x)) =
eval (((PolyHom h) . q),(h . x))
by Th28
.=
eval (((h . b) * ((PolyHom h) . p)),(h . x))
by Th27
.=
(h . b) * (eval (((PolyHom h) . p),(h . x)))
by RING_5:7
;
hence
h . (eval ((b * p),x)) = (h . b) * (eval (((PolyHom h) . p),(h . x)))
; verum