let R be Ring; :: thesis: for S being R -homomorphic R -monomorphic Ring
for h being Monomorphism of R,S
for p being Element of the carrier of (Polynom-Ring R)
for a being Element of R holds
( a is_a_root_of p iff h . a is_a_root_of (PolyHom h) . p )
let S be R -homomorphic R -monomorphic Ring; :: thesis: for h being Monomorphism of R,S
for p being Element of the carrier of (Polynom-Ring R)
for a being Element of R holds
( a is_a_root_of p iff h . a is_a_root_of (PolyHom h) . p )
let h be Monomorphism of R,S; :: thesis: for p being Element of the carrier of (Polynom-Ring R)
for a being Element of R holds
( a is_a_root_of p iff 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 holds
( a is_a_root_of p iff h . a is_a_root_of (PolyHom h) . p )
let a be Element of R; :: thesis: ( a is_a_root_of p iff h . a is_a_root_of (PolyHom h) . p )

now :: thesis: ( h . a is_a_root_of (PolyHom h) . p implies a is_a_root_of p )

assume A1: h . a is_a_root_of (PolyHom h) . p ; :: thesis: a is_a_root_of p
h . (0. R) = 0. S by RING_2:6
.= eval (((PolyHom h) . p),(h . a)) by A1, POLYNOM5:def 7
.= h . (eval (p,a)) by Th28 ;
then eval (p,a) = 0. R by FUNCT_2:19;
hence a is_a_root_of p by POLYNOM5:def 7; :: thesis: verum

end;

hence ( a is_a_root_of p iff h . a is_a_root_of (PolyHom h) . p ) by Th34; :: thesis: verum