let F be Field; :: thesis: for E being FieldExtension of F
for p, q being non zero Polynomial of F
for a being Element of E holds multiplicity ((p *' q),a) = (multiplicity (p,a)) + (multiplicity (q,a))
let E be FieldExtension of F; :: thesis: for p, q being non zero Polynomial of F
for a being Element of E holds multiplicity ((p *' q),a) = (multiplicity (p,a)) + (multiplicity (q,a))
let p, q be non zero Polynomial of F; :: thesis: for a being Element of E holds multiplicity ((p *' q),a) = (multiplicity (p,a)) + (multiplicity (q,a))
let a be Element of E; :: thesis: multiplicity ((p *' q),a) = (multiplicity (p,a)) + (multiplicity (q,a))
reconsider pE = p, qE = q as Polynomial of E by FIELD_4:8;
p <> 0_. F ;
then p <> 0_. E by FIELD_4:12;
then reconsider pE = pE as non zero Polynomial of E by UPROOTS:def 5;
q <> 0_. F ;
then q <> 0_. E by FIELD_4:12;
then reconsider qE = qE as non zero Polynomial of E by UPROOTS:def 5;
pE *' qE = p *' q by FIELD_4:17;
hence multiplicity ((p *' q),a) = multiplicity ((pE *' qE),a) by sepsep1
.= (multiplicity (pE,a)) + (multiplicity (qE,a)) by UPROOTS:55
.= (multiplicity (p,a)) + (multiplicity (qE,a)) by sepsep1
.= (multiplicity (p,a)) + (multiplicity (q,a)) by sepsep1 ;
:: thesis: verum