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 a being Element of E 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 a being Element of E 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 a being Element of E holds multiplicity (q,a) = multiplicity (p,a)
let q be non zero Polynomial of E; :: thesis: ( q = p implies for a being Element of E holds multiplicity (q,a) = multiplicity (p,a) )
assume AS: q = p ; :: thesis: for a being Element of E holds multiplicity (q,a) = multiplicity (p,a)
let a be Element of E; :: thesis: multiplicity (q,a) = multiplicity (p,a)
reconsider K = E as E -extending FieldExtension of F by FIELD_4:6;
multiplicity (q,(@ (a,K))) = multiplicity (p,(@ (a,K))) by AS, sepsep
.= multiplicity (p,a) by multi3K ;
hence multiplicity (q,a) = multiplicity (p,a) by multi3; :: thesis: verum