set cMGFC = the carrier of (MultGroup F_Complex);

set cPRFC = the carrier of (Polynom-Ring F_Complex);

let n, ni be non zero Element of NAT ; :: thesis: for f being FinSequence of the carrier of (Polynom-Ring F_Complex)

for s being finite Subset of F_Complex st s = { y where y is Element of (MultGroup F_Complex) : ( ord y divides n & not ord y divides ni & ord y <> n ) } & dom f = Seg n & ( for i being non zero Element of NAT st i in dom f holds

( ( ( not i divides n or i divides ni or i = n ) implies f . i = <%(1_ F_Complex)%> ) & ( i divides n & not i divides ni & i <> n implies f . i = cyclotomic_poly i ) ) ) holds

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

let f be FinSequence of the carrier of (Polynom-Ring F_Complex); :: thesis: for s being finite Subset of F_Complex st s = { y where y is Element of (MultGroup F_Complex) : ( ord y divides n & not ord y divides ni & ord y <> n ) } & dom f = Seg n & ( for i being non zero Element of NAT st i in dom f holds

( ( ( not i divides n or i divides ni or i = n ) implies f . i = <%(1_ F_Complex)%> ) & ( i divides n & not i divides ni & i <> n implies f . i = cyclotomic_poly i ) ) ) holds

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

let s be finite Subset of F_Complex; :: thesis: ( s = { y where y is Element of (MultGroup F_Complex) : ( ord y divides n & not ord y divides ni & ord y <> n ) } & dom f = Seg n & ( for i being non zero Element of NAT st i in dom f holds

( ( ( not i divides n or i divides ni or i = n ) implies f . i = <%(1_ F_Complex)%> ) & ( i divides n & not i divides ni & i <> n implies f . i = cyclotomic_poly i ) ) ) implies Product f = poly_with_roots ((s,1) -bag) )

assume that

A1: s = { y where y is Element of the carrier of (MultGroup F_Complex) : ( ord y divides n & not ord y divides ni & ord y <> n ) } and

A2: dom f = Seg n and

A3: for i being non zero Element of NAT st i in dom f holds

( ( ( not i divides n or i divides ni or i = n ) implies f . i = <%(1_ F_Complex)%> ) & ( i divides n & not i divides ni & i <> n implies f . i = cyclotomic_poly i ) ) ; :: thesis: Product f = poly_with_roots ((s,1) -bag)

deffunc H_{1}( Nat) -> set = { y where y is Element of the carrier of (MultGroup F_Complex) : ( y in s & ord y <= $1 ) } ;

_{1}(n) as finite Subset of F_Complex ;

A5: len f = n by A2, FINSEQ_1:def 3;

defpred S_{1}[ Nat, set ] means for fi being FinSequence of the carrier of (Polynom-Ring F_Complex) st fi = f | (Seg $1) holds

$2 = Product fi;

dom F = Seg (len f) and

A7: for i being Nat st i in Seg (len f) holds

S_{1}[i,F . i]
from FINSEQ_1:sch 5(A6);

defpred S_{2}[ Nat] means ex t being finite Subset of F_Complex st

( t = H_{1}($1) & F . $1 = poly_with_roots ((t,1) -bag) );

A8: for i being Element of NAT st 1 <= i & i < len f & S_{2}[i] holds

S_{2}[i + 1]

A48: 0 + 1 <= n by NAT_1:13;

A49: S_{2}[1]

S_{2}[i]
from INT_1:sch 7(A49, A8);

then ( f = f | (Seg (len f)) & ex S being finite Subset of F_Complex st

( S = H_{1}( len f) & F . (len f) = poly_with_roots ((S,1) -bag) ) )
by A5, A48, FINSEQ_3:49;

hence Product f = poly_with_roots ((s,1) -bag) by A5, A7, A47, FINSEQ_1:3; :: thesis: verum

set cPRFC = the carrier of (Polynom-Ring F_Complex);

let n, ni be non zero Element of NAT ; :: thesis: for f being FinSequence of the carrier of (Polynom-Ring F_Complex)

for s being finite Subset of F_Complex st s = { y where y is Element of (MultGroup F_Complex) : ( ord y divides n & not ord y divides ni & ord y <> n ) } & dom f = Seg n & ( for i being non zero Element of NAT st i in dom f holds

( ( ( not i divides n or i divides ni or i = n ) implies f . i = <%(1_ F_Complex)%> ) & ( i divides n & not i divides ni & i <> n implies f . i = cyclotomic_poly i ) ) ) holds

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

