let F be Field; :: thesis: for E being FieldExtension of F
for p being Polynomial of E st Coeff p c= the carrier of F holds
p is Polynomial of F
let E be FieldExtension of F; :: thesis: for p being Polynomial of E st Coeff p c= the carrier of F holds
p is Polynomial of F
let p be Polynomial of E; :: thesis: ( Coeff p c= the carrier of F implies p is Polynomial of F )
assume AS: Coeff p c= the carrier of F ; :: thesis: p is Polynomial of F
F is Subring of E by FIELD_4:def 1;
then A: 0. E = 0. F by C0SP1:def 3;

now :: thesis: for y being object st y in rng p holds
y in the carrier of F

let y be object ; :: thesis: ( y in rng p implies b₁ in the carrier of F )
assume y in rng p ; :: thesis: b₁ in the carrier of F
then consider x being object such that
A1: ( x in dom p & y = p . x ) by FUNCT_1:def 3;
reconsider x = x as Element of NAT by A1;

per cases ( p . x = 0. F or p . x <> 0. F ) ;

suppose p . x = 0. F ; :: thesis: b₁ in the carrier of F

hence y in the carrier of F by A1; :: thesis: verum

end;

suppose p . x <> 0. F ; :: thesis: b₁ in the carrier of F

then y in Coeff p by A, A1;
hence y in the carrier of F by AS; :: thesis: verum

end;

end;

end;

then rng p c= the carrier of F ;
then reconsider q = p as sequence of the carrier of F by FUNCT_2:6;
consider n being Nat such that
C: for i being Nat st i >= n holds
p . i = 0. E by ALGSEQ_1:def 1;
for i being Nat st i >= n holds
q . i = 0. F by C, A;
hence p is Polynomial of F by ALGSEQ_1:def 1; :: thesis: verum