let L be non empty right_complementable well-unital distributive Abelian add-associative right_zeroed associative commutative 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 A2: len p = 0 ; :: thesis: ex s being Polynomial of L st p = (rpoly (1,z)) *' s

take 0_. L ; :: thesis: p = (rpoly (1,z)) *' (0_. L)
p = 0_. L by A2, POLYNOM4:5;
hence p = (rpoly (1,z)) *' (0_. L) by POLYNOM3:34; :: 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:5;
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)) );
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)) ) ) );
A4: 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] )
A5: dom p = NAT by FUNCT_2:def 1;
assume k in Seg m1 ; :: thesis: ex x being Element of the carrier of (Polynom-Ring L) st S₂[k,x]
then A6: 1 <= k by FINSEQ_1:1;

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

suppose A7: 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 10;
take t ; :: thesis: S₂[k,t]
thus S₂[k,t] by A7; :: thesis: verum

end;

suppose A8: 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 10;
take t ; :: thesis: S₂[k,t]
ex u being Element of L ex b being Element of NAT st
( u = p . k & b = k & t = u * (qpoly (b,z)) )

proof

take p /. k ; :: thesis: ex b being Element of NAT st
( p /. k = p . k & b = k & t = (p /. k) * (qpoly (b,z)) )
reconsider b = k as Element of NAT by ORDINAL1:def 12;
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 A5, PARTFUN1:def 6; :: thesis: verum

end;

hence S₂[k,t] by A8; :: thesis: verum

end;

end;

end;

consider hs being FinSequence of (Polynom-Ring L) such that
A9: ( dom hs = Seg m1 & ( for k being Nat st k in Seg m1 holds
S₂[k,hs . k] ) ) from FINSEQ_1:sch 5(A4);

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

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

end;

A13: 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 10;
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)) )
A14: k1 in NAT ;
dom p = NAT by FUNCT_2:def 1;
hence ( p /. k = p . k & k1 = k & t = (p /. k) * (rpoly (k1,z)) ) by A14, PARTFUN1:def 6; :: thesis: verum

end;

consider h being FinSequence of (Polynom-Ring L) such that
A15: ( dom h = Seg m1 & ( for k being Nat st k in Seg m1 holds
S₁[k,h . k] ) ) from FINSEQ_1:sch 5(A13);
set s = Sum hs;
set rs = Sum h;
reconsider s = Sum hs, rs = Sum h as Polynomial of L by POLYNOM3:def 10;

A16: now :: thesis: for k being Element of NAT st 1 <= k & k <= m1 holds
h . k = (p . k) * (rpoly (k,z))

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

end;

A19: m1 + 1 = len p ;

A20: now :: thesis: for i being Element of NAT st i >= len p holds
rs . i = 0. L

let i be Element of NAT ; :: thesis: ( i >= len p implies rs . i = 0. L )
assume A21: i >= len p ; :: thesis: rs . i = 0. L
set co = Coeff (h,i);
A22: 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 :: thesis: for j being Element of NAT st j in dom (Coeff (h,i)) holds
(Coeff (h,i)) . j = 0. L

let j be Element of NAT ; :: thesis: ( j in dom (Coeff (h,i)) implies (Coeff (h,i)) . j = 0. L )
assume A23: j in dom (Coeff (h,i)) ; :: thesis: (Coeff (h,i)) . j = 0. L
then A24: ex ci being Polynomial of L st
( ci = h . j & (Coeff (h,i)) . j = ci . i ) by Def1;
A25: j <= m1 by A15, A22, A23, FINSEQ_1:1;
then A26: j <> i by A19, A21, NAT_1:16, XXREAL_0:2;
1 <= j by A15, A22, A23, FINSEQ_1:1;
hence (Coeff (h,i)) . j = ((p . j) * (rpoly (j,z))) . i by A16, A24, A25
.= (p . j) * ((rpoly (j,z)) . i) by POLYNOM5:def 4
.= (p . j) * (0. L) by A3, A21, A26, Lm11
.= 0. L ;
:: thesis: verum

end;

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

end;

A27: len h = m1 by A15, FINSEQ_1:def 3;

A28: now :: thesis: for i being Element of NAT st i > 0 & i < len p holds
rs . i = ((p . i) * (rpoly (i,z))) . i

