let L be comRing; :: thesis: for s being non empty finite Subset of L

for f being FinSequence of (Polynom-Ring L) st len f = card s & ( for i being Element of NAT

for c being Element of L st i in dom f & c = (canFS s) . i holds

f . i = <%(- c),(1. L)%> ) holds

poly_with_roots ((s,1) -bag) = Product f

set cL = the carrier of L;

set cPRL = the carrier of (Polynom-Ring L);

let s be non empty finite Subset of the carrier of L; :: thesis: for f being FinSequence of (Polynom-Ring L) st len f = card s & ( for i being Element of NAT

for c being Element of L st i in dom f & c = (canFS s) . i holds

f . i = <%(- c),(1. L)%> ) holds

poly_with_roots ((s,1) -bag) = Product f

let f be FinSequence of the carrier of (Polynom-Ring L); :: thesis: ( len f = card s & ( for i being Element of NAT

for c being Element of L st i in dom f & c = (canFS s) . i holds

f . i = <%(- c),(1. L)%> ) implies poly_with_roots ((s,1) -bag) = Product f )

assume that

A1: len f = card s and

A2: for i being Element of NAT

for c being Element of the carrier of L st i in dom f & c = (canFS s) . i holds

f . i = <%(- c),(1. L)%> ; :: thesis: poly_with_roots ((s,1) -bag) = Product f

set cs = canFS s;

A3: rng (canFS s) = s by FUNCT_2:def 3;

defpred S_{1}[ Nat] means ex t being finite Subset of the carrier of L ex g being FinSequence of the carrier of (Polynom-Ring L) st

( t = rng ((canFS s) | (Seg $1)) & g = f | (Seg $1) & poly_with_roots ((t,1) -bag) = Product g );

A4: len (canFS s) = card s by FINSEQ_1:93;

then A5: dom f = dom (canFS s) by A1, FINSEQ_3:29;

A6: for j being Element of NAT st 1 <= j & j < len f & S_{1}[j] holds

S_{1}[j + 1]

then A27: ( (canFS s) | (Seg (len f)) is FinSequence & f | (Seg (len f)) = f ) by FINSEQ_1:18, FINSEQ_2:20;

A28: 0 + 1 <= len f by A1, NAT_1:13;

A29: S_{1}[1]

S_{1}[i]
from INT_1:sch 7(A29, A6);

then ex t being finite Subset of the carrier of L ex g being FinSequence of the carrier of (Polynom-Ring L) st

( t = rng ((canFS s) | (Seg (len f))) & g = f | (Seg (len f)) & poly_with_roots ((t,1) -bag) = Product g ) by A28;

hence poly_with_roots ((s,1) -bag) = Product f by A1, A4, A27, A3, FINSEQ_2:20; :: thesis: verum

for f being FinSequence of (Polynom-Ring L) st len f = card s & ( for i being Element of NAT

for c being Element of L st i in dom f & c = (canFS s) . i holds

f . i = <%(- c),(1. L)%> ) holds

poly_with_roots ((s,1) -bag) = Product f

set cL = the carrier of L;

set cPRL = the carrier of (Polynom-Ring L);

let s be non empty finite Subset of the carrier of L; :: thesis: for f being FinSequence of (Polynom-Ring L) st len f = card s & ( for i being Element of NAT

for c being Element of L st i in dom f & c = (canFS s) . i holds

f . i = <%(- c),(1. L)%> ) holds

poly_with_roots ((s,1) -bag) = Product f

let f be FinSequence of the carrier of (Polynom-Ring L); :: thesis: ( len f = card s & ( for i being Element of NAT

for c being Element of L st i in dom f & c = (canFS s) . i holds

f . i = <%(- c),(1. L)%> ) implies poly_with_roots ((s,1) -bag) = Product f )

assume that

A1: len f = card s and

A2: for i being Element of NAT

for c being Element of the carrier of L st i in dom f & c = (canFS s) . i holds

