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) holds Roots p c= { a where a is Element of R : h . a in Roots ((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) holds Roots p c= { a where a is Element of R : h . a in Roots ((PolyHom h) . p) }
let h be Homomorphism of R,S; :: thesis: for p being Element of the carrier of (Polynom-Ring R) holds Roots p c= { a where a is Element of R : h . a in Roots ((PolyHom h) . p) }
let p be Element of the carrier of (Polynom-Ring R); :: thesis: Roots p c= { a where a is Element of R : h . a in Roots ((PolyHom h) . p) }
let o be object ; :: according to TARSKI:def 3 :: thesis: ( not o in Roots p or o in { a where a is Element of R : h . a in Roots ((PolyHom h) . p) } )
assume A1: o in Roots p ; :: thesis: o in { a where a is Element of R : h . a in Roots ((PolyHom h) . p) }
then reconsider a = o as Element of R ;
a is_a_root_of p by A1, POLYNOM5:def 10;
then h . a is_a_root_of (PolyHom h) . p by Th34;
then h . a in Roots ((PolyHom h) . p) by POLYNOM5:def 10;
hence o in { a where a is Element of R : h . a in Roots ((PolyHom h) . p) } ; :: thesis: verum