let i be Element of NAT ; :: thesis: ( i > 0 & i < len p implies rs . i = ((p . i) * (rpoly (i,z))) . i )
assume that
A29: i > 0 and
A30: i < len p ; :: thesis: rs . i = ((p . i) * (rpoly (i,z))) . i
i < m1 + 1 by A30;
then A31: i <= m1 by NAT_1:13;
i + 1 > 0 + 1 by A29, XREAL_1:8;
then A32: i >= 1 by NAT_1:13;
then A33: h . i = (p . i) * (rpoly (i,z)) by A16, A31;
set co = Coeff (h,i);
A34: 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 ;
i in Seg (len h) by A27, A32, A31;
then A35: i in dom (Coeff (h,i)) by A34, FINSEQ_1:def 3;
then A36: ex cc being Polynomial of L st
( cc = h . i & (Coeff (h,i)) . i = cc . i ) by Def1;

now :: thesis: for i9 being Element of NAT st i9 in dom (Coeff (h,i)) & i9 <> i holds
(Coeff (h,i)) /. i9 = 0. L

let i9 be Element of NAT ; :: thesis: ( i9 in dom (Coeff (h,i)) & i9 <> i implies (Coeff (h,i)) /. i9 = 0. L )
assume that
A37: i9 in dom (Coeff (h,i)) and
A38: i9 <> i ; :: thesis: (Coeff (h,i)) /. i9 = 0. L
A39: ex ci being Polynomial of L st
( ci = h . i9 & (Coeff (h,i)) . i9 = ci . i ) by A37, Def1;
A40: i9 <= (len p) - 1 by A15, A34, A37, FINSEQ_1:1;
1 <= i9 by A15, A34, A37, FINSEQ_1:1;
then (Coeff (h,i)) . i9 = ((p . i9) * (rpoly (i9,z))) . i by A16, A39, A40
.= (p . i9) * ((rpoly (i9,z)) . i) by POLYNOM5:def 4
.= (p . i9) * (0. L) by A29, A38, Lm11
.= 0. L ;
hence (Coeff (h,i)) /. i9 = 0. L by A37, PARTFUN1:def 6; :: thesis: verum

end;

then Sum (Coeff (h,i)) = (Coeff (h,i)) /. i by A35, POLYNOM2:3
.= (Coeff (h,i)) . i by A35, PARTFUN1:def 6 ;
hence rs . i = ((p . i) * (rpoly (i,z))) . i by A36, A33, Th13; :: thesis: verum

end;

A41: now :: thesis: for i9 being object st i9 in dom p holds
p . i9 = rs . i9

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

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

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

set co = Coeff (h,0);
consider evp being FinSequence of L such that
A43: eval (p,z) = Sum evp and
A44: len evp = len p and
A45: 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;
set cop = <*(- (p . 0))*> ^ (Coeff (h,0));
A46: len (<*(- (p . 0))*> ^ (Coeff (h,0))) = (len <*(- (p . 0))*>) + (len (Coeff (h,0))) by FINSEQ_1:22
.= 1 + (len (Coeff (h,0))) by FINSEQ_1:39 ;
then A47: len (<*(- (p . 0))*> ^ (Coeff (h,0))) = 1 + (len h) by Def1
.= len evp by A27, A44 ;
then A48: dom (<*(- (p . 0))*> ^ (Coeff (h,0))) = Seg (len evp) by FINSEQ_1:def 3
.= dom evp by FINSEQ_1:def 3 ;
A49: 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 ;

A50: now :: thesis: for j being Element of NAT st j in dom (Coeff (h,0)) holds
(Coeff (h,0)) . j = - ((p . j) * ((power L) . (z,j)))

let j be Element of NAT ; :: thesis: ( j in dom (Coeff (h,0)) implies (Coeff (h,0)) . j = - ((p . j) * ((power L) . (z,j))) )
reconsider aj = - ((power L) . (z,j)) as Element of L ;
assume A51: j in dom (Coeff (h,0)) ; :: thesis: (Coeff (h,0)) . j = - ((p . j) * ((power L) . (z,j)))
then A52: 1 <= j by A15, A49, FINSEQ_1:1;
A53: j <= m1 by A15, A49, A51, FINSEQ_1:1;
ex ci being Polynomial of L st
( ci = h . j & (Coeff (h,0)) . j = ci . i ) by A42, A51, Def1;
hence (Coeff (h,0)) . j = ((p . j) * (rpoly (j,z))) . i by A16, A52, A53
.= (p . j) * ((rpoly (j,z)) . i) by POLYNOM5:def 4
.= (p . j) * aj by A42, A52, Lm10
.= - ((p . j) * ((power L) . (z,j))) by VECTSP_1:8 ;
:: thesis: verum

