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 ;

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

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

i + j in F
by A1, A16;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;

end;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;

end;

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;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

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;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

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