let f be Field-yielding ascending sequence ; :: thesis: for p being non constant Polynomial of (SeqField f) ex i being Element of NAT st p is non constant Polynomial of (f . i)
let p be non constant Polynomial of (SeqField f); :: thesis: ex i being Element of NAT st p is non constant Polynomial of (f . i)
consider i being Element of NAT such that
H: p is Polynomial of (f . i) by alg3;
reconsider p1 = p as Element of the carrier of (Polynom-Ring (f . i)) by H, POLYNOM3:def 10;
reconsider q = p as Element of the carrier of (Polynom-Ring (SeqField f)) by POLYNOM3:def 10;
f . i is Subfield of SeqField f by Fsub;
then SeqField f is FieldExtension of f . i by FIELD_4:7;
then deg p1 = deg q by FIELD_4:20;
then reconsider p1 = p1 as non constant Element of the carrier of (Polynom-Ring (f . i)) by RING_4:def 4, RATFUNC1:def 2;
reconsider q1 = p1 as Polynomial of (f . i) ;
H: deg q1 >= 0 ;
take i ; :: thesis: p is non constant Polynomial of (f . i)
thus p is non constant Polynomial of (f . i) by H, RING_4:def 4, RATFUNC1:def 2; :: thesis: verum