end;

now :: thesis: for j being Element of NAT st j in dom (<*(- (p . 0))*> ^ (Coeff (h,0))) holds
(<*(- (p . 0))*> ^ (Coeff (h,0))) /. j = - (evp /. j)

let j be Element of NAT ; :: thesis: ( j in dom (<*(- (p . 0))*> ^ (Coeff (h,0))) implies (<*(- (p . 0))*> ^ (Coeff (h,0))) /. b₁ = - (evp /. b₁) )
A54: dom <*(- (p . 0))*> = {1} by FINSEQ_1:2, FINSEQ_1:38;
assume A55: j in dom (<*(- (p . 0))*> ^ (Coeff (h,0))) ; :: thesis: (<*(- (p . 0))*> ^ (Coeff (h,0))) /. b₁ = - (evp /. b₁)
then A56: evp /. j = evp . j by A48, PARTFUN1:def 6
.= (p . (j -' 1)) * ((power L) . (z,(j -' 1))) by A45, A48, A55 ;
A57: j in Seg (len (<*(- (p . 0))*> ^ (Coeff (h,0)))) by A55, FINSEQ_1:def 3;
then A58: 1 <= j by FINSEQ_1:1;
A59: j <= len (<*(- (p . 0))*> ^ (Coeff (h,0))) by A57, FINSEQ_1:1;

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

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

then j -' 1 = 1 - 1 by XREAL_0:def 2;
then A61: evp /. j = (p . 0) * (1_ L) by A56, GROUP_1:def 7
.= p . 0 ;
j in dom <*(- (p . 0))*> by A54, A60, TARSKI:def 1;
then (<*(- (p . 0))*> ^ (Coeff (h,0))) . j = <*(- (p . 0))*> . j by FINSEQ_1:def 7
.= - (p . 0) by A60 ;
hence (<*(- (p . 0))*> ^ (Coeff (h,0))) /. j = - (evp /. j) by A55, A61, PARTFUN1:def 6; :: thesis: verum

end;

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

then reconsider j1 = j - 1 as Element of NAT by INT_1:5;
1 < j1 + 1 by A62;
then A63: 1 <= j1 by NAT_1:13;
j1 <= (len (<*(- (p . 0))*> ^ (Coeff (h,0)))) - 1 by A59, XREAL_1:9;
then j1 in Seg (len (Coeff (h,0))) by A46, A63;
then A64: j1 in dom (Coeff (h,0)) by FINSEQ_1:def 3;
A65: j <= len (<*(- (p . 0))*> ^ (Coeff (h,0))) by A57, FINSEQ_1:1;
j - 1 >= 1 - 1 by A62, XREAL_1:9;
then A66: j -' 1 = j - 1 by XREAL_0:def 2;
len <*(- (p . 0))*> < j by A62, FINSEQ_1:40;
then (<*(- (p . 0))*> ^ (Coeff (h,0))) . j = (Coeff (h,0)) . (j - (len <*(- (p . 0))*>)) by A65, FINSEQ_1:24
.= (Coeff (h,0)) . (j - 1) by FINSEQ_1:40
.= - ((p . j1) * ((power L) . (z,j1))) by A50, A64 ;
hence (<*(- (p . 0))*> ^ (Coeff (h,0))) /. j = - (evp /. j) by A55, A56, A66, PARTFUN1:def 6; :: thesis: verum

end;

end;

end;

then A67: - (Sum evp) = Sum (<*(- (p . 0))*> ^ (Coeff (h,0))) by A47, Th7
.= (Sum <*(- (p . 0))*>) + (Sum (Coeff (h,0))) by RLVECT_1:41
.= (- (p . 0)) + (Sum (Coeff (h,0))) by RLVECT_1:44 ;
Sum evp = 0. L by A1, A43, POLYNOM5:def 7;
then 0. L = (- (p . 0)) + (Sum (Coeff (h,0))) by A67, RLVECT_1:12;
then p . 0 = (p . 0) + ((- (p . 0)) + (Sum (Coeff (h,0)))) by ALGSTR_1:def 2
.= ((p . 0) + (- (p . 0))) + (Sum (Coeff (h,0))) by RLVECT_1:def 3
.= (0. L) + (Sum (Coeff (h,0))) by RLVECT_1:5
.= Sum (Coeff (h,0)) by ALGSTR_1:def 2 ;
hence p . i9 = rs . i9 by A42, Th13; :: thesis: verum

