let n be Nat; :: thesis: for F being Field
for E being FieldExtension of F
for p being Polynomial of n,F
for q being Polynomial of n,E st p = q holds
Support q = Support p
let F be Field; :: thesis: for E being FieldExtension of F
for p being Polynomial of n,F
for q being Polynomial of n,E st p = q holds
Support q = Support p
let E be FieldExtension of F; :: thesis: for p being Polynomial of n,F
for q being Polynomial of n,E st p = q holds
Support q = Support p
let p be Polynomial of n,F; :: thesis: for q being Polynomial of n,E st p = q holds
Support q = Support p
let q be Polynomial of n,E; :: thesis: ( p = q implies Support q = Support p )
assume AS: p = q ; :: thesis: Support q = Support p
H1: F is Subring of E by FIELD_4:def 1;

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

let o be object ; :: thesis: ( o in Support p implies o in Support q )
assume A1: o in Support p ; :: thesis: o in Support q
then reconsider b = o as Element of Bags n ;
p . b <> 0. F by A1, POLYNOM1:def 4;
then p . b <> 0. E by H1, C0SP1:def 3;
hence o in Support q by AS, POLYNOM1:def 4; :: thesis: verum

end;

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

let o be object ; :: thesis: ( o in Support q implies o in Support p )
assume A1: o in Support q ; :: thesis: o in Support p
then reconsider b = o as Element of Bags n ;
q . b <> 0. E by A1, POLYNOM1:def 4;
then q . b <> 0. F by H1, C0SP1:def 3;
hence o in Support p by AS, POLYNOM1:def 4; :: thesis: verum

end;

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