let L be non empty right_complementable associative commutative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr ; :: thesis: for p being Polynomial of L
for z being Element of L st z is_a_root_of p holds
ex s being Polynomial of L st p = (rpoly 1,z) *' s
let p be Polynomial of L; :: thesis: for z being Element of L st z is_a_root_of p holds
ex s being Polynomial of L st p = (rpoly 1,z) *' s
let z be Element of L; :: thesis: ( z is_a_root_of p implies ex s being Polynomial of L st p = (rpoly 1,z) *' s )
assume A1: z is_a_root_of p ; :: thesis: ex s being Polynomial of L st p = (rpoly 1,z) *' s
set m = len p;

per cases ( len p = 0 or len p > 0 ) ;

suppose len p = 0 ; :: thesis: ex s being Polynomial of L st p = (rpoly 1,z) *' s

then A2: p = 0_. L by POLYNOM4:8;
take s = 0_. L; :: thesis: p = (rpoly 1,z) *' s
thus p = (rpoly 1,z) *' s by A2, POLYNOM3:35; :: thesis: verum

end;

suppose A3: len p > 0 ; :: thesis: ex s being Polynomial of L st p = (rpoly 1,z) *' s

then len p >= 0 + 1 by NAT_1:13;
then reconsider m1 = (len p) - 1 as Element of NAT by INT_1:18;
A4: m1 + 1 = len p ;

A5: now

assume m1 < 1 ; :: thesis: contradiction
then deg p = 0 by NAT_1:14;
then not p is with_roots by Th24;
hence contradiction by A1, POLYNOM5:def 7; :: thesis: verum

end;

defpred S₁[ set , set ] means ( ( $1 = 1 & $2 = (p . 1) * (1_. L) ) or ( $1 <> 1 & ex u being Element of L ex b being Element of NAT st
( u = p . $1 & b = $1 & $2 = u * (qpoly b,z) ) ) );
A6: for k being Nat st k in Seg m1 holds
ex x being Element of the carrier of (Polynom-Ring L) st S₁[k,x]

proof

let k be Nat; :: thesis: ( k in Seg m1 implies ex x being Element of the carrier of (Polynom-Ring L) st S₁[k,x] )
assume k in Seg m1 ; :: thesis: ex x being Element of the carrier of (Polynom-Ring L) st S₁[k,x]
then A7: ( 1 <= k & k <= m1 ) by FINSEQ_1:3;
A8: dom p = NAT by FUNCT_2:def 1;

per cases ( k = 1 or k > 1 ) by A7, XXREAL_0:1;

suppose A9: k = 1 ; :: thesis: ex x being Element of the carrier of (Polynom-Ring L) st S₁[k,x]

reconsider t = (p . 1) * (1_. L) as Element of the carrier of (Polynom-Ring L) by POLYNOM3:def 12;
take t ; :: thesis: S₁[k,t]
thus S₁[k,t] by A9; :: thesis: verum

end;

suppose A10: k > 1 ; :: thesis: ex x being Element of the carrier of (Polynom-Ring L) st S₁[k,x]

reconsider t = (p /. k) * (qpoly k,z) as Element of the carrier of (Polynom-Ring L) by POLYNOM3:def 12;
take t ; :: thesis: S₁[k,t]
S₁[k,t]

proof

ex u being Element of L ex b being Element of NAT st
( u = p . k & b = k & t = u * (qpoly b,z) )

proof

reconsider b = k as Element of NAT by ORDINAL1:def 13;
take p /. k ; :: thesis: ex b being Element of NAT st
( p /. k = p . k & b = k & t = (p /. k) * (qpoly b,z) )
take b ; :: thesis: ( p /. k = p . k & b = k & t = (p /. k) * (qpoly b,z) )
b in NAT ;
hence ( p /. k = p . k & b = k & t = (p /. k) * (qpoly b,z) ) by A8, PARTFUN1:def 8; :: thesis: verum

end;

hence S₁[k,t] by A10; :: thesis: verum

end;

hence S₁[k,t] ; :: thesis: verum

end;

end;

end;

consider hs being FinSequence of (Polynom-Ring L) such that
A11: ( dom hs = Seg m1 & ( for k being Nat st k in Seg m1 holds
S₁[k,hs . k] ) ) from FINSEQ_1:sch 5(A6);
A12: ( len hs = m1 & hs . 1 = (p . 1) * (1_. L) & ( for i being Element of NAT st 1 < i & i <= (len p) - 1 holds
hs . i = (p . i) * (qpoly i,z) ) )

proof

thus len hs = m1 by A11, FINSEQ_1:def 3; :: thesis: ( hs . 1 = (p . 1) * (1_. L) & ( for i being Element of NAT st 1 < i & i <= (len p) - 1 holds
hs . i = (p . i) * (qpoly i,z) ) )
1 in Seg m1 by A5;
hence hs . 1 = (p . 1) * (1_. L) by A11; :: thesis: for i being Element of NAT st 1 < i & i <= (len p) - 1 holds
hs . i = (p . i) * (qpoly i,z)

now

let i be Element of NAT ; :: thesis: ( 1 < i & i <= (len p) - 1 implies hs . i = (p . i) * (qpoly i,z) )
assume A13: ( 1 < i & i <= (len p) - 1 ) ; :: thesis: hs . i = (p . i) * (qpoly i,z)
then i in Seg m1 ;
then consider u being Element of L such that
A14: ex b being Element of NAT st
( u = p . i & b = i & hs . i = u * (qpoly b,z) ) by A11, A13;
consider b being Element of NAT such that
A15: ( u = p . i & b = i & hs . i = u * (qpoly b,z) ) by A14;
thus hs . i = (p . i) * (qpoly i,z) by A15; :: thesis: verum

end;

hence for i being Element of NAT st 1 < i & i <= (len p) - 1 holds
hs . i = (p . i) * (qpoly i,z) ; :: thesis: verum

end;

defpred S₂[ set , set ] means ex u being Element of L ex b being Element of NAT st
( u = p . $1 & b = $1 & $2 = u * (rpoly b,z) );
A16: for k being Nat st k in Seg m1 holds
ex x being Element of the carrier of (Polynom-Ring L) st S₂[k,x]

proof

let k be Nat; :: thesis: ( k in Seg m1 implies ex x being Element of the carrier of (Polynom-Ring L) st S₂[k,x] )
assume k in Seg m1 ; :: thesis: ex x being Element of the carrier of (Polynom-Ring L) st S₂[k,x]
then reconsider k1 = k as Element of NAT ;
reconsider t = (p /. k) * (rpoly k1,z) as Element of the carrier of (Polynom-Ring L) by POLYNOM3:def 12;
take t ; :: thesis: S₂[k,t]
take p /. k ; :: thesis: ex b being Element of NAT st
( p /. k = p . k & b = k & t = (p /. k) * (rpoly b,z) )
take k1 ; :: thesis: ( p /. k = p . k & k1 = k & t = (p /. k) * (rpoly k1,z) )
A17: dom p = NAT by FUNCT_2:def 1;
k1 in NAT ;
hence ( p /. k = p . k & k1 = k & t = (p /. k) * (rpoly k1,z) ) by A17, PARTFUN1:def 8; :: thesis: verum

end;

consider h being FinSequence of (Polynom-Ring L) such that
A18: ( dom h = Seg m1 & ( for k being Nat st k in Seg m1 holds
S₂[k,h . k] ) ) from FINSEQ_1:sch 5(A16);
A19: ( len h = m1 & ( for i being Element of NAT st 1 <= i & i <= m1 holds
h . i = (p . i) * (rpoly i,z) ) )

proof

thus len h = m1 by A18, FINSEQ_1:def 3; :: thesis: for i being Element of NAT st 1 <= i & i <= m1 holds
h . i = (p . i) * (rpoly i,z)

now

let k be Element of NAT ; :: thesis: ( 1 <= k & k <= m1 implies h . k = (p . k) * (rpoly k,z) )
assume ( 1 <= k & k <= m1 ) ; :: thesis: h . k = (p . k) * (rpoly k,z)
then k in Seg m1 ;
then consider u being Element of L such that
A20: ex b being Element of NAT st
( u = p . k & b = k & h . k = u * (rpoly b,z) ) by A18;
consider b being Element of NAT such that
A21: ( u = p . k & b = k & h . k = u * (rpoly b,z) ) by A20;
thus h . k = (p . k) * (rpoly k,z) by A21; :: thesis: verum

end;

hence for i being Element of NAT st 1 <= i & i <= m1 holds
h . i = (p . i) * (rpoly i,z) ; :: thesis: verum

end;

set s = Sum hs;
set rs = Sum h;
reconsider s = Sum hs, rs = Sum h as Polynomial of L by POLYNOM3:def 12;
take s ; :: thesis: p = (rpoly 1,z) *' s
A22: (rpoly 1,z) *' s = rs

proof

A23: dom ((rpoly 1,z) *' s) = NAT by FUNCT_2:def 1
.= dom rs by FUNCT_2:def 1 ;

now

let i' be set ; :: thesis: ( i' in dom rs implies rs . i' = ((rpoly 1,z) *' s) . i' )
assume i' in dom rs ; :: thesis: rs . i' = ((rpoly 1,z) *' s) . i'
reconsider r1z = rpoly 1,z as Element of (Polynom-Ring L) by POLYNOM3:def 12;
A24: dom (r1z * hs) = dom h by A11, A18, POLYNOM1:def 2;

now

let k be Nat; :: thesis: ( k in dom h implies (r1z * hs) . b₁ = h . b₁ )
assume A25: k in dom h ; :: thesis: (r1z * hs) . b₁ = h . b₁
then k in Seg m1 by A19, FINSEQ_1:def 3;
then A26: ( 1 <= k & k <= m1 ) by FINSEQ_1:3;

per cases ( k = 1 or k > 1 ) by A26, XXREAL_0:1;

suppose A27: k = 1 ; :: thesis: (r1z * hs) . b₁ = h . b₁

then A28: hs /. k = (p . 1) * (1_. L) by A11, A12, A18, A25, PARTFUN1:def 8;
thus (r1z * hs) . k = (r1z * hs) /. k by A24, A25, PARTFUN1:def 8
.= r1z * (hs /. k) by A11, A18, A25, POLYNOM1:def 2
.= (rpoly 1,z) *' ((p . 1) * (1_. L)) by A28, POLYNOM3:def 12
.= (p . 1) * ((rpoly 1,z) *' (1_. L)) by Th19
.= (p . 1) * (rpoly 1,z) by POLYNOM3:36
.= h . k by A19, A26, A27 ; :: thesis: verum

end;

suppose A29: k > 1 ; :: thesis: (r1z * hs) . b₁ = h . b₁

reconsider k1 = k as Element of NAT by A25;
A30: hs /. k = hs . k by A11, A18, A25, PARTFUN1:def 8
.= (p . k1) * (qpoly k1,z) by A12, A26, A29 ;
thus (r1z * hs) . k = (r1z * hs) /. k by A24, A25, PARTFUN1:def 8
.= r1z * (hs /. k) by A11, A18, A25, POLYNOM1:def 2
.= (rpoly 1,z) *' ((p . k1) * (qpoly k1,z)) by A30, POLYNOM3:def 12
.= (p . k1) * ((rpoly 1,z) *' (qpoly k1,z)) by Th19
.= (p . k1) * (rpoly k1,z) by A29, Th32
.= h . k by A19, A26 ; :: thesis: verum

end;

end;

end;

then r1z * hs = h by A24, FINSEQ_1:17;
hence rs . i' = ((rpoly 1,z) *' s) . i' by Lm6; :: thesis: verum

end;

hence (rpoly 1,z) *' s = rs by A23, FUNCT_1:9; :: thesis: verum

end;

A31: now

let i be Element of NAT ; :: thesis: ( i > 0 & i < len p implies rs . i = ((p . i) * (rpoly i,z)) . i )
assume A32: ( i > 0 & i < len p ) ; :: thesis: rs . i = ((p . i) * (rpoly i,z)) . i
then i + 1 > 0 + 1 by XREAL_1:10;
then A33: i >= 1 by NAT_1:13;
i < m1 + 1 by A32;
then A34: i <= m1 by NAT_1:13;
then A35: i in Seg (len h) by A19, A33;
set co = Coeff h,i;
A36: dom h = Seg (len h) by FINSEQ_1:def 3
.= Seg (len (Coeff h,i)) by Def1
.= dom (Coeff h,i) by FINSEQ_1:def 3 ;
then A37: i in dom (Coeff h,i) by A35, FINSEQ_1:def 3;

now

let i' be Element of NAT ; :: thesis: ( i' in dom (Coeff h,i) & i' <> i implies (Coeff h,i) /. i' = 0. L )
assume A38: ( i' in dom (Coeff h,i) & i' <> i ) ; :: thesis: (Coeff h,i) /. i' = 0. L
then consider ci being Polynomial of L such that
A39: ( ci = h . i' & (Coeff h,i) . i' = ci . i ) by Def1;
i' in Seg m1 by A19, A36, A38, FINSEQ_1:def 3;
then ( 1 <= i' & i' <= (len p) - 1 ) by FINSEQ_1:3;
then (Coeff h,i) . i' = ((p . i') * (rpoly i',z)) . i by A19, A39
.= (p . i') * ((rpoly i',z) . i) by POLYNOM5:def 3
.= (p . i') * (0. L) by A32, A38, Lm12
.= 0. L by VECTSP_1:36 ;
hence (Coeff h,i) /. i' = 0. L by A38, PARTFUN1:def 8; :: thesis: verum

end;

then A40: Sum (Coeff h,i) = (Coeff h,i) /. i by A37, POLYNOM2:5
.= (Coeff h,i) . i by A37, PARTFUN1:def 8 ;
consider cc being Polynomial of L such that
A41: ( cc = h . i & (Coeff h,i) . i = cc . i ) by A37, Def1;
h . i = (p . i) * (rpoly i,z) by A19, A33, A34;
hence rs . i = ((p . i) * (rpoly i,z)) . i by A40, A41, Th13; :: thesis: verum

end;

A42: now

let i be Element of NAT ; :: thesis: ( i >= len p implies rs . i = 0. L )
assume A43: i >= len p ; :: thesis: rs . i = 0. L
set co = Coeff h,i;
A44: dom h = Seg (len h) by FINSEQ_1:def 3
.= Seg (len (Coeff h,i)) by Def1
.= dom (Coeff h,i) by FINSEQ_1:def 3 ;

now

let j be Element of NAT ; :: thesis: ( j in dom (Coeff h,i) implies (Coeff h,i) . j = 0. L )
assume A45: j in dom (Coeff h,i) ; :: thesis: (Coeff h,i) . j = 0. L
then consider ci being Polynomial of L such that
A46: ( ci = h . j & (Coeff h,i) . j = ci . i ) by Def1;
j in Seg m1 by A19, A44, A45, FINSEQ_1:def 3;
then A47: ( 1 <= j & j <= m1 ) by FINSEQ_1:3;
then A48: j <> i by A4, A43, NAT_1:16, XXREAL_0:2;
thus (Coeff h,i) . j = ((p . j) * (rpoly j,z)) . i by A19, A46, A47
.= (p . j) * ((rpoly j,z) . i) by POLYNOM5:def 3
.= (p . j) * (0. L) by A3, A43, A48, Lm12
.= 0. L by VECTSP_1:36 ; :: thesis: verum

end;

then Sum (Coeff h,i) = 0. L by POLYNOM3:1;
hence rs . i = 0. L by Th13; :: thesis: verum

end;

rs = p

proof

A49: dom p = NAT by FUNCT_2:def 1
.= dom rs by FUNCT_2:def 1 ;

now

let i' be set ; :: thesis: ( i' in dom p implies p . b₁ = rs . b₁ )
assume i' in dom p ; :: thesis: p . b₁ = rs . b₁
then reconsider i = i' as Element of NAT ;

per cases ( i = 0 or i > 0 ) ;

suppose A50: i = 0 ; :: thesis: p . b₁ = rs . b₁

consider evp being FinSequence of L such that
A51: ( eval p,z = Sum evp & len evp = len p & ( for n being Element of NAT st n in dom evp holds
evp . n = (p . (n -' 1)) * ((power L) . z,(n -' 1)) ) ) by POLYNOM4:def 2;
A52: Sum evp = 0. L by A1, A51, POLYNOM5:def 6;
set co = Coeff h,0 ;
A53: dom h = Seg (len h) by FINSEQ_1:def 3
.= Seg (len (Coeff h,0 )) by Def1
.= dom (Coeff h,0 ) by FINSEQ_1:def 3 ;

A54: now

let j be Element of NAT ; :: thesis: ( j in dom (Coeff h,0 ) implies (Coeff h,0 ) . j = - ((p . j) * ((power L) . z,j)) )
assume A55: j in dom (Coeff h,0 ) ; :: thesis: (Coeff h,0 ) . j = - ((p . j) * ((power L) . z,j))
then consider ci being Polynomial of L such that
A56: ( ci = h . j & (Coeff h,0 ) . j = ci . i ) by A50, Def1;
reconsider aj = - ((power L) . z,j) as Element of L ;
j in Seg m1 by A19, A53, A55, FINSEQ_1:def 3;
then A57: ( 1 <= j & j <= m1 ) by FINSEQ_1:3;
hence (Coeff h,0 ) . j = ((p . j) * (rpoly j,z)) . i by A19, A56
.= (p . j) * ((rpoly j,z) . i) by POLYNOM5:def 3
.= (p . j) * aj by A50, A57, Lm11
.= - ((p . j) * ((power L) . z,j)) by VECTSP_1:40 ;
:: thesis: verum

end;

set cop = <*(- (p . 0 ))*> ^ (Coeff h,0 );
A58: len (<*(- (p . 0 ))*> ^ (Coeff h,0 )) = (len <*(- (p . 0 ))*>) + (len (Coeff h,0 )) by FINSEQ_1:35
.= 1 + (len (Coeff h,0 )) by FINSEQ_1:56 ;
then A59: len (<*(- (p . 0 ))*> ^ (Coeff h,0 )) = 1 + (len h) by Def1
.= len evp by A19, A51 ;
then A60: dom (<*(- (p . 0 ))*> ^ (Coeff h,0 )) = Seg (len evp) by FINSEQ_1:def 3
.= dom evp by FINSEQ_1:def 3 ;

now

let j be Element of NAT ; :: thesis: ( j in dom (<*(- (p . 0 ))*> ^ (Coeff h,0 )) implies (<*(- (p . 0 ))*> ^ (Coeff h,0 )) /. b₁ = - (evp /. b₁) )
assume A61: j in dom (<*(- (p . 0 ))*> ^ (Coeff h,0 )) ; :: thesis: (<*(- (p . 0 ))*> ^ (Coeff h,0 )) /. b₁ = - (evp /. b₁)
then A62: j in Seg (len (<*(- (p . 0 ))*> ^ (Coeff h,0 ))) by FINSEQ_1:def 3;
then A63: ( 1 <= j & j <= len (<*(- (p . 0 ))*> ^ (Coeff h,0 )) ) by FINSEQ_1:3;
A64: dom <*(- (p . 0 ))*> = {1} by FINSEQ_1:4, FINSEQ_1:55;
A65: evp /. j = evp . j by A60, A61, PARTFUN1:def 8
.= (p . (j -' 1)) * ((power L) . z,(j -' 1)) by A51, A60, A61 ;

per cases ( j = 1 or j > 1 ) by A63, XXREAL_0:1;

suppose A66: j = 1 ; :: thesis: (<*(- (p . 0 ))*> ^ (Coeff h,0 )) /. b₁ = - (evp /. b₁)

then j in dom <*(- (p . 0 ))*> by A64, TARSKI:def 1;
then A67: (<*(- (p . 0 ))*> ^ (Coeff h,0 )) . j = <*(- (p . 0 ))*> . j by FINSEQ_1:def 7
.= - (p . 0 ) by A66, FINSEQ_1:57 ;
j -' 1 = 1 - 1 by A66, XREAL_0:def 2;
then evp /. j = (p . 0 ) * (1_ L) by A65, GROUP_1:def 8
.= p . 0 by VECTSP_1:def 13 ;
hence (<*(- (p . 0 ))*> ^ (Coeff h,0 )) /. j = - (evp /. j) by A61, A67, PARTFUN1:def 8; :: thesis: verum

end;

suppose A68: j > 1 ; :: thesis: (<*(- (p . 0 ))*> ^ (Coeff h,0 )) /. b₁ = - (evp /. b₁)

then reconsider j1 = j - 1 as Element of NAT by INT_1:18;
1 < j1 + 1 by A68;
then A69: 1 <= j1 by NAT_1:13;
j1 <= (len (<*(- (p . 0 ))*> ^ (Coeff h,0 ))) - 1 by A63, XREAL_1:11;
then j1 in Seg (len (Coeff h,0 )) by A58, A69;
then A70: j1 in dom (Coeff h,0 ) by FINSEQ_1:def 3;
( len <*(- (p . 0 ))*> < j & j <= len (<*(- (p . 0 ))*> ^ (Coeff h,0 )) ) by A62, A68, FINSEQ_1:3, FINSEQ_1:57;
then A71: (<*(- (p . 0 ))*> ^ (Coeff h,0 )) . j = (Coeff h,0 ) . (j - (len <*(- (p . 0 ))*>)) by FINSEQ_1:37
.= (Coeff h,0 ) . (j - 1) by FINSEQ_1:57
.= - ((p . j1) * ((power L) . z,j1)) by A54, A70 ;
j - 1 >= 1 - 1 by A68, XREAL_1:11;
then j -' 1 = j - 1 by XREAL_0:def 2;
hence (<*(- (p . 0 ))*> ^ (Coeff h,0 )) /. j = - (evp /. j) by A61, A65, A71, PARTFUN1:def 8; :: thesis: verum

end;

end;

end;

then - (Sum evp) = Sum (<*(- (p . 0 ))*> ^ (Coeff h,0 )) by A59, Th7
.= (Sum <*(- (p . 0 ))*>) + (Sum (Coeff h,0 )) by RLVECT_1:58
.= (- (p . 0 )) + (Sum (Coeff h,0 )) by RLVECT_1:61 ;
then 0. L = (- (p . 0 )) + (Sum (Coeff h,0 )) by A52, RLVECT_1:25;
then p . 0 = (p . 0 ) + ((- (p . 0 )) + (Sum (Coeff h,0 ))) by ALGSTR_1:def 5
.= ((p . 0 ) + (- (p . 0 ))) + (Sum (Coeff h,0 )) by RLVECT_1:def 6
.= (0. L) + (Sum (Coeff h,0 )) by RLVECT_1:16
.= Sum (Coeff h,0 ) by ALGSTR_1:def 5 ;
hence p . i' = rs . i' by A50, Th13; :: thesis: verum

end;

suppose A72: i > 0 ; :: thesis: rs . b₁ = p . b₁

per cases ( i >= len p or i < len p ) ;

suppose A73: i >= len p ; :: thesis: rs . b₁ = p . b₁

hence rs . i' = 0. L by A42
.= p . i' by A73, ALGSEQ_1:22 ;
:: thesis: verum

end;

suppose i < len p ; :: thesis: rs . b₁ = p . b₁

hence rs . i' = ((p . i) * (rpoly i,z)) . i by A31, A72
.= (p . i) * ((rpoly i,z) . i) by POLYNOM5:def 3
.= (p . i) * (1_ L) by A72, Lm11
.= p . i' by VECTSP_1:def 13 ;
:: thesis: verum

end;

end;

end;

end;

end;

hence rs = p by A49, FUNCT_1:9; :: thesis: verum

end;

hence p = (rpoly 1,z) *' s by A22; :: thesis: verum

end;

end;