let R be domRing; :: thesis: 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; :: thesis: 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; :: thesis: 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); :: thesis: 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; :: thesis: 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))) ; :: thesis: verum