let f be FinSequence of the carrier of (Polynom-Ring F_Complex); :: thesis: for s being finite Subset of F_Complex st s = { y where y is Element of (MultGroup F_Complex) : ( ord y divides n & not ord y divides ni & ord y <> n ) } & dom f = Seg n & ( for i being non zero Element of NAT st i in dom f holds

( ( ( not i divides n or i divides ni or i = n ) implies f . i = <%(1_ F_Complex)%> ) & ( i divides n & not i divides ni & i <> n implies f . i = cyclotomic_poly i ) ) ) holds

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

let s be finite Subset of F_Complex; :: thesis: ( s = { y where y is Element of (MultGroup F_Complex) : ( ord y divides n & not ord y divides ni & ord y <> n ) } & dom f = Seg n & ( for i being non zero Element of NAT st i in dom f holds

( ( ( not i divides n or i divides ni or i = n ) implies f . i = <%(1_ F_Complex)%> ) & ( i divides n & not i divides ni & i <> n implies f . i = cyclotomic_poly i ) ) ) implies Product f = poly_with_roots ((s,1) -bag) )

assume that

A1: s = { y where y is Element of the carrier of (MultGroup F_Complex) : ( ord y divides n & not ord y divides ni & ord y <> n ) } and

A2: dom f = Seg n and

A3: for i being non zero Element of NAT st i in dom f holds

( ( ( not i divides n or i divides ni or i = n ) implies f . i = <%(1_ F_Complex)%> ) & ( i divides n & not i divides ni & i <> n implies f . i = cyclotomic_poly i ) ) ; :: thesis: Product f = poly_with_roots ((s,1) -bag)

deffunc H

A4: now :: thesis: for i being Element of NAT holds H_{1}(i) is finite Subset of F_Complex

then reconsider sB = Hlet i be Element of NAT ; :: thesis: H_{1}(i) is finite Subset of F_Complex

H_{1}(i) c= s
_{1}(i) is finite Subset of F_Complex
by XBOOLE_1:1; :: thesis: verum

end;H

proof

hence
H
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in H_{1}(i) or x in s )

assume x in H_{1}(i)
; :: thesis: x in s

then ex y being Element of the carrier of (MultGroup F_Complex) st

( x = y & y in s & ord y <= i ) ;

hence x in s ; :: thesis: verum

end;assume x in H

then ex y being Element of the carrier of (MultGroup F_Complex) st

( x = y & y in s & ord y <= i ) ;

hence x in s ; :: thesis: verum

A5: len f = n by A2, FINSEQ_1:def 3;

defpred S

$2 = Product fi;

A6: now :: thesis: for i being Nat st i in Seg (len f) holds

ex x being Element of the carrier of (Polynom-Ring F_Complex) st S_{1}[i,x]

consider F being FinSequence of the carrier of (Polynom-Ring F_Complex) such that ex x being Element of the carrier of (Polynom-Ring F_Complex) st S

let i be Nat; :: thesis: ( i in Seg (len f) implies ex x being Element of the carrier of (Polynom-Ring F_Complex) st S_{1}[i,x] )

assume i in Seg (len f) ; :: thesis: ex x being Element of the carrier of (Polynom-Ring F_Complex) st S_{1}[i,x]

reconsider fi = f | (Seg i) as FinSequence of the carrier of (Polynom-Ring F_Complex) by FINSEQ_1:18;

set x = Product fi;

take x = Product fi; :: thesis: S_{1}[i,x]

thus S_{1}[i,x]
; :: thesis: verum

end;assume i in Seg (len f) ; :: thesis: ex x being Element of the carrier of (Polynom-Ring F_Complex) st S

reconsider fi = f | (Seg i) as FinSequence of the carrier of (Polynom-Ring F_Complex) by FINSEQ_1:18;

set x = Product fi;

take x = Product fi; :: thesis: S

thus S

dom F = Seg (len f) and

A7: for i being Nat st i in Seg (len f) holds

S

defpred S

