let R be Ring; :: thesis: for S being R -homomorphic R -isomorphic Ring
for h being Isomorphism of R,S
for p being Element of the carrier of (Polynom-Ring R) holds Roots ((PolyHom h) . p) = { (h . a) where a is Element of R : a in Roots p }
let S be R -homomorphic R -isomorphic Ring; :: thesis: for h being Isomorphism of R,S
for p being Element of the carrier of (Polynom-Ring R) holds Roots ((PolyHom h) . p) = { (h . a) where a is Element of R : a in Roots p }
let h be Isomorphism of R,S; :: thesis: for p being Element of the carrier of (Polynom-Ring R) holds Roots ((PolyHom h) . p) = { (h . a) where a is Element of R : a in Roots p }
let p be Element of the carrier of (Polynom-Ring R); :: thesis: Roots ((PolyHom h) . p) = { (h . a) where a is Element of R : a in Roots p }

A1: now :: thesis: for o being object st o in Roots ((PolyHom h) . p) holds
o in { (h . a) where a is Element of R : a in Roots p }

let o be object ; :: thesis: ( o in Roots ((PolyHom h) . p) implies o in { (h . a) where a is Element of R : a in Roots p } )
assume A2: o in Roots ((PolyHom h) . p) ; :: thesis: o in { (h . a) where a is Element of R : a in Roots p }
then reconsider b = o as Element of S ;
b is_a_root_of (PolyHom h) . p by A2, POLYNOM5:def 10;
then consider a being Element of R such that
A3: ( a is_a_root_of p & h . a = b ) by Th36;
a in Roots p by A3, POLYNOM5:def 10;
hence o in { (h . a) where a is Element of R : a in Roots p } by A3; :: thesis: verum

end;

now :: thesis: for o being object st o in { (h . a) where a is Element of R : a in Roots p } holds
o in Roots ((PolyHom h) . p)

let o be object ; :: thesis: ( o in { (h . a) where a is Element of R : a in Roots p } implies o in Roots ((PolyHom h) . p) )
assume o in { (h . a) where a is Element of R : a in Roots p } ; :: thesis: o in Roots ((PolyHom h) . p)
then consider a being Element of R such that
A4: ( o = h . a & a in Roots p ) ;
a is_a_root_of p by A4, POLYNOM5:def 10;
then h . a is_a_root_of (PolyHom h) . p by Th36;
hence o in Roots ((PolyHom h) . p) by A4, POLYNOM5:def 10; :: thesis: verum

end;

hence Roots ((PolyHom h) . p) = { (h . a) where a is Element of R : a in Roots p } by A1, TARSKI:2; :: thesis: verum