f . i = <%(- c),(1. L)%> ; :: thesis: poly_with_roots ((s,1) -bag) = Product f

set cs = canFS s;

A3: rng (canFS s) = s by FUNCT_2:def 3;

defpred S

( t = rng ((canFS s) | (Seg $1)) & g = f | (Seg $1) & poly_with_roots ((t,1) -bag) = Product g );

A4: len (canFS s) = card s by FINSEQ_1:93;

then A5: dom f = dom (canFS s) by A1, FINSEQ_3:29;

A6: for j being Element of NAT st 1 <= j & j < len f & S

S

proof

f | (Seg (len f)) is FinSequence
by FINSEQ_1:18;
let j be Element of NAT ; :: thesis: ( 1 <= j & j < len f & S_{1}[j] implies S_{1}[j + 1] )

assume that

A7: 1 <= j and

A8: j < len f ; :: thesis: ( not S_{1}[j] or S_{1}[j + 1] )

reconsider g1 = f | (Seg (j + 1)) as FinSequence of the carrier of (Polynom-Ring L) by FINSEQ_1:18;

A9: j + 1 <= len f by A8, NAT_1:13;

then ex l being Nat st len f = (j + 1) + l by NAT_1:10;

then A10: len g1 = j + 1 by FINSEQ_3:53;

1 <= j + 1 by A7, NAT_1:13;

then A11: j + 1 in dom (canFS s) by A1, A4, A9, FINSEQ_3:25;

then (canFS s) . (j + 1) in s by FINSEQ_2:11;

then reconsider csj1 = (canFS s) . (j + 1) as Element of the carrier of L ;

A12: g1 . (j + 1) = f . (j + 1) by FINSEQ_1:4, FUNCT_1:49

.= <%(- csj1),(1. L)%> by A2, A5, A11 ;

reconsider csja1 = (canFS s) | (Seg (j + 1)) as FinSequence of s by FINSEQ_1:18;

reconsider csja = (canFS s) | (Seg j) as FinSequence of s by FINSEQ_1:18;

given t being finite Subset of the carrier of L, g being FinSequence of the carrier of (Polynom-Ring L) such that A13: t = rng ((canFS s) | (Seg j)) and

A14: g = f | (Seg j) and

A15: poly_with_roots ((t,1) -bag) = Product g ; :: thesis: S_{1}[j + 1]

j <= j + 1 by NAT_1:12;

then Seg j c= Seg (j + 1) by FINSEQ_1:5;

then g = g1 | (Seg j) by A14, RELAT_1:74;

then A16: g1 = g ^ <*<%(- csj1),(1. L)%>*> by A10, A12, FINSEQ_3:55;

reconsider pt = poly_with_roots ((t,1) -bag) as Polynomial of L ;

set t1 = rng csja1;

Seg (j + 1) = (Seg j) \/ {(j + 1)} by FINSEQ_1:9;

then A17: csja1 = csja \/ ((canFS s) | {(j + 1)}) by RELAT_1:78;

(canFS s) | {(j + 1)} = (j + 1) .--> csj1 by A11, FUNCT_7:6;

then rng ((canFS s) | {(j + 1)}) = {csj1} by FUNCOP_1:8;

then A18: rng csja1 = t \/ {csj1} by A13, A17, RELAT_1:12;

reconsider epj1 = <%(- csj1),(1. L)%> as Element of the carrier of (Polynom-Ring L) by POLYNOM3:def 10;

reconsider pj1 = poly_with_roots (({csj1},1) -bag) as Polynomial of L ;

A19: pj1 = epj1 by Th58;

reconsider t1 = rng csja1 as finite Subset of the carrier of L by A18;

take t1 ; :: thesis: ex g being FinSequence of the carrier of (Polynom-Ring L) st

( t1 = rng ((canFS s) | (Seg (j + 1))) & g = f | (Seg (j + 1)) & poly_with_roots ((t1,1) -bag) = Product g )

