let F be Field; :: thesis: for E being FieldExtension of F
for p being Element of the carrier of (Polynom-Ring F)
for q being Element of the carrier of (Polynom-Ring E) st q = p holds
Coeff q = Coeff p
let E be FieldExtension of F; :: thesis: for p being Element of the carrier of (Polynom-Ring F)
for q being Element of the carrier of (Polynom-Ring E) st q = p holds
Coeff q = Coeff p
let p be Element of the carrier of (Polynom-Ring F); :: thesis: for q being Element of the carrier of (Polynom-Ring E) st q = p holds
Coeff q = Coeff p
let q be Element of the carrier of (Polynom-Ring E); :: thesis: ( q = p implies Coeff q = Coeff p )
assume AS: q = p ; :: thesis: Coeff q = Coeff p
H: F is Subfield of E by FIELD_4:7;

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

let o be object ; :: thesis: ( o in Coeff q implies o in Coeff p )
assume o in Coeff q ; :: thesis: o in Coeff p
then o in { (q . i) where i is Element of NAT : q . i <> 0. E } by FIELD_7:def 3;
then consider i being Element of NAT such that
A1: ( o = q . i & q . i <> 0. E ) ;
( o = p . i & p . i <> 0. F ) by A1, AS, H, EC_PF_1:def 1;
then o in { (p . i) where i is Element of NAT : p . i <> 0. F } ;
hence o in Coeff p by FIELD_7:def 3; :: thesis: verum

end;

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

let o be object ; :: thesis: ( o in Coeff p implies o in Coeff q )
assume o in Coeff p ; :: thesis: o in Coeff q
then o in { (p . i) where i is Element of NAT : p . i <> 0. F } by FIELD_7:def 3;
then consider i being Element of NAT such that
A1: ( o = p . i & p . i <> 0. F ) ;
( o = q . i & q . i <> 0. E ) by A1, AS, H, EC_PF_1:def 1;
then o in { (q . i) where i is Element of NAT : q . i <> 0. E } ;
hence o in Coeff q by FIELD_7:def 3; :: thesis: verum

end;

hence Coeff q = Coeff p by A, TARSKI:2; :: thesis: verum