let F be Field; :: thesis: for p being non zero Polynomial of F
for E being FieldExtension of F
for K being b₂ -extending FieldExtension of F
for a being Element of E holds multiplicity (p,a) = multiplicity (p,(@ (a,K)))
let p be non zero Polynomial of F; :: thesis: for E being FieldExtension of F
for K being b₁ -extending FieldExtension of F
for a being Element of E holds multiplicity (p,a) = multiplicity (p,(@ (a,K)))
let E be FieldExtension of F; :: thesis: for K being E -extending FieldExtension of F
for a being Element of E holds multiplicity (p,a) = multiplicity (p,(@ (a,K)))
let K be E -extending FieldExtension of F; :: thesis: for a being Element of E holds multiplicity (p,a) = multiplicity (p,(@ (a,K)))
let a be Element of E; :: thesis: multiplicity (p,a) = multiplicity (p,(@ (a,K)))
consider pE being non zero Polynomial of E such that
A: ( pE = p & multiplicity (p,a) = multiplicity (pE,a) ) by FIELD_14:def 6;
reconsider K1 = K as FieldExtension of E ;
E is Subfield of K1 by FIELD_4:7;
then the carrier of E c= the carrier of K1 by EC_PF_1:def 1;
then reconsider a1 = a as Element of K1 ;
consider pK being non zero Polynomial of K1 such that
B: ( pK = pE & multiplicity (pE,a1) = multiplicity (pK,a1) ) by FIELD_14:def 6;
C: @ (a,K) = a1 by FIELD_7:def 4;
thus multiplicity (p,a) = multiplicity (p,(@ (a,K))) by A, B, C, multi3, FIELD_14:def 6; :: thesis: verum