let R be Ring; :: thesis: for S being R -homomorphic Ring
for h being Homomorphism of R,S
for p being Element of the carrier of (Polynom-Ring R)
for a being Element of R st a is_a_root_of p holds
h . a is_a_root_of (PolyHom h) . p
let S be R -homomorphic Ring; :: thesis: for h being Homomorphism of R,S
for p being Element of the carrier of (Polynom-Ring R)
for a being Element of R st a is_a_root_of p holds
h . a is_a_root_of (PolyHom h) . p
let h be Homomorphism of R,S; :: thesis: for p being Element of the carrier of (Polynom-Ring R)
for a being Element of R st a is_a_root_of p holds
h . a is_a_root_of (PolyHom h) . p
let p be Element of the carrier of (Polynom-Ring R); :: thesis: for a being Element of R st a is_a_root_of p holds
h . a is_a_root_of (PolyHom h) . p
let a be Element of R; :: thesis: ( a is_a_root_of p implies h . a is_a_root_of (PolyHom h) . p )
assume a is_a_root_of p ; :: thesis: h . a is_a_root_of (PolyHom h) . p
then eval (p,a) = 0. R by POLYNOM5:def 7;
then eval (((PolyHom h) . p),(h . a)) = h . (0. R) by Th28
.= 0. S by RING_2:6 ;
hence h . a is_a_root_of (PolyHom h) . p by POLYNOM5:def 7; :: thesis: verum