let F be Ring; :: thesis: for S being RingExtension of F
for p being Element of the carrier of (Polynom-Ring F)
for h being F -fixing Monomorphism of S
for a being Element of S holds
( a in Roots (S,p) iff h . a in Roots (S,p) )
let E be RingExtension of F; :: thesis: for p being Element of the carrier of (Polynom-Ring F)
for h being F -fixing Monomorphism of E
for a being Element of E holds
( a in Roots (E,p) iff h . a in Roots (E,p) )
let p be Element of the carrier of (Polynom-Ring F); :: thesis: for h being F -fixing Monomorphism of E
for a being Element of E holds
( a in Roots (E,p) iff h . a in Roots (E,p) )
let h be F -fixing Monomorphism of E; :: thesis: for a being Element of E holds
( a in Roots (E,p) iff h . a in Roots (E,p) )
let a be Element of E; :: thesis: ( a in Roots (E,p) iff h . a in Roots (E,p) )
h is monomorphism ;
then reconsider E1 = E as E -homomorphic E -monomorphic Ring by RING_2:def 4, RING_3:def 3;
reconsider h1 = h as Monomorphism of E,E1 ;
the carrier of (Polynom-Ring F) c= the carrier of (Polynom-Ring E) by FIELD_4:10;
then reconsider p1 = p as Element of the carrier of (Polynom-Ring E) ;

now :: thesis: for i being Element of NAT holds p . i = ((PolyHom h1) . p1) . i

let i be Element of NAT ; :: thesis: p . i = ((PolyHom h1) . p1) . i
thus p . i = h1 . (p . i) by deffix
.= ((PolyHom h1) . p1) . i by FIELD_1:def 2 ; :: thesis: verum

end;

then H: (PolyHom h1) . p1 = p1 ;

A: now :: thesis: ( a in Roots (E,p) implies h . a in Roots (E,p) )

assume a in Roots (E,p) ; :: thesis: h . a in Roots (E,p)
then a in Roots p1 by FIELD_7:13;
then a is_a_root_of p1 by POLYNOM5:def 10;
then h1 . a is_a_root_of (PolyHom h1) . p1 by FIELD_1:34;
then h . a in Roots p1 by H, POLYNOM5:def 10;
hence h . a in Roots (E,p) by FIELD_7:13; :: thesis: verum

end;

now :: thesis: ( h . a in Roots (E,p) implies a in Roots (E,p) )

assume h . a in Roots (E,p) ; :: thesis: a in Roots (E,p)
then A0: h . a in Roots ((PolyHom h1) . p1) by H, FIELD_7:13;
Roots p1 = { a where a is Element of E : h1 . a in Roots ((PolyHom h1) . p1) } by FIELD_1:37;
then a in Roots p1 by A0;
hence a in Roots (E,p) by FIELD_7:13; :: thesis: verum

end;

hence ( a in Roots (E,p) iff h . a in Roots (E,p) ) by A; :: thesis: verum