let f be Field-yielding ascending sequence ; :: thesis: for p being Polynomial of (SeqField f) ex i being Element of NAT st p is Polynomial of (f . i)
let p be Polynomial of (SeqField f); :: thesis: ex i being Element of NAT st p is Polynomial of (f . i)
consider i being Element of NAT such that
H: Coeff p c= the carrier of (f . i) by alg3a;
take i ; :: thesis: p is Polynomial of (f . i)
f . i is Subfield of SeqField f by Fsub;
then SeqField f is FieldExtension of f . i by FIELD_4:7;
hence p is Polynomial of (f . i) by H, FIELD_7:11; :: thesis: verum