let F be Field; :: thesis: for E being FieldExtension of F
for p being Polynomial of F
for q being Polynomial of E st q = p holds
MonicDivisors p c= MonicDivisors q
let E be FieldExtension of F; :: thesis: for p being Polynomial of F
for q being Polynomial of E st q = p holds
MonicDivisors p c= MonicDivisors q
let p be Polynomial of F; :: thesis: for q being Polynomial of E st q = p holds
MonicDivisors p c= MonicDivisors q
let q be Polynomial of E; :: thesis: ( q = p implies MonicDivisors p c= MonicDivisors q )
assume AS: q = p ; :: thesis: MonicDivisors p c= MonicDivisors q

now :: thesis: for o being object st o in MonicDivisors p holds
o in MonicDivisors q

let o be object ; :: thesis: ( o in MonicDivisors p implies o in MonicDivisors q )
assume o in MonicDivisors p ; :: thesis: o in MonicDivisors q
then consider rp being monic Element of the carrier of (Polynom-Ring F) such that
A: ( o = rp & rp divides p ) ;
consider up being Polynomial of F such that
B: p = rp *' up by A, RING_4:1;
reconsider rq = rp as Polynomial of E by FIELD_4:8;
C: F is Subfield of E by FIELD_4:7;
LC rq = LC rp by FIELD_8:5
.= 1. F by RATFUNC1:def 7
.= 1. E by C, EC_PF_1:def 1 ;
then reconsider rq = rq as monic Element of the carrier of (Polynom-Ring E) by RATFUNC1:def 7, POLYNOM3:def 10;
reconsider uq = up as Polynomial of E by FIELD_4:8;
p = rq *' uq by B, FIELD_4:17;
then rq divides q by AS, RING_4:1;
hence o in MonicDivisors q by A; :: thesis: verum

end;

hence MonicDivisors p c= MonicDivisors q ; :: thesis: verum