end;

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

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

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

hence rs . i9 = 0. L by A20
.= p . i9 by A69, ALGSEQ_1:8 ;
:: thesis: verum

end;

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

hence rs . i9 = ((p . i) * (rpoly (i,z))) . i by A28, A68
.= (p . i) * ((rpoly (i,z)) . i) by POLYNOM5:def 4
.= (p . i) * (1_ L) by A68, Lm10
.= p . i9 ;
:: thesis: verum

end;

end;

end;

end;

end;

now :: thesis: not m1 < 1

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 8; :: thesis: verum

end;

then 1 in Seg m1 ;
then A70: hs . 1 = (p . 1) * (1_. L) by A9;

A71: now :: thesis: for i9 being object st i9 in dom rs holds
rs . i9 = ((rpoly (1,z)) *' s) . i9

reconsider r1z = rpoly (1,z) as Element of (Polynom-Ring L) by POLYNOM3:def 10;
let i9 be object ; :: thesis: ( i9 in dom rs implies rs . i9 = ((rpoly (1,z)) *' s) . i9 )
assume i9 in dom rs ; :: thesis: rs . i9 = ((rpoly (1,z)) *' s) . i9
A72: dom (r1z * hs) = dom h by A9, A15, POLYNOM1:def 1;

now :: thesis: for k being Nat st k in dom h holds
(r1z * hs) . k = h . k

let k be Nat; :: thesis: ( k in dom h implies (r1z * hs) . b₁ = h . b₁ )
assume A73: k in dom h ; :: thesis: (r1z * hs) . b₁ = h . b₁
then A74: 1 <= k by A15, FINSEQ_1:1;
A75: k <= m1 by A15, A73, FINSEQ_1:1;

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

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

then A77: hs /. k = (p . 1) * (1_. L) by A9, A70, A15, A73, PARTFUN1:def 6;
thus (r1z * hs) . k = (r1z * hs) /. k by A72, A73, PARTFUN1:def 6
.= r1z * (hs /. k) by A9, A15, A73, POLYNOM1:def 1
.= (rpoly (1,z)) *' ((p . 1) * (1_. L)) by A77, POLYNOM3:def 10
.= (p . 1) * ((rpoly (1,z)) *' (1_. L)) by Th19
.= (p . 1) * (rpoly (1,z)) by POLYNOM3:35
.= h . k by A16, A75, A76 ; :: thesis: verum

end;

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

reconsider k1 = k as Element of NAT by A73;
A79: hs /. k = hs . k by A9, A15, A73, PARTFUN1:def 6
.= (p . k1) * (qpoly (k1,z)) by A10, A75, A78 ;
thus (r1z * hs) . k = (r1z * hs) /. k by A72, A73, PARTFUN1:def 6
.= r1z * (hs /. k) by A9, A15, A73, POLYNOM1:def 1
.= (rpoly (1,z)) *' ((p . k1) * (qpoly (k1,z))) by A79, POLYNOM3:def 10
.= (p . k1) * ((rpoly (1,z)) *' (qpoly (k1,z))) by Th19
.= (p . k1) * (rpoly (k1,z)) by A78, Th32
.= h . k by A16, A74, A75 ; :: thesis: verum

end;

end;

end;

then r1z * hs = h by A72, FINSEQ_1:13;
hence rs . i9 = ((rpoly (1,z)) *' s) . i9 by Lm5; :: thesis: verum

end;

take s ; :: thesis: p = (rpoly (1,z)) *' s
dom ((rpoly (1,z)) *' s) = NAT by FUNCT_2:def 1
.= dom rs by FUNCT_2:def 1 ;
then A80: (rpoly (1,z)) *' s = rs by A71, FUNCT_1:2;
dom p = NAT by FUNCT_2:def 1
.= dom rs by FUNCT_2:def 1 ;
hence p = (rpoly (1,z)) *' s by A80, A41, FUNCT_1:2; :: thesis: verum

end;

end;