( t = H

A8: for i being Element of NAT st 1 <= i & i < len f & S

S

proof

let i be Element of NAT ; :: thesis: ( 1 <= i & i < len f & S_{2}[i] implies S_{2}[i + 1] )

assume that

A9: 1 <= i and

A10: i < len f and

A11: S_{2}[i]
; :: thesis: S_{2}[i + 1]

reconsider fi = f | (Seg i) as FinSequence of the carrier of (Polynom-Ring F_Complex) by FINSEQ_1:18;

i in Seg (len f) by A9, A10, FINSEQ_1:1;

then A12: F . i = Product fi by A7;

reconsider fi1 = f | (Seg (i + 1)) as FinSequence of the carrier of (Polynom-Ring F_Complex) by FINSEQ_1:18;

A13: i + 1 <= len f by A10, NAT_1:13;

then i + 1 = min ((i + 1),(len f)) by XXREAL_0:def 9;

then A14: len fi1 = i + 1 by FINSEQ_2:21;

i + 1 in NAT by ORDINAL1:def 12;

then reconsider sB = H_{1}(i + 1) as finite Subset of F_Complex by A4;

take sB ; :: thesis: ( sB = H_{1}(i + 1) & F . (i + 1) = poly_with_roots ((sB,1) -bag) )

thus sB = H_{1}(i + 1)
; :: thesis: F . (i + 1) = poly_with_roots ((sB,1) -bag)

set B = (sB,1) -bag ;

consider sb being finite Subset of F_Complex such that

A15: sb = H_{1}(i)
and

A16: F . i = poly_with_roots ((sb,1) -bag) by A11;

1 <= i + 1 by A9, NAT_1:13;

then A17: i + 1 in Seg (len f) by A13, FINSEQ_1:1;

then A18: i + 1 in dom f by FINSEQ_1:def 3;

A19: (f | (Seg (i + 1))) . (i + 1) = f . (i + 1) by FINSEQ_1:4, FUNCT_1:49;

then reconsider fi1d1 = fi1 . (i + 1) as Element of the carrier of (Polynom-Ring F_Complex) by A18, FINSEQ_2:11;

reconsider fi1d1p = fi1d1 as Polynomial of F_Complex by POLYNOM3:def 10;

A20: F . (i + 1) = Product fi1 by A7, A17;

set b = (sb,1) -bag ;

fi = fi1 | (Seg i) by Lm2, NAT_1:12;

then fi1 = fi ^ <*fi1d1*> by A14, FINSEQ_3:55;

then Product fi1 = (Product fi) * fi1d1 by GROUP_4:6;

then A21: Product fi1 = (poly_with_roots ((sb,1) -bag)) *' fi1d1p by A12, A16, POLYNOM3:def 10;

end;assume that

A9: 1 <= i and

A10: i < len f and

A11: S

reconsider fi = f | (Seg i) as FinSequence of the carrier of (Polynom-Ring F_Complex) by FINSEQ_1:18;

i in Seg (len f) by A9, A10, FINSEQ_1:1;

then A12: F . i = Product fi by A7;

reconsider fi1 = f | (Seg (i + 1)) as FinSequence of the carrier of (Polynom-Ring F_Complex) by FINSEQ_1:18;

A13: i + 1 <= len f by A10, NAT_1:13;

then i + 1 = min ((i + 1),(len f)) by XXREAL_0:def 9;

then A14: len fi1 = i + 1 by FINSEQ_2:21;

i + 1 in NAT by ORDINAL1:def 12;

then reconsider sB = H

take sB ; :: thesis: ( sB = H

thus sB = H

set B = (sB,1) -bag ;

consider sb being finite Subset of F_Complex such that

A15: sb = H

A16: F . i = poly_with_roots ((sb,1) -bag) by A11;

1 <= i + 1 by A9, NAT_1:13;

then A17: i + 1 in Seg (len f) by A13, FINSEQ_1:1;

then A18: i + 1 in dom f by FINSEQ_1:def 3;

A19: (f | (Seg (i + 1))) . (i + 1) = f . (i + 1) by FINSEQ_1:4, FUNCT_1:49;

then reconsider fi1d1 = fi1 . (i + 1) as Element of the carrier of (Polynom-Ring F_Complex) by A18, FINSEQ_2:11;

reconsider fi1d1p = fi1d1 as Polynomial of F_Complex by POLYNOM3:def 10;

A20: F . (i + 1) = Product fi1 by A7, A17;

set b = (sb,1) -bag ;

fi = fi1 | (Seg i) by Lm2, NAT_1:12;

then fi1 = fi ^ <*fi1d1*> by A14, FINSEQ_3:55;

then Product fi1 = (Product fi) * fi1d1 by GROUP_4:6;

then A21: Product fi1 = (poly_with_roots ((sb,1) -bag)) *' fi1d1p by A12, A16, POLYNOM3:def 10;

per cases
( not i + 1 divides n or i + 1 divides ni or i + 1 = n or ( i + 1 divides n & not i + 1 divides ni & i + 1 <> n ) )
;

end;

suppose A22:
( not i + 1 divides n or i + 1 divides ni or i + 1 = n )
; :: thesis: F . (i + 1) = poly_with_roots ((sB,1) -bag)

then F . (i + 1) = poly_with_roots ((sb,1) -bag) by A20, A19, A21, UPROOTS:32

.= poly_with_roots ((sB,1) -bag) by A23, TARSKI:2 ;

hence F . (i + 1) = poly_with_roots ((sB,1) -bag) ; :: thesis: verum

end;

A23: now :: thesis: for x being object holds

( ( x in sB implies x in sb ) & ( x in sb implies x in sB ) )

f . (i + 1) = <%(1_ F_Complex)%>
by A3, A18, A22;( ( x in sB implies x in sb ) & ( x in sb implies x in sB ) )

let x be object ; :: thesis: ( ( x in sB implies x in sb ) & ( x in sb implies x in sB ) )

then consider y being Element of (MultGroup F_Complex) such that

A27: ( x = y & y in s ) and

A28: ord y <= i by A15;

ord y <= i + 1 by A28, NAT_1:12;

hence x in sB by A27; :: thesis: verum

end;hereby :: thesis: ( x in sb implies x in sB )

assume
x in sb
; :: thesis: x in sBassume
x in sB
; :: thesis: x in sb

then consider y being Element of (MultGroup F_Complex) such that

A24: x = y and

A25: y in s and

A26: ord y <= i + 1 ;

ex y1 being Element of the carrier of (MultGroup F_Complex) st

( y = y1 & ord y1 divides n & not ord y1 divides ni & ord y1 <> n ) by A1, A25;

then ord y < i + 1 by A22, A26, XXREAL_0:1;

then ord y <= i by NAT_1:13;

hence x in sb by A15, A24, A25; :: thesis: verum

end;then consider y being Element of (MultGroup F_Complex) such that

A24: x = y and

A25: y in s and

A26: ord y <= i + 1 ;

ex y1 being Element of the carrier of (MultGroup F_Complex) st

( y = y1 & ord y1 divides n & not ord y1 divides ni & ord y1 <> n ) by A1, A25;

then ord y < i + 1 by A22, A26, XXREAL_0:1;

then ord y <= i by NAT_1:13;

hence x in sb by A15, A24, A25; :: thesis: verum

then consider y being Element of (MultGroup F_Complex) such that

A27: ( x = y & y in s ) and

A28: ord y <= i by A15;

ord y <= i + 1 by A28, NAT_1:12;

hence x in sB by A27; :: thesis: verum

then F . (i + 1) = poly_with_roots ((sb,1) -bag) by A20, A19, A21, UPROOTS:32

.= poly_with_roots ((sB,1) -bag) by A23, TARSKI:2 ;

hence F . (i + 1) = poly_with_roots ((sB,1) -bag) ; :: thesis: verum

suppose A29:
( i + 1 divides n & not i + 1 divides ni & i + 1 <> n )
; :: thesis: F . (i + 1) = poly_with_roots ((sB,1) -bag)

consider scb being non empty finite Subset of F_Complex such that

A30: scb = { y where y is Element of the carrier of (MultGroup F_Complex) : ord y = i + 1 } and

A31: cyclotomic_poly (i + 1) = poly_with_roots ((scb,1) -bag) by Def5;

set cb = (scb,1) -bag ;

A41: sb misses scb

then F . (i + 1) = (poly_with_roots ((sb,1) -bag)) *' (poly_with_roots ((scb,1) -bag)) by A7, A17, A19, A21

.= poly_with_roots (((sb,1) -bag) + ((scb,1) -bag)) by UPROOTS:64

.= poly_with_roots ((sB,1) -bag) by A40, A41, UPROOTS:10 ;

hence F . (i + 1) = poly_with_roots ((sB,1) -bag) ; :: thesis: verum

end;A30: scb = { y where y is Element of the carrier of (MultGroup F_Complex) : ord y = i + 1 } and

A31: cyclotomic_poly (i + 1) = poly_with_roots ((scb,1) -bag) by Def5;

now :: thesis: for x being object holds

( ( x in sB implies x in sb \/ scb ) & ( x in sb \/ scb implies x in sB ) )

then A40:
sB = sb \/ scb
by TARSKI:2;( ( x in sB implies x in sb \/ scb ) & ( x in sb \/ scb implies x in sB ) )

let x be object ; :: thesis: ( ( x in sB implies x in sb \/ scb ) & ( x in sb \/ scb implies b_{1} in sB ) )

_{1} in sB

end;hereby :: thesis: ( x in sb \/ scb implies b_{1} in sB )

assume A35:
x in sb \/ scb
; :: thesis: bassume
x in sB
; :: thesis: x in sb \/ scb

then consider y being Element of the carrier of (MultGroup F_Complex) such that

A32: x = y and

A33: y in s and

A34: ord y <= i + 1 ;

( ord y <= i or ord y = i + 1 ) by A34, NAT_1:8;

then ( y in sb or y in scb ) by A15, A30, A33;

hence x in sb \/ scb by A32, XBOOLE_0:def 3; :: thesis: verum

end;then consider y being Element of the carrier of (MultGroup F_Complex) such that

A32: x = y and

A33: y in s and

A34: ord y <= i + 1 ;

( ord y <= i or ord y = i + 1 ) by A34, NAT_1:8;

then ( y in sb or y in scb ) by A15, A30, A33;

hence x in sb \/ scb by A32, XBOOLE_0:def 3; :: thesis: verum

per cases
( x in sb or x in scb )
by A35, XBOOLE_0:def 3;

end;

set cb = (scb,1) -bag ;

A41: sb misses scb

proof

f . (i + 1) = poly_with_roots ((scb,1) -bag)
by A3, A18, A29, A31;
assume
sb /\ scb <> {}
; :: according to XBOOLE_0:def 7 :: thesis: contradiction

then consider x being object such that

A42: x in sb /\ scb by XBOOLE_0:def 1;

x in scb by A42, XBOOLE_0:def 4;

then A43: ex y2 being Element of the carrier of (MultGroup F_Complex) st

( x = y2 & ord y2 = i + 1 ) by A30;

x in sb by A42, XBOOLE_0:def 4;

then ex y1 being Element of the carrier of (MultGroup F_Complex) st

( x = y1 & y1 in s & ord y1 <= i ) by A15;

hence contradiction by A43, NAT_1:13; :: thesis: verum

end;then consider x being object such that

A42: x in sb /\ scb by XBOOLE_0:def 1;

x in scb by A42, XBOOLE_0:def 4;

then A43: ex y2 being Element of the carrier of (MultGroup F_Complex) st

( x = y2 & ord y2 = i + 1 ) by A30;

x in sb by A42, XBOOLE_0:def 4;

then ex y1 being Element of the carrier of (MultGroup F_Complex) st

( x = y1 & y1 in s & ord y1 <= i ) by A15;

hence contradiction by A43, NAT_1:13; :: thesis: verum

then F . (i + 1) = (poly_with_roots ((sb,1) -bag)) *' (poly_with_roots ((scb,1) -bag)) by A7, A17, A19, A21

.= poly_with_roots (((sb,1) -bag) + ((scb,1) -bag)) by UPROOTS:64

.= poly_with_roots ((sB,1) -bag) by A40, A41, UPROOTS:10 ;

hence F . (i + 1) = poly_with_roots ((sB,1) -bag) ; :: thesis: verum

now :: thesis: for x being object holds

( ( x in s implies x in sB ) & ( x in sB implies x in s ) )

then A47:
s = sB
by TARSKI:2;( ( x in s implies x in sB ) & ( x in sB implies x in s ) )

let x be object ; :: thesis: ( ( x in s implies x in sB ) & ( x in sB implies x in s ) )

then ex y being Element of (MultGroup F_Complex) st

( y = x & y in s & ord y <= n ) ;

hence x in s ; :: thesis: verum

end;hereby :: thesis: ( x in sB implies x in s )

assume
x in sB
; :: thesis: x in sassume A44:
x in s
; :: thesis: x in sB

then consider y being Element of (MultGroup F_Complex) such that

A45: x = y and

A46: ord y divides n and

not ord y divides ni and

ord y <> n by A1;

ord y <= n by A46, NAT_D:7;

hence x in sB by A44, A45; :: thesis: verum

end;then consider y being Element of (MultGroup F_Complex) such that

A45: x = y and

A46: ord y divides n and

not ord y divides ni and

ord y <> n by A1;

ord y <= n by A46, NAT_D:7;

hence x in sB by A44, A45; :: thesis: verum

then ex y being Element of (MultGroup F_Complex) st

( y = x & y in s & ord y <= n ) ;

hence x in s ; :: thesis: verum

A48: 0 + 1 <= n by NAT_1:13;

A49: S

proof

for i being Element of NAT st 1 <= i & i <= len f holds
reconsider t = H_{1}(1) as finite Subset of F_Complex by A4;

take t ; :: thesis: ( t = H_{1}(1) & F . 1 = poly_with_roots ((t,1) -bag) )

thus t = H_{1}(1)
; :: thesis: F . 1 = poly_with_roots ((t,1) -bag)

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

A50: 1 in dom f by A5, A48, FINSEQ_3:25;

A51: 1 divides ni by NAT_D:6;

A59: 1 in Seg (len f) by A5, A48, FINSEQ_1:1;

then 1 in dom f by FINSEQ_1:def 3;

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

f1 = <*(f . 1)*> by A5, A48, Th1;

then F . 1 = Product <*fd1*> by A7, A59

.= fd1 by FINSOP_1:11

.= <%(1_ F_Complex)%> by A3, A50, A51 ;

hence F . 1 = poly_with_roots ((t,1) -bag) by A58, UPROOTS:60; :: thesis: verum

end;take t ; :: thesis: ( t = H

thus t = H

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

A50: 1 in dom f by A5, A48, FINSEQ_3:25;

A51: 1 divides ni by NAT_D:6;

now :: thesis: t is empty

then A58:
(t,1) -bag = EmptyBag the carrier of F_Complex
by UPROOTS:9;assume
not t is empty
; :: thesis: contradiction

then consider x being object such that

A52: x in t ;

consider y being Element of the carrier of (MultGroup F_Complex) such that

x = y and

A53: y in s and

A54: ord y <= 1 by A52;

consider y1 being Element of the carrier of (MultGroup F_Complex) such that

A55: y = y1 and

A56: ord y1 divides n and

A57: not ord y1 divides ni and

ord y1 <> n by A1, A53;

hence contradiction by A51, A54, A55, A57, XXREAL_0:1; :: thesis: verum

end;then consider x being object such that

A52: x in t ;

consider y being Element of the carrier of (MultGroup F_Complex) such that

x = y and

A53: y in s and

A54: ord y <= 1 by A52;

consider y1 being Element of the carrier of (MultGroup F_Complex) such that

A55: y = y1 and

A56: ord y1 divides n and

A57: not ord y1 divides ni and

ord y1 <> n by A1, A53;

now :: thesis: not ord y1 = 0

then
0 + 1 <= ord y1
by NAT_1:13;assume
ord y1 = 0
; :: thesis: contradiction

then ex u being Nat st n = 0 * u by A56, NAT_D:def 3;

hence contradiction ; :: thesis: verum

end;then ex u being Nat st n = 0 * u by A56, NAT_D:def 3;

hence contradiction ; :: thesis: verum

hence contradiction by A51, A54, A55, A57, XXREAL_0:1; :: thesis: verum

A59: 1 in Seg (len f) by A5, A48, FINSEQ_1:1;

then 1 in dom f by FINSEQ_1:def 3;

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

f1 = <*(f . 1)*> by A5, A48, Th1;

then F . 1 = Product <*fd1*> by A7, A59

.= fd1 by FINSOP_1:11

.= <%(1_ F_Complex)%> by A3, A50, A51 ;

hence F . 1 = poly_with_roots ((t,1) -bag) by A58, UPROOTS:60; :: thesis: verum

S

then ( f = f | (Seg (len f)) & ex S being finite Subset of F_Complex st

( S = H

hence Product f = poly_with_roots ((s,1) -bag) by A5, A7, A47, FINSEQ_1:3; :: thesis: verum