theorem alg3: :: FIELD_12:27

for f being Field-yielding ascending sequence
for p being Polynomial of (SeqField f) ex i being Element of NAT st p is Polynomial of (f . i)