let L be domRing; :: thesis: for x being Element of L
for p, q being non-zero Polynomial of L holds multiplicity ((p *' q),x) = (multiplicity (p,x)) + (multiplicity (q,x))
let x be Element of L; :: thesis: for p, q being non-zero Polynomial of L holds multiplicity ((p *' q),x) = (multiplicity (p,x)) + (multiplicity (q,x))
let p, q be non-zero Polynomial of L; :: thesis: multiplicity ((p *' q),x) = (multiplicity (p,x)) + (multiplicity (q,x))
set r = <%(- x),(1. L)%>;
consider F being non empty finite Subset of NAT such that
A1: F = { k where k is Element of NAT : ex pqq being Polynomial of L st p *' q = (<%(- x),(1. L)%> `^ k) *' pqq } and
A2: multiplicity ((p *' q),x) = max F by Def7;
consider f being non empty finite Subset of NAT such that
A3: f = { k where k is Element of NAT : ex pq being Polynomial of L st p = (<%(- x),(1. L)%> `^ k) *' pq } and
A4: multiplicity (p,x) = max f by Def7;
max f in f by XXREAL_2:def 8;
then consider i being Element of NAT such that
A5: i = max f and
A6: ex pq being Polynomial of L st p = (<%(- x),(1. L)%> `^ i) *' pq by A3;
consider pq being Polynomial of L such that
A7: p = (<%(- x),(1. L)%> `^ i) *' pq by A6;
consider g being non empty finite Subset of NAT such that
A8: g = { k where k is Element of NAT : ex qq being Polynomial of L st q = (<%(- x),(1. L)%> `^ k) *' qq } and
A9: multiplicity (q,x) = max g by Def7;
max F in F by XXREAL_2:def 8;
then consider k being Element of NAT such that
A10: k = max F and
A11: ex pqq being Polynomial of L st p *' q = (<%(- x),(1. L)%> `^ k) *' pqq by A1;
consider pqq being Polynomial of L such that
A12: p *' q = (<%(- x),(1. L)%> `^ k) *' pqq by A11;
max g in g by XXREAL_2:def 8;
then consider j being Element of NAT such that
A13: j = max g and
A14: ex qq being Polynomial of L st q = (<%(- x),(1. L)%> `^ j) *' qq by A8;
consider qq being Polynomial of L such that
A15: q = (<%(- x),(1. L)%> `^ j) *' qq by A14;
A16: p *' q = (((<%(- x),(1. L)%> `^ i) *' pq) *' (<%(- x),(1. L)%> `^ j)) *' qq by A7, A15, POLYNOM3:33
.= (((<%(- x),(1. L)%> `^ i) *' (<%(- x),(1. L)%> `^ j)) *' pq) *' qq by POLYNOM3:33
.= ((<%(- x),(1. L)%> `^ (i + j)) *' pq) *' qq by Th27
.= (<%(- x),(1. L)%> `^ (i + j)) *' (pq *' qq) by POLYNOM3:33 ;

A17: now :: thesis: not i + j < k

assume i + j < k ; :: thesis: contradiction
then 0 + (i + j) < k ;
then A18: 0 < k - (i + j) by XREAL_1:20;
then reconsider kij = k - (i + j) as Element of NAT by INT_1:3;
consider kk being Nat such that
A19: kij = kk + 1 by A18, NAT_1:6;
reconsider kk = kk as Element of NAT by ORDINAL1:def 12;
<%(- x),(1. L)%> `^ kij = (<%(- x),(1. L)%> `^ 1) *' (<%(- x),(1. L)%> `^ kk) by A19, Th27
.= <%(- x),(1. L)%> *' (<%(- x),(1. L)%> `^ kk) by POLYNOM5:16 ;
then A20: (<%(- x),(1. L)%> `^ kij) *' pqq = <%(- x),(1. L)%> *' ((<%(- x),(1. L)%> `^ kk) *' pqq) by POLYNOM3:33;
( (0_. L) . 1 = 0. L & <%(- x),(1. L)%> . 1 = 1. L ) by FUNCOP_1:7, POLYNOM5:38;
then A21: <%(- x),(1. L)%> `^ (i + j) <> 0_. L by Th26;
k = kij + (i + j) ;
then p *' q = ((<%(- x),(1. L)%> `^ (i + j)) *' (<%(- x),(1. L)%> `^ kij)) *' pqq by A12, Th27
.= (<%(- x),(1. L)%> `^ (i + j)) *' ((<%(- x),(1. L)%> `^ kij) *' pqq) by POLYNOM3:33 ;
then x is_a_root_of pq *' qq by A16, A21, A20, Th25, Th46;
then x in Roots (pq *' qq) by POLYNOM5:def 10;
then A22: x in (Roots pq) \/ (Roots qq) by Th20;

per cases ( x in Roots pq or x in Roots qq ) by A22, XBOOLE_0:def 3;

suppose x in Roots pq ; :: thesis: contradiction

then x is_a_root_of pq by POLYNOM5:def 10;
then pq = <%(- x),(1. L)%> *' (poly_quotient (pq,x)) by Th47;
then p = ((<%(- x),(1. L)%> `^ i) *' <%(- x),(1. L)%>) *' (poly_quotient (pq,x)) by A7, POLYNOM3:33
.= ((<%(- x),(1. L)%> `^ i) *' (<%(- x),(1. L)%> `^ 1)) *' (poly_quotient (pq,x)) by POLYNOM5:16
.= (<%(- x),(1. L)%> `^ (i + 1)) *' (poly_quotient (pq,x)) by Th27 ;
then i + 1 in f by A3;
then i + 1 <= i by A5, XXREAL_2:def 8;
hence contradiction by NAT_1:13; :: thesis: verum

end;

suppose x in Roots qq ; :: thesis: contradiction

then x is_a_root_of qq by POLYNOM5:def 10;
then qq = <%(- x),(1. L)%> *' (poly_quotient (qq,x)) by Th47;
then q = ((<%(- x),(1. L)%> `^ j) *' <%(- x),(1. L)%>) *' (poly_quotient (qq,x)) by A15, POLYNOM3:33
.= ((<%(- x),(1. L)%> `^ j) *' (<%(- x),(1. L)%> `^ 1)) *' (poly_quotient (qq,x)) by POLYNOM5:16
.= (<%(- x),(1. L)%> `^ (j + 1)) *' (poly_quotient (qq,x)) by Th27 ;
then j + 1 in g by A8;
then j + 1 <= j by A13, XXREAL_2:def 8;
hence contradiction by NAT_1:13; :: thesis: verum

end;

end;

end;

i + j in F by A1, A16;
then i + j <= k by A10, XXREAL_2:def 8;
hence multiplicity ((p *' q),x) = (multiplicity (p,x)) + (multiplicity (q,x)) by A2, A4, A9, A10, A5, A13, A17, XXREAL_0:1; :: thesis: verum