take g1 ; :: thesis: ( t1 = rng ((canFS s) | (Seg (j + 1))) & g1 = f | (Seg (j + 1)) & poly_with_roots ((t1,1) -bag) = Product g1 )

thus ( t1 = rng ((canFS s) | (Seg (j + 1))) & g1 = f | (Seg (j + 1)) ) ; :: thesis: poly_with_roots ((t1,1) -bag) = Product g1

t misses {csj1}

hence poly_with_roots ((t1,1) -bag) = pt *' pj1 by Th61

.= (Product g) * epj1 by A15, A19, POLYNOM3:def 10

.= Product g1 by A16, GROUP_4:6 ;

:: thesis: verum

end;assume that

A7: 1 <= j and

A8: j < len f ; :: thesis: ( not S

reconsider g1 = f | (Seg (j + 1)) as FinSequence of the carrier of (Polynom-Ring L) by FINSEQ_1:18;

A9: j + 1 <= len f by A8, NAT_1:13;

then ex l being Nat st len f = (j + 1) + l by NAT_1:10;

then A10: len g1 = j + 1 by FINSEQ_3:53;

1 <= j + 1 by A7, NAT_1:13;

then A11: j + 1 in dom (canFS s) by A1, A4, A9, FINSEQ_3:25;

then (canFS s) . (j + 1) in s by FINSEQ_2:11;

then reconsider csj1 = (canFS s) . (j + 1) as Element of the carrier of L ;

A12: g1 . (j + 1) = f . (j + 1) by FINSEQ_1:4, FUNCT_1:49

.= <%(- csj1),(1. L)%> by A2, A5, A11 ;

reconsider csja1 = (canFS s) | (Seg (j + 1)) as FinSequence of s by FINSEQ_1:18;

reconsider csja = (canFS s) | (Seg j) as FinSequence of s by FINSEQ_1:18;

given t being finite Subset of the carrier of L, g being FinSequence of the carrier of (Polynom-Ring L) such that A13: t = rng ((canFS s) | (Seg j)) and

A14: g = f | (Seg j) and

A15: poly_with_roots ((t,1) -bag) = Product g ; :: thesis: S

j <= j + 1 by NAT_1:12;

then Seg j c= Seg (j + 1) by FINSEQ_1:5;

then g = g1 | (Seg j) by A14, RELAT_1:74;

then A16: g1 = g ^ <*<%(- csj1),(1. L)%>*> by A10, A12, FINSEQ_3:55;

reconsider pt = poly_with_roots ((t,1) -bag) as Polynomial of L ;

set t1 = rng csja1;

Seg (j + 1) = (Seg j) \/ {(j + 1)} by FINSEQ_1:9;

then A17: csja1 = csja \/ ((canFS s) | {(j + 1)}) by RELAT_1:78;

(canFS s) | {(j + 1)} = (j + 1) .--> csj1 by A11, FUNCT_7:6;

then rng ((canFS s) | {(j + 1)}) = {csj1} by FUNCOP_1:8;

then A18: rng csja1 = t \/ {csj1} by A13, A17, RELAT_1:12;

reconsider epj1 = <%(- csj1),(1. L)%> as Element of the carrier of (Polynom-Ring L) by POLYNOM3:def 10;

reconsider pj1 = poly_with_roots (({csj1},1) -bag) as Polynomial of L ;

A19: pj1 = epj1 by Th58;

reconsider t1 = rng csja1 as finite Subset of the carrier of L by A18;

take t1 ; :: thesis: ex g being FinSequence of the carrier of (Polynom-Ring L) st

( t1 = rng ((canFS s) | (Seg (j + 1))) & g = f | (Seg (j + 1)) & poly_with_roots ((t1,1) -bag) = Product g )

take g1 ; :: thesis: ( t1 = rng ((canFS s) | (Seg (j + 1))) & g1 = f | (Seg (j + 1)) & poly_with_roots ((t1,1) -bag) = Product g1 )

thus ( t1 = rng ((canFS s) | (Seg (j + 1))) & g1 = f | (Seg (j + 1)) ) ; :: thesis: poly_with_roots ((t1,1) -bag) = Product g1

t misses {csj1}

proof

then
(t1,1) -bag = ((t,1) -bag) + (({csj1},1) -bag)
by A18, Th7;
assume
not t misses {csj1}
; :: thesis: contradiction

then t /\ {csj1} <> {} by XBOOLE_0:def 7;

then consider x being object such that

A20: x in t /\ {csj1} by XBOOLE_0:def 1;

x in {csj1} by A20, XBOOLE_0:def 4;

then A21: x = csj1 by TARSKI:def 1;

x in t by A20, XBOOLE_0:def 4;

then consider i being object such that

A22: i in dom ((canFS s) | (Seg j)) and

A23: x = ((canFS s) | (Seg j)) . i by A13, FUNCT_1:def 3;

A24: i in Seg j by A22, RELAT_1:57;

reconsider i = i as Element of NAT by A22;

A25: 1 <= i by A24, FINSEQ_1:1;

i <= j by A24, FINSEQ_1:1;

then A26: i < j + 1 by NAT_1:13;

x = (canFS s) . i by A22, A23, FUNCT_1:47;

hence contradiction by A1, A4, A3, A9, A21, A25, A26, GRAPH_5:7; :: thesis: verum

end;then t /\ {csj1} <> {} by XBOOLE_0:def 7;

then consider x being object such that

A20: x in t /\ {csj1} by XBOOLE_0:def 1;

x in {csj1} by A20, XBOOLE_0:def 4;

then A21: x = csj1 by TARSKI:def 1;

x in t by A20, XBOOLE_0:def 4;

then consider i being object such that

A22: i in dom ((canFS s) | (Seg j)) and

A23: x = ((canFS s) | (Seg j)) . i by A13, FUNCT_1:def 3;

A24: i in Seg j by A22, RELAT_1:57;

reconsider i = i as Element of NAT by A22;

A25: 1 <= i by A24, FINSEQ_1:1;

i <= j by A24, FINSEQ_1:1;

then A26: i < j + 1 by NAT_1:13;

x = (canFS s) . i by A22, A23, FUNCT_1:47;

hence contradiction by A1, A4, A3, A9, A21, A25, A26, GRAPH_5:7; :: thesis: verum

hence poly_with_roots ((t1,1) -bag) = pt *' pj1 by Th61

.= (Product g) * epj1 by A15, A19, POLYNOM3:def 10

.= Product g1 by A16, GROUP_4:6 ;

:: thesis: verum

then A27: ( (canFS s) | (Seg (len f)) is FinSequence & f | (Seg (len f)) = f ) by FINSEQ_1:18, FINSEQ_2:20;

A28: 0 + 1 <= len f by A1, NAT_1:13;

A29: S

proof

for i being Element of NAT st 1 <= i & i <= len f holds
1 in dom (canFS s)
by A1, A4, A28, FINSEQ_3:25;

then reconsider cs1 = (canFS s) . 1 as Element of s by FINSEQ_2:11;

reconsider g = f | (Seg 1) as FinSequence of the carrier of (Polynom-Ring L) by FINSEQ_1:18;

reconsider cs1a = (canFS s) | (Seg 1) as FinSequence of s by FINSEQ_1:18;

A30: cs1 in the carrier of L ;

A31: 1 in Seg 1 by FINSEQ_1:1;

then A32: cs1a . 1 = cs1 by FUNCT_1:49;

reconsider cs1 = (canFS s) . 1 as Element of the carrier of L by A30;

reconsider t = {cs1} as finite Subset of the carrier of L ;

take t ; :: thesis: ex g being FinSequence of the carrier of (Polynom-Ring L) st

( t = rng ((canFS s) | (Seg 1)) & g = f | (Seg 1) & poly_with_roots ((t,1) -bag) = Product g )

take g ; :: thesis: ( t = rng ((canFS s) | (Seg 1)) & g = f | (Seg 1) & poly_with_roots ((t,1) -bag) = Product g )

consider s1 being Element of s such that

A33: cs1a = <*s1*> by A1, A4, A28, TREES_9:34;

cs1a . 1 = s1 by A33, FINSEQ_1:40;

hence ( t = rng ((canFS s) | (Seg 1)) & g = f | (Seg 1) ) by A33, A32, FINSEQ_1:39; :: thesis: poly_with_roots ((t,1) -bag) = Product g

consider p1 being Element of the carrier of (Polynom-Ring L) such that

A34: g = <*p1*> by A28, TREES_9:34;

A35: ( g . 1 = p1 & Product g = p1 ) by A34, FINSEQ_1:40, FINSOP_1:11;

A36: 1 in dom f by A28, FINSEQ_3:25;

then reconsider f1 = f . 1 as Element of the carrier of (Polynom-Ring L) by FINSEQ_2:11;

A37: g . 1 = f1 by A31, FUNCT_1:49;

f1 = <%(- cs1),(1. L)%> by A2, A36;

hence poly_with_roots ((t,1) -bag) = Product g by A37, A35, Th58; :: thesis: verum

end;then reconsider cs1 = (canFS s) . 1 as Element of s by FINSEQ_2:11;

reconsider g = f | (Seg 1) as FinSequence of the carrier of (Polynom-Ring L) by FINSEQ_1:18;

reconsider cs1a = (canFS s) | (Seg 1) as FinSequence of s by FINSEQ_1:18;

A30: cs1 in the carrier of L ;

A31: 1 in Seg 1 by FINSEQ_1:1;

then A32: cs1a . 1 = cs1 by FUNCT_1:49;

reconsider cs1 = (canFS s) . 1 as Element of the carrier of L by A30;

reconsider t = {cs1} as finite Subset of the carrier of L ;

take t ; :: thesis: ex g being FinSequence of the carrier of (Polynom-Ring L) st

( t = rng ((canFS s) | (Seg 1)) & g = f | (Seg 1) & poly_with_roots ((t,1) -bag) = Product g )

take g ; :: thesis: ( t = rng ((canFS s) | (Seg 1)) & g = f | (Seg 1) & poly_with_roots ((t,1) -bag) = Product g )

consider s1 being Element of s such that

A33: cs1a = <*s1*> by A1, A4, A28, TREES_9:34;

cs1a . 1 = s1 by A33, FINSEQ_1:40;

hence ( t = rng ((canFS s) | (Seg 1)) & g = f | (Seg 1) ) by A33, A32, FINSEQ_1:39; :: thesis: poly_with_roots ((t,1) -bag) = Product g

consider p1 being Element of the carrier of (Polynom-Ring L) such that

A34: g = <*p1*> by A28, TREES_9:34;

A35: ( g . 1 = p1 & Product g = p1 ) by A34, FINSEQ_1:40, FINSOP_1:11;

A36: 1 in dom f by A28, FINSEQ_3:25;

then reconsider f1 = f . 1 as Element of the carrier of (Polynom-Ring L) by FINSEQ_2:11;

A37: g . 1 = f1 by A31, FUNCT_1:49;

f1 = <%(- cs1),(1. L)%> by A2, A36;

hence poly_with_roots ((t,1) -bag) = Product g by A37, A35, Th58; :: thesis: verum

S

then ex t being finite Subset of the carrier of L ex g being FinSequence of the carrier of (Polynom-Ring L) st

( t = rng ((canFS s) | (Seg (len f))) & g = f | (Seg (len f)) & poly_with_roots ((t,1) -bag) = Product g ) by A28;

hence poly_with_roots ((s,1) -bag) = Product f by A1, A4, A27, A3, FINSEQ_2:20; :: thesis: verum