let F be Field; :: thesis: for p being non zero Polynomial of F
for E being FieldExtension of F
for q being non zero Polynomial of E st q = p holds
for K being b₂ -extending FieldExtension of F
for a being Element of K holds multiplicity (q,a) = multiplicity (p,a)
let p be non zero Polynomial of F; :: thesis: for E being FieldExtension of F
for q being non zero Polynomial of E st q = p holds
for K being b₁ -extending FieldExtension of F
for a being Element of K holds multiplicity (q,a) = multiplicity (p,a)
let E be FieldExtension of F; :: thesis: for q being non zero Polynomial of E st q = p holds
for K being E -extending FieldExtension of F
for a being Element of K holds multiplicity (q,a) = multiplicity (p,a)
let q be non zero Polynomial of E; :: thesis: ( q = p implies for K being E -extending FieldExtension of F
for a being Element of K holds multiplicity (q,a) = multiplicity (p,a) )
assume AS: q = p ; :: thesis: for K being E -extending FieldExtension of F
for a being Element of K holds multiplicity (q,a) = multiplicity (p,a)
let K be E -extending FieldExtension of F; :: thesis: for a being Element of K holds multiplicity (q,a) = multiplicity (p,a)
let a be Element of K; :: thesis: multiplicity (q,a) = multiplicity (p,a)
reconsider r = q as Polynomial of K by FIELD_4:8;
q <> 0_. E ;
then r <> 0_. K by FIELD_4:12;
then reconsider r = r as non zero Polynomial of K by UPROOTS:def 5;
thus multiplicity (q,a) = multiplicity (r,a) by FIELD_14:def 6
.= multiplicity (p,a) by AS, FIELD_14:def 6 ; :: thesis: verum