:: POLYNOM5 semantic presentation

begin

theorem Th1: :: POLYNOM5:1
for n, m being Element of NAT st n <> 0 & m <> 0 holds
(((n * m) - n) - m) + 1 >= 0
proof
let n, m be Element of NAT ; ::_thesis: ( n <> 0 & m <> 0 implies (((n * m) - n) - m) + 1 >= 0 )
assume that
A1: n <> 0 and
A2: m <> 0 ; ::_thesis: (((n * m) - n) - m) + 1 >= 0
 m >= 0 + 1 by A2, NAT_1:13;
then A3: m - 1 >= (0 + 1) - 1 by XREAL_1:9;
 n >= 0 + 1 by A1, NAT_1:13;
then  n - 1 >= (0 + 1) - 1 by XREAL_1:9;
then  (n - 1) * (m - 1) >= 0 by A3;
hence  (((n * m) - n) - m) + 1 >= 0 ; ::_thesis: verum
end;

theorem Th2: :: POLYNOM5:2
for x, y being real number st y > 0 holds
(min (x,y)) / (max (x,y)) <= 1
proof
let x, y be real number ; ::_thesis: ( y > 0 implies (min (x,y)) / (max (x,y)) <= 1 )
assume A1: y > 0 ; ::_thesis: (min (x,y)) / (max (x,y)) <= 1
percases ( x > 0 or x <= 0 ) ;
supposeA2: x > 0 ; ::_thesis: (min (x,y)) / (max (x,y)) <= 1
now__::_thesis:_(min_(x,y))_/_(max_(x,y))_<=_1
percases ( x >= y or x < y ) ;
supposeA3: x >= y ; ::_thesis: (min (x,y)) / (max (x,y)) <= 1
then  ( max (x,y) = x & min (x,y) = y ) by XXREAL_0:def_9, XXREAL_0:def_10;
hence  (min (x,y)) / (max (x,y)) <= 1 by A1, A3, XREAL_1:183; ::_thesis: verum
end;
supposeA4: x < y ; ::_thesis: (min (x,y)) / (max (x,y)) <= 1
then  ( max (x,y) = y & min (x,y) = x ) by XXREAL_0:def_9, XXREAL_0:def_10;
hence  (min (x,y)) / (max (x,y)) <= 1 by A2, A4, XREAL_1:183; ::_thesis: verum
end;
end;
end;
hence  (min (x,y)) / (max (x,y)) <= 1 ; ::_thesis: verum
end;
supposeA5: x <= 0 ; ::_thesis: (min (x,y)) / (max (x,y)) <= 1
then  ( min (x,y) = x & max (x,y) = y ) by A1, XXREAL_0:def_9, XXREAL_0:def_10;
hence  (min (x,y)) / (max (x,y)) <= 1 by A1, A5; ::_thesis: verum
end;
end;
end;

theorem Th3: :: POLYNOM5:3
for x, y being real number st ( for c being real number st c > 0 & c < 1 holds
c * x >= y ) holds
y <= 0
proof
let x, y be real number ; ::_thesis: ( ( for c being real number st c > 0 & c < 1 holds
c * x >= y ) implies y <= 0 )
assume A1: for c being real number st c > 0 & c < 1 holds
c * x >= y ; ::_thesis: y <= 0
set ma = max (x,y);
set mi = min (x,y);
set c = (min (x,y)) / (2 * (max (x,y)));
assume A2: y > 0 ; ::_thesis: contradiction
then A3: y * 2 > y by XREAL_1:155;
percases ( x > 0 or x <= 0 ) ;
supposeA4: x > 0 ; ::_thesis: contradiction
then A5: ( min (x,y) > 0 & max (x,y) > 0 ) by A2, XXREAL_0:15, XXREAL_0:16;
then  ((min (x,y)) / (max (x,y))) * 2 > (min (x,y)) / (max (x,y)) by XREAL_1:155;
then  (min (x,y)) / (max (x,y)) > ((min (x,y)) / (max (x,y))) / 2 by XREAL_1:83;
then A6: (min (x,y)) / (max (x,y)) > (min (x,y)) / ((max (x,y)) * 2) by XCMPLX_1:78;
 (min (x,y)) / (max (x,y)) <= 1 by A4, Th2;
then  (min (x,y)) / (2 * (max (x,y))) < 1 by A6, XXREAL_0:2;
then A7: ((min (x,y)) / (2 * (max (x,y)))) * x >= y by A1, A5;
now__::_thesis:_contradiction
percases ( x >= y or x < y ) ;
suppose x >= y ; ::_thesis: contradiction
then  ( max (x,y) = x & min (x,y) = y ) by XXREAL_0:def_9, XXREAL_0:def_10;
then  ((min (x,y)) / (2 * (max (x,y)))) * x = y / 2 by A4, XCMPLX_1:92;
hence  contradiction by A3, A7, XREAL_1:83; ::_thesis: verum
end;
supposeA8: x < y ; ::_thesis: contradiction
then  ( max (x,y) = y & min (x,y) = x ) by XXREAL_0:def_9, XXREAL_0:def_10;
then  ((min (x,y)) / (2 * (max (x,y)))) * x < (x / (2 * y)) * y by A4, A8, XREAL_1:98;
then A9: ((min (x,y)) / (2 * (max (x,y)))) * x < x / 2 by A2, XCMPLX_1:92;
A10: y > y / 2 by A3, XREAL_1:83;
 x / 2 < y / 2 by A8, XREAL_1:74;
then  ((min (x,y)) / (2 * (max (x,y)))) * x < y / 2 by A9, XXREAL_0:2;
hence  contradiction by A7, A10, XXREAL_0:2; ::_thesis: verum
end;
end;
end;
hence  contradiction ; ::_thesis: verum
end;
suppose x <= 0 ; ::_thesis: contradiction
then  (1 / 2) * x <= 0 ;
hence  contradiction by A1, A2; ::_thesis: verum
end;
end;
end;

Lm1:  for x, y being Real st ( for c being Real st c > 0 & c < 1 holds
c * x >= y ) holds
y <= 0
proof
let x, y be Real; ::_thesis: ( ( for c being Real st c > 0 & c < 1 holds
c * x >= y ) implies y <= 0 )
assume A1: for c being Real st c > 0 & c < 1 holds
c * x >= y ; ::_thesis: y <= 0
 for c being real number st c > 0 & c < 1 holds
c * x >= y
proof
let c be real number ; ::_thesis: ( c > 0 & c < 1 implies c * x >= y )
assume A2: ( c > 0 & c < 1 ) ; ::_thesis: c * x >= y
 c is Real by XREAL_0:def_1;
hence  c * x >= y by A1, A2; ::_thesis: verum
end;
hence  y <= 0 by Th3; ::_thesis: verum
end;

theorem Th4: :: POLYNOM5:4
for p being FinSequence of REAL st ( for n being Element of NAT st n in dom p holds
p . n >= 0 ) holds
for i being Element of NAT st i in dom p holds
Sum p >= p . i
proof
defpred S1[ FinSequence of REAL ] means ( ( for n being Element of NAT st n in dom $1 holds
$1 . n >= 0 ) implies for i being Element of NAT st i in dom $1 holds
Sum $1 >= $1 . i );
A1: for p being FinSequence of REAL
for x being Element of REAL st S1[p] holds
S1[p ^ <*x*>]
proof
let p be FinSequence of REAL ; ::_thesis: for x being Element of REAL st S1[p] holds
S1[p ^ <*x*>]
let x be Element of REAL ; ::_thesis: ( S1[p] implies S1[p ^ <*x*>] )
assume A2: ( ( for n being Element of NAT st n in dom p holds
p . n >= 0 ) implies for i being Element of NAT st i in dom p holds
Sum p >= p . i ) ; ::_thesis: S1[p ^ <*x*>]
defpred S2[ Element of NAT ] means  Sum (p | $1) >= 0 ;
assume A3: for n being Element of NAT st n in dom (p ^ <*x*>) holds
(p ^ <*x*>) . n >= 0 ; ::_thesis: for i being Element of NAT st i in dom (p ^ <*x*>) holds
Sum (p ^ <*x*>) >= (p ^ <*x*>) . i
A4: dom p c= dom (p ^ <*x*>) by FINSEQ_1:26;
A5: now__::_thesis:_for_n_being_Element_of_NAT_st_n_in_dom_p_holds_
p_._n_>=_0
let n be Element of NAT ; ::_thesis: ( n in dom p implies p . n >= 0 )
assume A6: n in dom p ; ::_thesis: p . n >= 0
then  (p ^ <*x*>) . n >= 0 by A3, A4;
hence  p . n >= 0 by A6, FINSEQ_1:def_7; ::_thesis: verum
end;
A7: for j being Element of NAT st S2[j] holds
S2[j + 1]
proof
let j be Element of NAT ; ::_thesis: ( S2[j] implies S2[j + 1] )
assume A8: Sum (p | j) >= 0 ; ::_thesis: S2[j + 1]
percases ( j + 1 <= len p or j + 1 > len p ) ;
supposeA9: j + 1 <= len p ; ::_thesis: S2[j + 1]
then  p | (j + 1) = (p | j) ^ <*(p /. (j + 1))*> by FINSEQ_5:82;
then A10: Sum (p | (j + 1)) = (Sum (p | j)) + (p /. (j + 1)) by RVSUM_1:74;
 j + 1 >= 1 by NAT_1:11;
then A11: j + 1 in dom p by A9, FINSEQ_3:25;
then  p . (j + 1) >= 0 by A5;
then  p /. (j + 1) >= 0 by A11, PARTFUN1:def_6;
hence  S2[j + 1] by A8, A10; ::_thesis: verum
end;
supposeA12: j + 1 > len p ; ::_thesis: S2[j + 1]
then  j >= len p by NAT_1:13;
then  p | j = p by FINSEQ_1:58;
hence  S2[j + 1] by A8, A12, FINSEQ_1:58; ::_thesis: verum
end;
end;
end;
let i be Element of NAT ; ::_thesis: ( i in dom (p ^ <*x*>) implies Sum (p ^ <*x*>) >= (p ^ <*x*>) . i )
 (len p) + 1 >= 0 + 1 by XREAL_1:6;
then  len (p ^ <*x*>) >= 1 by FINSEQ_2:16;
then  len (p ^ <*x*>) in dom (p ^ <*x*>) by FINSEQ_3:25;
then  (p ^ <*x*>) . (len (p ^ <*x*>)) >= 0 by A3;
then  (p ^ <*x*>) . ((len p) + 1) >= 0 by FINSEQ_2:16;
then  x >= 0 by FINSEQ_1:42;
then A13: (p . i) + x >= (p . i) + 0 by XREAL_1:6;
A14: p | (len p) = p by FINSEQ_1:58;
 len (p ^ <*x*>) = (len p) + 1 by FINSEQ_2:16;
then A15: dom (p ^ <*x*>) = Seg ((len p) + 1) by FINSEQ_1:def_3
.= (Seg (len p)) \/ {((len p) + 1)} by FINSEQ_1:9
.= (dom p) \/ {((len p) + 1)} by FINSEQ_1:def_3 ;
A16: S2[ 0 ] by RVSUM_1:72;
 for j being Element of NAT holds S2[j] from NAT_1:sch_1(A16, A7);
then A17: Sum p >= 0 by A14;
assume A18: i in dom (p ^ <*x*>) ; ::_thesis: Sum (p ^ <*x*>) >= (p ^ <*x*>) . i
percases ( i in dom p or i in {((len p) + 1)} ) by A18, A15, XBOOLE_0:def_3;
supposeA19: i in dom p ; ::_thesis: Sum (p ^ <*x*>) >= (p ^ <*x*>) . i
A20: Sum (p ^ <*x*>) = (Sum p) + x by RVSUM_1:74;
 Sum p >= p . i by A2, A5, A19;
then  Sum (p ^ <*x*>) >= (p . i) + x by A20, XREAL_1:6;
then  Sum (p ^ <*x*>) >= p . i by A13, XXREAL_0:2;
hence  Sum (p ^ <*x*>) >= (p ^ <*x*>) . i by A19, FINSEQ_1:def_7; ::_thesis: verum
end;
suppose i in {((len p) + 1)} ; ::_thesis: Sum (p ^ <*x*>) >= (p ^ <*x*>) . i
then  i = (len p) + 1 by TARSKI:def_1;
then  (p ^ <*x*>) . i = x by FINSEQ_1:42;
then  (Sum p) + x >= 0 + ((p ^ <*x*>) . i) by A17, XREAL_1:6;
hence  Sum (p ^ <*x*>) >= (p ^ <*x*>) . i by RVSUM_1:74; ::_thesis: verum
end;
end;
end;
A21: S1[ <*> REAL] ;
thus  for p being FinSequence of REAL holds S1[p] from FINSEQ_2:sch_2(A21, A1); ::_thesis: verum
end;

theorem Th5: :: POLYNOM5:5
for x, y being Real holds - [**x,y**] = [**(- x),(- y)**]
proof
let x, y be Real; ::_thesis: - [**x,y**] = [**(- x),(- y)**]
thus  - [**x,y**] = - (x + (y * <i>)) by COMPLFLD:2
.= [**(- x),(- y)**] ; ::_thesis: verum
end;

theorem Th6: :: POLYNOM5:6
for x1, y1, x2, y2 being Real holds [**x1,y1**] - [**x2,y2**] = [**(x1 - x2),(y1 - y2)**]
proof
let x1, y1, x2, y2 be Real; ::_thesis: [**x1,y1**] - [**x2,y2**] = [**(x1 - x2),(y1 - y2)**]
thus [**x1,y1**] - [**x2,y2**] = [**x1,y1**] + [**(- x2),(- y2)**] by Th5
.= [**(x1 - x2),(y1 - y2)**] ; ::_thesis: verum
end;

theorem Th7: :: POLYNOM5:7
for z being Element of F_Complex st z <> 0. F_Complex holds
for n being Element of NAT holds |.((power F_Complex) . (z,n)).| = |.z.| to_power n
proof
let z be Element of F_Complex; ::_thesis: ( z <> 0. F_Complex implies for n being Element of NAT holds |.((power F_Complex) . (z,n)).| = |.z.| to_power n )
defpred S1[ Element of NAT ] means |.((power F_Complex) . (z,$1)).| = |.z.| to_power $1;
assume  z <> 0. F_Complex ; ::_thesis: for n being Element of NAT holds |.((power F_Complex) . (z,n)).| = |.z.| to_power n
then A1: |.z.| <> 0 by COMPLFLD:58;
A2: |.z.| >= 0 by COMPLEX1:46;
A3: for n being Element of NAT st S1[n] holds
S1[n + 1]
proof
let n be Element of NAT ; ::_thesis: ( S1[n] implies S1[n + 1] )
assume A4: |.((power F_Complex) . (z,n)).| = |.z.| to_power n ; ::_thesis: S1[n + 1]
thus |.((power F_Complex) . (z,(n + 1))).| = |.(((power F_Complex) . (z,n)) * z).| by GROUP_1:def_7
.= (|.z.| to_power n) * |.z.| by A4, COMPLFLD:71
.= (|.z.| to_power n) * (|.z.| to_power 1) by POWER:25
.= |.z.| to_power (n + 1) by A1, A2, POWER:27 ; ::_thesis: verum
end;
|.((power F_Complex) . (z,0)).| = 1 by COMPLEX1:48, COMPLFLD:8, GROUP_1:def_7
.= |.z.| to_power 0 by POWER:24 ;
then A5: S1[ 0 ] ;
thus  for n being Element of NAT holds S1[n] from NAT_1:sch_1(A5, A3); ::_thesis: verum
end;

definition
let p be FinSequence of the carrier of F_Complex;
func|.p.| ->  FinSequence of REAL  means :Def1: :: POLYNOM5:def 1
( len it = len p & ( for n being Element of NAT st n in dom p holds
it /. n = |.(p /. n).| ) );
existence
 ex b1 being FinSequence of REAL st
( len b1 = len p & ( for n being Element of NAT st n in dom p holds
b1 /. n = |.(p /. n).| ) )
proof
deffunc H1( Nat) ->  Element of REAL = |.(p /. $1).|;
consider q being FinSequence of REAL  such that
A1: len q = len p and
A2: for n being Nat st n in dom q holds
q /. n = H1(n) from FINSEQ_4:sch_2();
take  q ; ::_thesis: ( len q = len p & ( for n being Element of NAT st n in dom p holds
q /. n = |.(p /. n).| ) )
 dom p = dom q by A1, FINSEQ_3:29;
hence  ( len q = len p & ( for n being Element of NAT st n in dom p holds
q /. n = |.(p /. n).| ) ) by A1, A2; ::_thesis: verum
end;
uniqueness
 for b1, b2 being FinSequence of REAL st len b1 = len p & ( for n being Element of NAT st n in dom p holds
b1 /. n = |.(p /. n).| ) & len b2 = len p & ( for n being Element of NAT st n in dom p holds
b2 /. n = |.(p /. n).| ) holds
b1 = b2
proof
let q1, q2 be FinSequence of REAL ; ::_thesis: ( len q1 = len p & ( for n being Element of NAT st n in dom p holds
q1 /. n = |.(p /. n).| ) & len q2 = len p & ( for n being Element of NAT st n in dom p holds
q2 /. n = |.(p /. n).| ) implies q1 = q2 )
assume that
A3: len q1 = len p and
A4: for n being Element of NAT st n in dom p holds
q1 /. n = |.(p /. n).| and
A5: len q2 = len p and
A6: for n being Element of NAT st n in dom p holds
q2 /. n = |.(p /. n).| ; ::_thesis: q1 = q2
A7: now__::_thesis:_for_n_being_Nat_st_n_in_dom_p_holds_
q1_/._n_=_q2_/._n
let n be Nat; ::_thesis: ( n in dom p implies q1 /. n = q2 /. n )
assume A8: n in dom p ; ::_thesis: q1 /. n = q2 /. n
hence q1 /. n = |.(p /. n).| by A4
.= q2 /. n by A6, A8 ;
::_thesis: verum
end;
 ( dom q1 = dom p & dom q2 = dom p ) by A3, A5, FINSEQ_3:29;
hence  q1 = q2 by A7, FINSEQ_5:12; ::_thesis: verum
end;
end;

:: deftheorem Def1 defines |. POLYNOM5:def_1_:_
 for p being FinSequence of the carrier of F_Complex
for b2 being FinSequence of REAL holds
( b2 = |.p.| iff ( len b2 = len p & ( for n being Element of NAT st n in dom p holds
b2 /. n = |.(p /. n).| ) ) );

theorem Th8: :: POLYNOM5:8
|.(<*> the carrier of F_Complex).| = <*> REAL
proof
len |.(<*> the carrier of F_Complex).| = len (<*> the carrier of F_Complex) by Def1
.= 0 ;
hence  |.(<*> the carrier of F_Complex).| = <*> REAL ; ::_thesis: verum
end;

theorem Th9: :: POLYNOM5:9
for x being Element of F_Complex holds |.<*x*>.| = <*|.x.|*>
proof
let x be Element of F_Complex; ::_thesis: |.<*x*>.| = <*|.x.|*>
 0 + 1 in Seg (0 + 1) by FINSEQ_1:4;
then A1: 1 in dom <*x*> by FINSEQ_1:38;
A2: len |.<*x*>.| = len <*x*> by Def1
.= 1 by FINSEQ_1:39 ;
then A3: dom |.<*x*>.| = Seg 1 by FINSEQ_1:def_3;
 len |.<*x*>.| = len <*x*> by Def1;
then A4: 1 in dom |.<*x*>.| by A1, FINSEQ_3:29;
A5: now__::_thesis:_for_n_being_Nat_st_n_in_dom_|.<*x*>.|_holds_
|.<*x*>.|_._n_=_<*|.x.|*>_._n
let n be Nat; ::_thesis: ( n in dom |.<*x*>.| implies |.<*x*>.| . n = <*|.x.|*> . n )
assume  n in dom |.<*x*>.| ; ::_thesis: |.<*x*>.| . n = <*|.x.|*> . n
then A6: n = 1 by A3, FINSEQ_1:2, TARSKI:def_1;
hence |.<*x*>.| . n = |.<*x*>.| /. 1 by A4, PARTFUN1:def_6
.= |.(<*x*> /. 1).| by A1, Def1
.= |.x.| by FINSEQ_4:16
.= <*|.x.|*> . n by A6, FINSEQ_1:40 ;
::_thesis: verum
end;
 len <*|.x.|*> = 1 by FINSEQ_1:39;
hence  |.<*x*>.| = <*|.x.|*> by A2, A5, FINSEQ_2:9; ::_thesis: verum
end;

theorem :: POLYNOM5:10
for x, y being Element of F_Complex holds |.<*x,y*>.| = <*|.x.|,|.y.|*>
proof
let x, y be Element of F_Complex; ::_thesis: |.<*x,y*>.| = <*|.x.|,|.y.|*>
A1: len |.<*x,y*>.| = len <*x,y*> by Def1
.= 2 by FINSEQ_1:44 ;
then A2: dom |.<*x,y*>.| = Seg 2 by FINSEQ_1:def_3;
A3: now__::_thesis:_for_n_being_Nat_st_n_in_dom_|.<*x,y*>.|_holds_
|.<*x,y*>.|_._n_=_<*|.x.|,|.y.|*>_._n
let n be Nat; ::_thesis: ( n in dom |.<*x,y*>.| implies |.<*x,y*>.| . b1 = <*|.x.|,|.y.|*> . b1 )
assume A4: n in dom |.<*x,y*>.| ; ::_thesis: |.<*x,y*>.| . b1 = <*|.x.|,|.y.|*> . b1
percases ( n = 1 or n = 2 ) by A2, A4, FINSEQ_1:2, TARSKI:def_2;
supposeA5: n = 1 ; ::_thesis: |.<*x,y*>.| . b1 = <*|.x.|,|.y.|*> . b1
then A6: 1 in dom <*x,y*> by A2, A4, FINSEQ_1:89;
|.<*x,y*>.| . 1 = |.<*x,y*>.| /. 1 by A4, A5, PARTFUN1:def_6
.= |.(<*x,y*> /. 1).| by A6, Def1 ;
then  |.<*x,y*>.| . 1 = |.x.| by FINSEQ_4:17;
hence  |.<*x,y*>.| . n = <*|.x.|,|.y.|*> . n by A5, FINSEQ_1:44; ::_thesis: verum
end;
supposeA7: n = 2 ; ::_thesis: |.<*x,y*>.| . b1 = <*|.x.|,|.y.|*> . b1
then A8: 2 in dom <*x,y*> by A2, A4, FINSEQ_1:89;
|.<*x,y*>.| . 2 = |.<*x,y*>.| /. 2 by A4, A7, PARTFUN1:def_6
.= |.(<*x,y*> /. 2).| by A8, Def1 ;
then  |.<*x,y*>.| . 2 = |.y.| by FINSEQ_4:17;
hence  |.<*x,y*>.| . n = <*|.x.|,|.y.|*> . n by A7, FINSEQ_1:44; ::_thesis: verum
end;
end;
end;
 len <*|.x.|,|.y.|*> = 2 by FINSEQ_1:44;
hence  |.<*x,y*>.| = <*|.x.|,|.y.|*> by A1, A3, FINSEQ_2:9; ::_thesis: verum
end;

theorem :: POLYNOM5:11
for x, y, z being Element of F_Complex holds |.<*x,y,z*>.| = <*|.x.|,|.y.|,|.z.|*>
proof
let x, y, z be Element of F_Complex; ::_thesis: |.<*x,y,z*>.| = <*|.x.|,|.y.|,|.z.|*>
A1: len |.<*x,y,z*>.| = len <*x,y,z*> by Def1
.= 3 by FINSEQ_1:45 ;
then A2: dom |.<*x,y,z*>.| = Seg 3 by FINSEQ_1:def_3;
A3: now__::_thesis:_for_n_being_Nat_st_n_in_dom_|.<*x,y,z*>.|_holds_
|.<*x,y,z*>.|_._n_=_<*|.x.|,|.y.|,|.z.|*>_._n
let n be Nat; ::_thesis: ( n in dom |.<*x,y,z*>.| implies |.<*x,y,z*>.| . b1 = <*|.x.|,|.y.|,|.z.|*> . b1 )
assume A4: n in dom |.<*x,y,z*>.| ; ::_thesis: |.<*x,y,z*>.| . b1 = <*|.x.|,|.y.|,|.z.|*> . b1
percases ( n = 1 or n = 2 or n = 3 ) by A2, A4, ENUMSET1:def_1, FINSEQ_3:1;
supposeA5: n = 1 ; ::_thesis: |.<*x,y,z*>.| . b1 = <*|.x.|,|.y.|,|.z.|*> . b1
A6: 1 in dom <*x,y,z*> by TOPREAL3:1;
 len |.<*x,y,z*>.| = len <*x,y,z*> by Def1;
then  1 in dom |.<*x,y,z*>.| by A6, FINSEQ_3:29;
then |.<*x,y,z*>.| . 1 = |.<*x,y,z*>.| /. 1 by PARTFUN1:def_6
.= |.(<*x,y,z*> /. 1).| by A6, Def1 ;
then  |.<*x,y,z*>.| . 1 = |.x.| by FINSEQ_4:18;
hence  |.<*x,y,z*>.| . n = <*|.x.|,|.y.|,|.z.|*> . n by A5, FINSEQ_1:45; ::_thesis: verum
end;
supposeA7: n = 2 ; ::_thesis: |.<*x,y,z*>.| . b1 = <*|.x.|,|.y.|,|.z.|*> . b1
A8: 2 in dom <*x,y,z*> by TOPREAL3:1;
 len |.<*x,y,z*>.| = len <*x,y,z*> by Def1;
then  2 in dom |.<*x,y,z*>.| by A8, FINSEQ_3:29;
then |.<*x,y,z*>.| . 2 = |.<*x,y,z*>.| /. 2 by PARTFUN1:def_6
.= |.(<*x,y,z*> /. 2).| by A8, Def1 ;
then  |.<*x,y,z*>.| . 2 = |.y.| by FINSEQ_4:18;
hence  |.<*x,y,z*>.| . n = <*|.x.|,|.y.|,|.z.|*> . n by A7, FINSEQ_1:45; ::_thesis: verum
end;
supposeA9: n = 3 ; ::_thesis: |.<*x,y,z*>.| . b1 = <*|.x.|,|.y.|,|.z.|*> . b1
A10: 3 in dom <*x,y,z*> by TOPREAL3:1;
 len |.<*x,y,z*>.| = len <*x,y,z*> by Def1;
then  3 in dom |.<*x,y,z*>.| by A10, FINSEQ_3:29;
then |.<*x,y,z*>.| . 3 = |.<*x,y,z*>.| /. 3 by PARTFUN1:def_6
.= |.(<*x,y,z*> /. 3).| by A10, Def1 ;
then  |.<*x,y,z*>.| . 3 = |.z.| by FINSEQ_4:18;
hence  |.<*x,y,z*>.| . n = <*|.x.|,|.y.|,|.z.|*> . n by A9, FINSEQ_1:45; ::_thesis: verum
end;
end;
end;
 len <*|.x.|,|.y.|,|.z.|*> = 3 by FINSEQ_1:45;
hence  |.<*x,y,z*>.| = <*|.x.|,|.y.|,|.z.|*> by A1, A3, FINSEQ_2:9; ::_thesis: verum
end;

theorem Th12: :: POLYNOM5:12
for p, q being FinSequence of the carrier of F_Complex holds |.(p ^ q).| = |.p.| ^ |.q.|
proof
let p, q be FinSequence of the carrier of F_Complex; ::_thesis: |.(p ^ q).| = |.p.| ^ |.q.|
A1: dom |.(p ^ q).| = Seg (len |.(p ^ q).|) by FINSEQ_1:def_3;
A2: now__::_thesis:_for_n_being_Nat_st_n_in_dom_|.(p_^_q).|_holds_
|.(p_^_q).|_._n_=_(|.p.|_^_|.q.|)_._n
let n be Nat; ::_thesis: ( n in dom |.(p ^ q).| implies |.(p ^ q).| . b1 = (|.p.| ^ |.q.|) . b1 )
A3: len |.p.| = len p by Def1;
assume A4: n in dom |.(p ^ q).| ; ::_thesis: |.(p ^ q).| . b1 = (|.p.| ^ |.q.|) . b1
then A5: n >= 1 by A1, FINSEQ_1:1;
A6: len |.(p ^ q).| = len (p ^ q) by Def1;
then A7: n in dom (p ^ q) by A1, A4, FINSEQ_1:def_3;
percases ( n in dom p or not n in dom p ) ;
supposeA8: n in dom p ; ::_thesis: |.(p ^ q).| . b1 = (|.p.| ^ |.q.|) . b1
A9: (p ^ q) /. n = (p ^ q) . n by A7, PARTFUN1:def_6
.= p . n by A8, FINSEQ_1:def_7
.= p /. n by A8, PARTFUN1:def_6 ;
A10: n in dom |.p.| by A3, A8, FINSEQ_3:29;
thus |.(p ^ q).| . n = |.(p ^ q).| /. n by A4, PARTFUN1:def_6
.= |.((p ^ q) /. n).| by A7, Def1
.= |.p.| /. n by A8, A9, Def1
.= |.p.| . n by A10, PARTFUN1:def_6
.= (|.p.| ^ |.q.|) . n by A10, FINSEQ_1:def_7 ; ::_thesis: verum
end;
suppose not n in dom p ; ::_thesis: |.(p ^ q).| . b1 = (|.p.| ^ |.q.|) . b1
then A11: n > 0 + (len p) by A5, FINSEQ_3:25;
then A12: n - (len p) > 0 by XREAL_1:20;
A13: n = (len p) + (n - (len p))
.= (len p) + (n -' (len p)) by A12, XREAL_0:def_2 ;
 n <= len (p ^ q) by A1, A4, A6, FINSEQ_1:1;
then  n <= (len q) + (len p) by FINSEQ_1:22;
then  n - (len p) <= len q by XREAL_1:20;
then A14: n -' (len p) <= len q by XREAL_0:def_2;
 1 + (len p) <= n by A11, NAT_1:13;
then  1 <= n - (len p) by XREAL_1:19;
then  1 <= n -' (len p) by XREAL_0:def_2;
then A15: n -' (len p) in Seg (len q) by A14, FINSEQ_1:1;
then A16: n -' (len p) in dom q by FINSEQ_1:def_3;
 len |.q.| = len q by Def1;
then A17: n -' (len p) in dom |.q.| by A15, FINSEQ_1:def_3;
A18: (p ^ q) /. n = (p ^ q) . n by A7, PARTFUN1:def_6
.= q . (n -' (len p)) by A13, A16, FINSEQ_1:def_7
.= q /. (n -' (len p)) by A16, PARTFUN1:def_6 ;
thus |.(p ^ q).| . n = |.(p ^ q).| /. n by A4, PARTFUN1:def_6
.= |.((p ^ q) /. n).| by A7, Def1
.= |.q.| /. (n -' (len p)) by A16, A18, Def1
.= |.q.| . (n -' (len p)) by A17, PARTFUN1:def_6
.= (|.p.| ^ |.q.|) . n by A3, A13, A17, FINSEQ_1:def_7 ; ::_thesis: verum
end;
end;
end;
len |.(p ^ q).| = len (p ^ q) by Def1
.= (len p) + (len q) by FINSEQ_1:22
.= (len p) + (len |.q.|) by Def1
.= (len |.p.|) + (len |.q.|) by Def1
.= len (|.p.| ^ |.q.|) by FINSEQ_1:22 ;
hence  |.(p ^ q).| = |.p.| ^ |.q.| by A2, FINSEQ_2:9; ::_thesis: verum
end;

theorem :: POLYNOM5:13
for p being FinSequence of the carrier of F_Complex
for x being Element of F_Complex holds
( |.(p ^ <*x*>).| = |.p.| ^ <*|.x.|*> & |.(<*x*> ^ p).| = <*|.x.|*> ^ |.p.| )
proof
let p be FinSequence of the carrier of F_Complex; ::_thesis: for x being Element of F_Complex holds
( |.(p ^ <*x*>).| = |.p.| ^ <*|.x.|*> & |.(<*x*> ^ p).| = <*|.x.|*> ^ |.p.| )
let x be Element of F_Complex; ::_thesis: ( |.(p ^ <*x*>).| = |.p.| ^ <*|.x.|*> & |.(<*x*> ^ p).| = <*|.x.|*> ^ |.p.| )
thus |.(p ^ <*x*>).| = |.p.| ^ |.<*x*>.| by Th12
.= |.p.| ^ <*|.x.|*> by Th9 ; ::_thesis: |.(<*x*> ^ p).| = <*|.x.|*> ^ |.p.|
thus |.(<*x*> ^ p).| = |.<*x*>.| ^ |.p.| by Th12
.= <*|.x.|*> ^ |.p.| by Th9 ; ::_thesis: verum
end;

theorem Th14: :: POLYNOM5:14
for p being FinSequence of the carrier of F_Complex holds |.(Sum p).| <= Sum |.p.|
proof
set D = the carrier of F_Complex;
defpred S1[ FinSequence of the carrier of F_Complex] means |.(Sum $1).| <= Sum |.$1.|;
A1: now__::_thesis:_for_p_being_FinSequence_of_the_carrier_of_F_Complex
for_x_being_Element_of_the_carrier_of_F_Complex_st_S1[p]_holds_
S1[p_^_<*x*>]
let p be FinSequence of the carrier of F_Complex; ::_thesis: for x being Element of the carrier of F_Complex st S1[p] holds
S1[p ^ <*x*>]
let x be Element of the carrier of F_Complex; ::_thesis: ( S1[p] implies S1[p ^ <*x*>] )
assume  S1[p] ; ::_thesis: S1[p ^ <*x*>]
then A2: |.(Sum p).| + |.x.| <= (Sum |.p.|) + |.x.| by XREAL_1:6;
 Sum (p ^ <*x*>) = (Sum p) + x by FVSUM_1:71;
then A3: |.(Sum (p ^ <*x*>)).| <= |.(Sum p).| + |.x.| by COMPLFLD:62;
(Sum |.p.|) + |.x.| = (Sum |.p.|) + (Sum <*|.x.|*>) by FINSOP_1:11
.= (Sum |.p.|) + (Sum |.<*x*>.|) by Th9
.= Sum (|.p.| ^ |.<*x*>.|) by RVSUM_1:75
.= Sum |.(p ^ <*x*>).| by Th12 ;
hence  S1[p ^ <*x*>] by A2, A3, XXREAL_0:2; ::_thesis: verum
end;
A4: S1[ <*> the carrier of F_Complex] by Th8, COMPLFLD:57, RLVECT_1:43, RVSUM_1:72;
thus  for p being FinSequence of the carrier of F_Complex holds S1[p] from FINSEQ_2:sch_2(A4, A1); ::_thesis: verum
end;

begin

definition
let L be non empty right_complementable Abelian add-associative right_zeroed commutative right_unital distributive doubleLoopStr ;
let p be Polynomial of L;
let n be Element of NAT ;
funcp `^ n ->  sequence of L equals :: POLYNOM5:def 2
(power (Polynom-Ring L)) . (p,n);
coherence
 (power (Polynom-Ring L)) . (p,n) is sequence of L
proof
reconsider p1 = p as Element of (Polynom-Ring L) by POLYNOM3:def_10;
 (power (Polynom-Ring L)) . (p1,n) is Element of (Polynom-Ring L) ;
hence  (power (Polynom-Ring L)) . (p,n) is sequence of L by POLYNOM3:def_10; ::_thesis: verum
end;
end;

:: deftheorem  defines `^ POLYNOM5:def_2_:_
 for L being non empty right_complementable Abelian add-associative right_zeroed commutative right_unital distributive doubleLoopStr
for p being Polynomial of L
for n being Element of NAT holds p `^ n = (power (Polynom-Ring L)) . (p,n);

registration
let L be non empty right_complementable Abelian add-associative right_zeroed commutative right_unital distributive doubleLoopStr ;
let p be Polynomial of L;
let n be Element of NAT ;
clusterp `^ n ->  finite-Support ;
coherence
 p `^ n is finite-Support
proof
reconsider p1 = p as Element of (Polynom-Ring L) by POLYNOM3:def_10;
 (power (Polynom-Ring L)) . (p1,n) is Polynomial of L by POLYNOM3:def_10;
hence  p `^ n is finite-Support ; ::_thesis: verum
end;
end;

theorem Th15: :: POLYNOM5:15
for L being non empty right_complementable Abelian add-associative right_zeroed commutative well-unital distributive doubleLoopStr
for p being Polynomial of L holds p `^ 0 = 1_. L
proof
let L be non empty right_complementable Abelian add-associative right_zeroed commutative well-unital distributive doubleLoopStr ; ::_thesis: for p being Polynomial of L holds p `^ 0 = 1_. L
let p be Polynomial of L; ::_thesis: p `^ 0 = 1_. L
reconsider p1 = p as Element of (Polynom-Ring L) by POLYNOM3:def_10;
thus p `^ 0 = (power (Polynom-Ring L)) . (p1,0)
.= 1_ (Polynom-Ring L) by GROUP_1:def_7
.= 1_. L by POLYNOM3:36 ; ::_thesis: verum
end;

theorem :: POLYNOM5:16
for L being non empty right_complementable Abelian add-associative right_zeroed commutative well-unital distributive doubleLoopStr
for p being Polynomial of L holds p `^ 1 = p
proof
let L be non empty right_complementable Abelian add-associative right_zeroed commutative well-unital distributive doubleLoopStr ; ::_thesis: for p being Polynomial of L holds p `^ 1 = p
let p be Polynomial of L; ::_thesis: p `^ 1 = p
reconsider p1 = p as Element of (Polynom-Ring L) by POLYNOM3:def_10;
thus p `^ 1 = (power (Polynom-Ring L)) . (p1,(0 + 1))
.= ((power (Polynom-Ring L)) . (p1,0)) * p1 by GROUP_1:def_7
.= (1_ (Polynom-Ring L)) * p1 by GROUP_1:def_7
.= p by GROUP_1:def_4 ; ::_thesis: verum
end;

theorem :: POLYNOM5:17
for L being non empty right_complementable Abelian add-associative right_zeroed commutative well-unital distributive doubleLoopStr
for p being Polynomial of L holds p `^ 2 = p *' p
proof
let L be non empty right_complementable Abelian add-associative right_zeroed commutative well-unital distributive doubleLoopStr ; ::_thesis: for p being Polynomial of L holds p `^ 2 = p *' p
let p be Polynomial of L; ::_thesis: p `^ 2 = p *' p
reconsider p1 = p as Element of (Polynom-Ring L) by POLYNOM3:def_10;
thus p `^ 2 = (power (Polynom-Ring L)) . (p1,(1 + 1))
.= ((power (Polynom-Ring L)) . (p1,(0 + 1))) * p1 by GROUP_1:def_7
.= (((power (Polynom-Ring L)) . (p1,0)) * p1) * p1 by GROUP_1:def_7
.= ((1_ (Polynom-Ring L)) * p1) * p1 by GROUP_1:def_7
.= p1 * p1 by GROUP_1:def_4
.= p *' p by POLYNOM3:def_10 ; ::_thesis: verum
end;

theorem :: POLYNOM5:18
for L being non empty right_complementable Abelian add-associative right_zeroed commutative well-unital distributive doubleLoopStr
for p being Polynomial of L holds p `^ 3 = (p *' p) *' p
proof
let L be non empty right_complementable Abelian add-associative right_zeroed commutative well-unital distributive doubleLoopStr ; ::_thesis: for p being Polynomial of L holds p `^ 3 = (p *' p) *' p
let p be Polynomial of L; ::_thesis: p `^ 3 = (p *' p) *' p
reconsider p1 = p as Element of (Polynom-Ring L) by POLYNOM3:def_10;
reconsider pp = p1 * p1 as Polynomial of L by POLYNOM3:def_10;
thus p `^ 3 = (power (Polynom-Ring L)) . (p1,(2 + 1))
.= ((power (Polynom-Ring L)) . (p1,(1 + 1))) * p1 by GROUP_1:def_7
.= (((power (Polynom-Ring L)) . (p1,(0 + 1))) * p1) * p1 by GROUP_1:def_7
.= ((((power (Polynom-Ring L)) . (p1,0)) * p1) * p1) * p1 by GROUP_1:def_7
.= (((1_ (Polynom-Ring L)) * p1) * p1) * p1 by GROUP_1:def_7
.= (p1 * p1) * p1 by GROUP_1:def_4
.= pp *' p by POLYNOM3:def_10
.= (p *' p) *' p by POLYNOM3:def_10 ; ::_thesis: verum
end;

theorem Th19: :: POLYNOM5:19
for L being non empty right_complementable Abelian add-associative right_zeroed commutative well-unital distributive doubleLoopStr
for p being Polynomial of L
for n being Element of NAT holds p `^ (n + 1) = (p `^ n) *' p
proof
let L be non empty right_complementable Abelian add-associative right_zeroed commutative well-unital distributive doubleLoopStr ; ::_thesis: for p being Polynomial of L
for n being Element of NAT holds p `^ (n + 1) = (p `^ n) *' p
let p be Polynomial of L; ::_thesis: for n being Element of NAT holds p `^ (n + 1) = (p `^ n) *' p
let n be Element of NAT ; ::_thesis: p `^ (n + 1) = (p `^ n) *' p
reconsider p1 = p as Element of (Polynom-Ring L) by POLYNOM3:def_10;
thus p `^ (n + 1) = ((power (Polynom-Ring L)) . (p1,n)) * p1 by GROUP_1:def_7
.= (p `^ n) *' p by POLYNOM3:def_10 ; ::_thesis: verum
end;

theorem Th20: :: POLYNOM5:20
for L being non empty right_complementable Abelian add-associative right_zeroed commutative well-unital distributive doubleLoopStr
for n being Element of NAT holds (0_. L) `^ (n + 1) = 0_. L
proof
let L be non empty right_complementable Abelian add-associative right_zeroed commutative well-unital distributive doubleLoopStr ; ::_thesis: for n being Element of NAT holds (0_. L) `^ (n + 1) = 0_. L
let n be Element of NAT ; ::_thesis: (0_. L) `^ (n + 1) = 0_. L
thus (0_. L) `^ (n + 1) = ((0_. L) `^ n) *' (0_. L) by Th19
.= 0_. L by POLYNOM3:34 ; ::_thesis: verum
end;

theorem :: POLYNOM5:21
for L being non empty right_complementable Abelian add-associative right_zeroed commutative well-unital distributive doubleLoopStr
for n being Element of NAT holds (1_. L) `^ n = 1_. L
proof
let L be non empty right_complementable Abelian add-associative right_zeroed commutative well-unital distributive doubleLoopStr ; ::_thesis: for n being Element of NAT holds (1_. L) `^ n = 1_. L
defpred S1[ Element of NAT ] means (1_. L) `^ $1 = 1_. L;
A1: now__::_thesis:_for_n_being_Element_of_NAT_st_S1[n]_holds_
S1[n_+_1]
let n be Element of NAT ; ::_thesis: ( S1[n] implies S1[n + 1] )
assume  S1[n] ; ::_thesis: S1[n + 1]
then (1_. L) `^ (n + 1) = (1_. L) *' (1_. L) by Th19
.= 1_. L by POLYNOM3:35 ;
hence  S1[n + 1] ; ::_thesis: verum
end;
A2: S1[ 0 ] by Th15;
thus  for n being Element of NAT holds S1[n] from NAT_1:sch_1(A2, A1); ::_thesis: verum
end;

theorem Th22: :: POLYNOM5:22
for L being Field
for p being Polynomial of L
for x being Element of L
for n being Element of NAT holds eval ((p `^ n),x) = (power L) . ((eval (p,x)),n)
proof
let L be Field; ::_thesis: for p being Polynomial of L
for x being Element of L
for n being Element of NAT holds eval ((p `^ n),x) = (power L) . ((eval (p,x)),n)
let p be Polynomial of L; ::_thesis: for x being Element of L
for n being Element of NAT holds eval ((p `^ n),x) = (power L) . ((eval (p,x)),n)
let x be Element of L; ::_thesis: for n being Element of NAT holds eval ((p `^ n),x) = (power L) . ((eval (p,x)),n)
defpred S1[ Element of NAT ] means  eval ((p `^ $1),x) = (power L) . ((eval (p,x)),$1);
A1: now__::_thesis:_for_n_being_Element_of_NAT_st_S1[n]_holds_
S1[n_+_1]
let n be Element of NAT ; ::_thesis: ( S1[n] implies S1[n + 1] )
assume A2: S1[n] ; ::_thesis: S1[n + 1]
eval ((p `^ (n + 1)),x) = eval (((p `^ n) *' p),x) by Th19
.= ((power L) . ((eval (p,x)),n)) * (eval (p,x)) by A2, POLYNOM4:24
.= (power L) . ((eval (p,x)),(n + 1)) by GROUP_1:def_7 ;
hence  S1[n + 1] ; ::_thesis: verum
end;
eval ((p `^ 0),x) = eval ((1_. L),x) by Th15
.= 1_ L by POLYNOM4:18
.= (power L) . ((eval (p,x)),0) by GROUP_1:def_7 ;
then A3: S1[ 0 ] ;
thus  for n being Element of NAT holds S1[n] from NAT_1:sch_1(A3, A1); ::_thesis: verum
end;

Lm2:  for L being non empty ZeroStr
for p being AlgSequence of L st len p > 0 holds
p . ((len p) -' 1) <> 0. L
proof
let L be non empty ZeroStr ; ::_thesis: for p being AlgSequence of L st len p > 0 holds
p . ((len p) -' 1) <> 0. L
let p be AlgSequence of L; ::_thesis: ( len p > 0 implies p . ((len p) -' 1) <> 0. L )
assume  len p > 0 ; ::_thesis: p . ((len p) -' 1) <> 0. L
then  ex k being Nat st len p = k + 1 by NAT_1:6;
then  len p = ((len p) -' 1) + 1 by NAT_D:34;
hence  p . ((len p) -' 1) <> 0. L by ALGSEQ_1:10; ::_thesis: verum
end;

theorem Th23: :: POLYNOM5:23
for L being domRing
for p being Polynomial of L st len p <> 0 holds
for n being Element of NAT holds len (p `^ n) = ((n * (len p)) - n) + 1
proof
let L be domRing; ::_thesis: for p being Polynomial of L st len p <> 0 holds
for n being Element of NAT holds len (p `^ n) = ((n * (len p)) - n) + 1
let p be Polynomial of L; ::_thesis: ( len p <> 0 implies for n being Element of NAT holds len (p `^ n) = ((n * (len p)) - n) + 1 )
defpred S1[ Element of NAT ] means  len (p `^ $1) = (($1 * (len p)) - $1) + 1;
assume A1: len p <> 0 ; ::_thesis: for n being Element of NAT holds len (p `^ n) = ((n * (len p)) - n) + 1
A2: now__::_thesis:_for_n_being_Element_of_NAT_st_S1[n]_holds_
S1[n_+_1]
 len p >= 0 + 1 by A1, NAT_1:13;
then  (len p) - 1 >= (0 + 1) - 1 by XREAL_1:9;
then A3: (len p) -' 1 = (len p) - 1 by XREAL_0:def_2;
A4: p . ((len p) -' 1) <> 0. L by A1, Lm2;
let n be Element of NAT ; ::_thesis: ( S1[n] implies S1[n + 1] )
assume A5: S1[n] ; ::_thesis: S1[n + 1]
 (n * ((len p) -' 1)) + 1 >= 0 + 1 by XREAL_1:6;
then  (p `^ n) . ((len (p `^ n)) -' 1) <> 0. L by A5, A3, Lm2;
then A6: ((p `^ n) . ((len (p `^ n)) -' 1)) * (p . ((len p) -' 1)) <> 0. L by A4, VECTSP_2:def_1;
len (p `^ (n + 1)) = len ((p `^ n) *' p) by Th19
.= ((((n * (len p)) - n) + 1) + (len p)) - 1 by A5, A6, POLYNOM4:10
.= (((n + 1) * (len p)) - (n + 1)) + 1 ;
hence  S1[n + 1] ; ::_thesis: verum
end;
len (p `^ 0) = len (1_. L) by Th15
.= ((0 * (len p)) - 0) + 1 by POLYNOM4:4 ;
then A7: S1[ 0 ] ;
thus  for n being Element of NAT holds S1[n] from NAT_1:sch_1(A7, A2); ::_thesis: verum
end;

definition
let L be non empty multMagma ;
let p be sequence of L;
let v be Element of L;
funcv * p ->  sequence of L means :Def3: :: POLYNOM5:def 3
 for n being Element of NAT holds it . n = v * (p . n);
existence
 ex b1 being sequence of L st
for n being Element of NAT holds b1 . n = v * (p . n)
proof
deffunc H1( Element of NAT ) ->  Element of the carrier of L = v * (p . $1);
consider r being sequence of L such that
A1: for n being Element of NAT holds r . n = H1(n) from FUNCT_2:sch_4();
take  r ; ::_thesis: for n being Element of NAT holds r . n = v * (p . n)
thus  for n being Element of NAT holds r . n = v * (p . n) by A1; ::_thesis: verum
end;
uniqueness
 for b1, b2 being sequence of L st ( for n being Element of NAT holds b1 . n = v * (p . n) ) & ( for n being Element of NAT holds b2 . n = v * (p . n) ) holds
b1 = b2
proof
let p1, p2 be sequence of L; ::_thesis: ( ( for n being Element of NAT holds p1 . n = v * (p . n) ) & ( for n being Element of NAT holds p2 . n = v * (p . n) ) implies p1 = p2 )
assume that
A2: for n being Element of NAT holds p1 . n = v * (p . n) and
A3: for n being Element of NAT holds p2 . n = v * (p . n) ; ::_thesis: p1 = p2
now__::_thesis:_for_k_being_Element_of_NAT_holds_p1_._k_=_p2_._k
let k be Element of NAT ; ::_thesis: p1 . k = p2 . k
thus p1 . k = v * (p . k) by A2
.= p2 . k by A3 ; ::_thesis: verum
end;
hence  p1 = p2 by FUNCT_2:63; ::_thesis: verum
end;
end;

:: deftheorem Def3 defines * POLYNOM5:def_3_:_
 for L being non empty multMagma
for p being sequence of L
for v being Element of L
for b4 being sequence of L holds
( b4 = v * p iff for n being Element of NAT holds b4 . n = v * (p . n) );

registration
let L be non empty right_complementable add-associative right_zeroed right-distributive doubleLoopStr ;
let p be Polynomial of L;
let v be Element of L;
clusterv * p ->  finite-Support ;
coherence
 v * p is finite-Support
proof
take s = len p; :: according to ALGSEQ_1:def_1 ::_thesis: for b1 being set holds
( not s <= b1 or (v * p) . b1 = 0. L )
let i be Nat; ::_thesis: ( not s <= i or (v * p) . i = 0. L )
assume A1: i >= s ; ::_thesis: (v * p) . i = 0. L
reconsider ii = i as Element of NAT by ORDINAL1:def_12;
thus (v * p) . i = v * (p . ii) by Def3
.= v * (0. L) by A1, ALGSEQ_1:8
.= 0. L by VECTSP_1:6 ; ::_thesis: verum
end;
end;

theorem Th24: :: POLYNOM5:24
for L being non empty right_complementable add-associative right_zeroed distributive doubleLoopStr
for p being Polynomial of L holds len ((0. L) * p) = 0
proof
let L be non empty right_complementable add-associative right_zeroed distributive doubleLoopStr ; ::_thesis: for p being Polynomial of L holds len ((0. L) * p) = 0
let p be Polynomial of L; ::_thesis: len ((0. L) * p) = 0
 0 is_at_least_length_of (0. L) * p
proof
let i be Nat; :: according to ALGSEQ_1:def_2 ::_thesis: ( not 0 <= i or ((0. L) * p) . i = 0. L )
assume  i >= 0 ; ::_thesis: ((0. L) * p) . i = 0. L
reconsider ii = i as Element of NAT by ORDINAL1:def_12;
thus ((0. L) * p) . i = (0. L) * (p . ii) by Def3
.= 0. L by VECTSP_1:7 ; ::_thesis: verum
end;
hence  len ((0. L) * p) = 0 by ALGSEQ_1:def_3; ::_thesis: verum
end;

theorem Th25: :: POLYNOM5:25
for L being non empty right_complementable almost_left_invertible add-associative right_zeroed associative commutative well-unital distributive doubleLoopStr
for p being Polynomial of L
for v being Element of L st v <> 0. L holds
len (v * p) = len p
proof
let L be non empty right_complementable almost_left_invertible add-associative right_zeroed associative commutative well-unital distributive doubleLoopStr ; ::_thesis: for p being Polynomial of L
for v being Element of L st v <> 0. L holds
len (v * p) = len p
let p be Polynomial of L; ::_thesis: for v being Element of L st v <> 0. L holds
len (v * p) = len p
let v be Element of L; ::_thesis: ( v <> 0. L implies len (v * p) = len p )
assume A1: v <> 0. L ; ::_thesis: len (v * p) = len p
A2: now__::_thesis:_for_n_being_Nat_st_n_is_at_least_length_of_v_*_p_holds_
len_p_<=_n
let n be Nat; ::_thesis: ( n is_at_least_length_of v * p implies len p <= n )
assume A3: n is_at_least_length_of v * p ; ::_thesis: len p <= n
 n is_at_least_length_of p
proof
let i be Nat; :: according to ALGSEQ_1:def_2 ::_thesis: ( not n <= i or p . i = 0. L )
reconsider i1 = i as Element of NAT by ORDINAL1:def_12;
assume  i >= n ; ::_thesis: p . i = 0. L
then  (v * p) . i = 0. L by A3, ALGSEQ_1:def_2;
then  v * (p . i1) = 0. L by Def3;
hence  p . i = 0. L by A1, VECTSP_1:12; ::_thesis: verum
end;
hence  len p <= n by ALGSEQ_1:def_3; ::_thesis: verum
end;
 len p is_at_least_length_of v * p
proof
let i be Nat; :: according to ALGSEQ_1:def_2 ::_thesis: ( not len p <= i or (v * p) . i = 0. L )
assume A4: i >= len p ; ::_thesis: (v * p) . i = 0. L
reconsider ii = i as Element of NAT by ORDINAL1:def_12;
thus (v * p) . i = v * (p . ii) by Def3
.= v * (0. L) by A4, ALGSEQ_1:8
.= 0. L by VECTSP_1:6 ; ::_thesis: verum
end;
hence  len (v * p) = len p by A2, ALGSEQ_1:def_3; ::_thesis: verum
end;

theorem Th26: :: POLYNOM5:26
for L being non empty right_complementable add-associative right_zeroed left-distributive doubleLoopStr
for p being sequence of L holds (0. L) * p = 0_. L
proof
let L be non empty right_complementable add-associative right_zeroed left-distributive doubleLoopStr ; ::_thesis: for p being sequence of L holds (0. L) * p = 0_. L
let p be sequence of L; ::_thesis: (0. L) * p = 0_. L
now__::_thesis:_for_n_being_Element_of_NAT_holds_(0_._L)_._n_=_(0._L)_*_(p_._n)
let n be Element of NAT ; ::_thesis: (0_. L) . n = (0. L) * (p . n)
thus (0_. L) . n = 0. L by FUNCOP_1:7
.= (0. L) * (p . n) by VECTSP_1:7 ; ::_thesis: verum
end;
hence  (0. L) * p = 0_. L by Def3; ::_thesis: verum
end;

theorem Th27: :: POLYNOM5:27
for L being non empty well-unital multLoopStr
for p being sequence of L holds (1. L) * p = p
proof
let L be non empty well-unital multLoopStr ; ::_thesis: for p being sequence of L holds (1. L) * p = p
let p be sequence of L; ::_thesis: (1. L) * p = p
 for n being Element of NAT holds p . n = (1. L) * (p . n) by VECTSP_1:def_8;
hence  (1. L) * p = p by Def3; ::_thesis: verum
end;

theorem Th28: :: POLYNOM5:28
for L being non empty right_complementable add-associative right_zeroed right-distributive doubleLoopStr
for v being Element of L holds v * (0_. L) = 0_. L
proof
let L be non empty right_complementable add-associative right_zeroed right-distributive doubleLoopStr ; ::_thesis: for v being Element of L holds v * (0_. L) = 0_. L
let v be Element of L; ::_thesis: v * (0_. L) = 0_. L
now__::_thesis:_for_n_being_Element_of_NAT_holds_(0_._L)_._n_=_v_*_((0_._L)_._n)
let n be Element of NAT ; ::_thesis: (0_. L) . n = v * ((0_. L) . n)
thus (0_. L) . n = 0. L by FUNCOP_1:7
.= v * (0. L) by VECTSP_1:6
.= v * ((0_. L) . n) by FUNCOP_1:7 ; ::_thesis: verum
end;
hence  v * (0_. L) = 0_. L by Def3; ::_thesis: verum
end;

theorem Th29: :: POLYNOM5:29
for L being non empty right_complementable add-associative right_zeroed right-distributive well-unital doubleLoopStr
for v being Element of L holds v * (1_. L) = <%v%>
proof
let L be non empty right_complementable add-associative right_zeroed right-distributive well-unital doubleLoopStr ; ::_thesis: for v being Element of L holds v * (1_. L) = <%v%>
let v be Element of L; ::_thesis: v * (1_. L) = <%v%>
now__::_thesis:_for_n_being_Element_of_NAT_holds_<%v%>_._n_=_v_*_((1_._L)_._n)
let n be Element of NAT ; ::_thesis: <%v%> . b1 = v * ((1_. L) . b1)
percases ( n = 0 or n <> 0 ) ;
supposeA1: n = 0 ; ::_thesis: <%v%> . b1 = v * ((1_. L) . b1)
hence <%v%> . n = v by ALGSEQ_1:def_5
.= v * (1. L) by VECTSP_1:def_4
.= v * ((1_. L) . n) by A1, POLYNOM3:30 ;
::_thesis: verum
end;
supposeA2: n <> 0 ; ::_thesis: <%v%> . b1 = v * ((1_. L) . b1)
A3: len <%v%> <= 1 by ALGSEQ_1:def_5;
 n >= 0 + 1 by A2, NAT_1:13;
hence <%v%> . n = 0. L by A3, ALGSEQ_1:8, XXREAL_0:2
.= v * (0. L) by VECTSP_1:6
.= v * ((1_. L) . n) by A2, POLYNOM3:30 ;
::_thesis: verum
end;
end;
end;
hence  v * (1_. L) = <%v%> by Def3; ::_thesis: verum
end;

theorem Th30: :: POLYNOM5:30
for L being non empty right_complementable almost_left_invertible add-associative right_zeroed associative commutative well-unital distributive doubleLoopStr
for p being Polynomial of L
for v, x being Element of L holds eval ((v * p),x) = v * (eval (p,x))
proof
let L be non empty right_complementable almost_left_invertible add-associative right_zeroed associative commutative well-unital distributive doubleLoopStr ; ::_thesis: for p being Polynomial of L
for v, x being Element of L holds eval ((v * p),x) = v * (eval (p,x))
let p be Polynomial of L; ::_thesis: for v, x being Element of L holds eval ((v * p),x) = v * (eval (p,x))
let v, x be Element of L; ::_thesis: eval ((v * p),x) = v * (eval (p,x))
consider F1 being FinSequence of the carrier of L such that
A1: eval (p,x) = Sum F1 and
A2: len F1 = len p and
A3: for n being Element of NAT st n in dom F1 holds
F1 . n = (p . (n -' 1)) * ((power L) . (x,(n -' 1))) by POLYNOM4:def_2;
consider F2 being FinSequence of the carrier of L such that
A4: eval ((v * p),x) = Sum F2 and
A5: len F2 = len (v * p) and
A6: for n being Element of NAT st n in dom F2 holds
F2 . n = ((v * p) . (n -' 1)) * ((power L) . (x,(n -' 1))) by POLYNOM4:def_2;
percases ( v <> 0. L or v = 0. L ) ;
suppose v <> 0. L ; ::_thesis: eval ((v * p),x) = v * (eval (p,x))
then  len F1 = len F2 by A2, A5, Th25;
then A7: dom F1 = dom F2 by FINSEQ_3:29;
now__::_thesis:_for_i_being_set_st_i_in_dom_F1_holds_
F2_/._i_=_v_*_(F1_/._i)
let i be set ; ::_thesis: ( i in dom F1 implies F2 /. i = v * (F1 /. i) )
assume A8: i in dom F1 ; ::_thesis: F2 /. i = v * (F1 /. i)
then reconsider i1 = i as Element of NAT ;
A9: (p . (i1 -' 1)) * ((power L) . (x,(i1 -' 1))) = F1 . i by A3, A8
.= F1 /. i by A8, PARTFUN1:def_6 ;
thus F2 /. i = F2 . i by A7, A8, PARTFUN1:def_6
.= ((v * p) . (i1 -' 1)) * ((power L) . (x,(i1 -' 1))) by A6, A7, A8
.= (v * (p . (i1 -' 1))) * ((power L) . (x,(i1 -' 1))) by Def3
.= v * (F1 /. i) by A9, GROUP_1:def_3 ; ::_thesis: verum
end;
then  F2 = v * F1 by A7, POLYNOM1:def_1;
hence  eval ((v * p),x) = v * (eval (p,x)) by A1, A4, POLYNOM1:12; ::_thesis: verum
end;
supposeA10: v = 0. L ; ::_thesis: eval ((v * p),x) = v * (eval (p,x))
hence  eval ((v * p),x) = eval ((0_. L),x) by Th26
.= 0. L by POLYNOM4:17
.= v * (eval (p,x)) by A10, VECTSP_1:7 ;
::_thesis: verum
end;
end;
end;

theorem Th31: :: POLYNOM5:31
for L being non empty right_complementable add-associative right_zeroed unital right-distributive doubleLoopStr
for p being Polynomial of L holds eval (p,(0. L)) = p . 0
proof
let L be non empty right_complementable add-associative right_zeroed unital right-distributive doubleLoopStr ; ::_thesis: for p being Polynomial of L holds eval (p,(0. L)) = p . 0
let p be Polynomial of L; ::_thesis: eval (p,(0. L)) = p . 0
consider F being FinSequence of the carrier of L such that
A1: eval (p,(0. L)) = Sum F and
A2: len F = len p and
A3: for n being Element of NAT st n in dom F holds
F . n = (p . (n -' 1)) * ((power L) . ((0. L),(n -' 1))) by POLYNOM4:def_2;
percases ( len F > 0 or len F = 0 ) ;
suppose len F > 0 ; ::_thesis: eval (p,(0. L)) = p . 0
then  0 + 1 <= len F by NAT_1:13;
then A4: 1 in dom F by FINSEQ_3:25;
now__::_thesis:_for_i_being_Element_of_NAT_st_i_in_dom_F_&_i_<>_1_holds_
F_/._i_=_0._L
let i be Element of NAT ; ::_thesis: ( i in dom F & i <> 1 implies F /. i = 0. L )
assume that
A5: i in dom F and
A6: i <> 1 ; ::_thesis: F /. i = 0. L
 0 + 1 <= i by A5, FINSEQ_3:25;
then  i > 0 + 1 by A6, XXREAL_0:1;
then  i - 1 > 0 by XREAL_1:20;
then A7: i -' 1 > 0 by XREAL_0:def_2;
thus F /. i = F . i by A5, PARTFUN1:def_6
.= (p . (i -' 1)) * ((power L) . ((0. L),(i -' 1))) by A3, A5
.= (p . (i -' 1)) * (0. L) by A7, VECTSP_1:36
.= 0. L by VECTSP_1:6 ; ::_thesis: verum
end;
hence  eval (p,(0. L)) = F /. 1 by A1, A4, POLYNOM2:3
.= F . 1 by A4, PARTFUN1:def_6
.= (p . (1 -' 1)) * ((power L) . ((0. L),(1 -' 1))) by A3, A4
.= (p . (1 -' 1)) * ((power L) . ((0. L),0)) by XREAL_1:232
.= (p . (1 -' 1)) * (1_ L) by GROUP_1:def_7
.= p . (1 -' 1) by GROUP_1:def_4
.= p . 0 by XREAL_1:232 ;
::_thesis: verum
end;
suppose len F = 0 ; ::_thesis: eval (p,(0. L)) = p . 0
then A8: p = 0_. L by A2, POLYNOM4:5;
hence  eval (p,(0. L)) = 0. L by POLYNOM4:17
.= p . 0 by A8, FUNCOP_1:7 ;
::_thesis: verum
end;
end;
end;

definition
let L be non empty ZeroStr ;
let z0, z1 be Element of L;
func<%z0,z1%> ->  sequence of L equals :: POLYNOM5:def 4
((0_. L) +* (0,z0)) +* (1,z1);
coherence
 ((0_. L) +* (0,z0)) +* (1,z1) is sequence of L ;
end;

:: deftheorem  defines <% POLYNOM5:def_4_:_
 for L being non empty ZeroStr
for z0, z1 being Element of L holds <%z0,z1%> = ((0_. L) +* (0,z0)) +* (1,z1);

theorem Th32: :: POLYNOM5:32
for L being non empty ZeroStr
for z0 being Element of L holds
( <%z0%> . 0 = z0 & ( for n being Element of NAT st n >= 1 holds
<%z0%> . n = 0. L ) )
proof
let L be non empty ZeroStr ; ::_thesis: for z0 being Element of L holds
( <%z0%> . 0 = z0 & ( for n being Element of NAT st n >= 1 holds
<%z0%> . n = 0. L ) )
let z0 be Element of L; ::_thesis: ( <%z0%> . 0 = z0 & ( for n being Element of NAT st n >= 1 holds
<%z0%> . n = 0. L ) )
thus  <%z0%> . 0 = z0 by ALGSEQ_1:def_5; ::_thesis: for n being Element of NAT st n >= 1 holds
<%z0%> . n = 0. L
let n be Element of NAT ; ::_thesis: ( n >= 1 implies <%z0%> . n = 0. L )
A1: len <%z0%> <= 1 by ALGSEQ_1:def_5;
assume  n >= 1 ; ::_thesis: <%z0%> . n = 0. L
hence  <%z0%> . n = 0. L by A1, ALGSEQ_1:8, XXREAL_0:2; ::_thesis: verum
end;

theorem Th33: :: POLYNOM5:33
for L being non empty ZeroStr
for z0 being Element of L st z0 <> 0. L holds
len <%z0%> = 1
proof
let L be non empty ZeroStr ; ::_thesis: for z0 being Element of L st z0 <> 0. L holds
len <%z0%> = 1
let z0 be Element of L; ::_thesis: ( z0 <> 0. L implies len <%z0%> = 1 )
assume  z0 <> 0. L ; ::_thesis: len <%z0%> = 1
then  <%z0%> . 0 <> 0. L by ALGSEQ_1:def_5;
then  <%z0%> <> <%(0. L)%> by ALGSEQ_1:def_5;
then  len <%z0%> <> 0 by ALGSEQ_1:14;
then A1: len <%z0%> >= 0 + 1 by NAT_1:13;
assume  len <%z0%> <> 1 ; ::_thesis: contradiction
then  len <%z0%> > 1 by A1, XXREAL_0:1;
hence  contradiction by ALGSEQ_1:def_5; ::_thesis: verum
end;

theorem Th34: :: POLYNOM5:34
for L being non empty ZeroStr holds <%(0. L)%> = 0_. L
proof
let L be non empty ZeroStr ; ::_thesis: <%(0. L)%> = 0_. L
 len <%(0. L)%> = 0 by ALGSEQ_1:14;
hence  <%(0. L)%> = 0_. L by POLYNOM4:5; ::_thesis: verum
end;

theorem Th35: :: POLYNOM5:35
for L being non empty right_complementable add-associative right_zeroed associative commutative well-unital distributive domRing-like doubleLoopStr
for x, y being Element of L holds <%x%> *' <%y%> = <%(x * y)%>
proof
let L be non empty right_complementable add-associative right_zeroed associative commutative well-unital distributive domRing-like doubleLoopStr ; ::_thesis: for x, y being Element of L holds <%x%> *' <%y%> = <%(x * y)%>
let x, y be Element of L; ::_thesis: <%x%> *' <%y%> = <%(x * y)%>
A1: len <%x%> <= 1 by ALGSEQ_1:def_5;
A2: len <%y%> <= 1 by ALGSEQ_1:def_5;
percases ( ( len <%x%> <> 0 & len <%y%> <> 0 ) or len <%x%> = 0 or len <%y%> = 0 ) ;
supposeA3: ( len <%x%> <> 0 & len <%y%> <> 0 ) ; ::_thesis: <%x%> *' <%y%> = <%(x * y)%>
 ( x <> 0. L & y <> 0. L )
proof
assume  ( x = 0. L or y = 0. L ) ; ::_thesis: contradiction
then  ( <%x%> = 0_. L or <%y%> = 0_. L ) by Th34;
hence  contradiction by A3, POLYNOM4:3; ::_thesis: verum
end;
then  x * y <> 0. L by VECTSP_2:def_1;
then A4: len <%(x * y)%> = 1 by Th33;
consider r being FinSequence of the carrier of L such that
A5: len r = 0 + 1 and
A6: (<%x%> *' <%y%>) . 0 = Sum r and
A7: for k being Element of NAT st k in dom r holds
r . k = (<%x%> . (k -' 1)) * (<%y%> . ((0 + 1) -' k)) by POLYNOM3:def_9;
 1 in dom r by A5, FINSEQ_3:25;
then r . 1 = (<%x%> . (1 -' 1)) * (<%y%> . ((0 + 1) -' 1)) by A7
.= (<%x%> . 0) * (<%y%> . (1 -' 1)) by XREAL_1:232
.= (<%x%> . 0) * (<%y%> . 0) by XREAL_1:232
.= (<%x%> . 0) * y by ALGSEQ_1:def_5
.= x * y by ALGSEQ_1:def_5 ;
then A8: r = <*(x * y)*> by A5, FINSEQ_1:40;
A9: now__::_thesis:_for_n_being_Nat_st_n_<_1_holds_
(<%x%>_*'_<%y%>)_._n_=_<%(x_*_y)%>_._n
let n be Nat; ::_thesis: ( n < 1 implies (<%x%> *' <%y%>) . n = <%(x * y)%> . n )
assume  n < 1 ; ::_thesis: (<%x%> *' <%y%>) . n = <%(x * y)%> . n
then  n < 0 + 1 ;
then A10: n = 0 by NAT_1:13;
hence (<%x%> *' <%y%>) . n = x * y by A6, A8, RLVECT_1:44
.= <%(x * y)%> . n by A10, ALGSEQ_1:def_5 ;
::_thesis: verum
end;
 ( <%x%> . ((len <%x%>) -' 1) <> 0. L & <%y%> . ((len <%y%>) -' 1) <> 0. L ) by A3, Lm2;
then A11: (<%x%> . ((len <%x%>) -' 1)) * (<%y%> . ((len <%y%>) -' 1)) <> 0. L by VECTSP_2:def_1;
 len <%y%> >= 0 + 1 by A3, NAT_1:13;
then A12: len <%y%> = 1 by A2, XXREAL_0:1;
 len <%x%> >= 0 + 1 by A3, NAT_1:13;
then  len <%x%> = 1 by A1, XXREAL_0:1;
then  len (<%x%> *' <%y%>) = (1 + 1) - 1 by A12, A11, POLYNOM4:10;
hence  <%x%> *' <%y%> = <%(x * y)%> by A9, A4, ALGSEQ_1:12; ::_thesis: verum
end;
supposeA13: len <%x%> = 0 ; ::_thesis: <%x%> *' <%y%> = <%(x * y)%>
then A14: x = 0. L by Th33;
 <%x%> = 0_. L by A13, POLYNOM4:5;
hence <%x%> *' <%y%> = 0_. L by POLYNOM4:2
.= <%(0. L)%> by Th34
.= <%(x * y)%> by A14, VECTSP_1:7 ;
::_thesis: verum
end;
supposeA15: len <%y%> = 0 ; ::_thesis: <%x%> *' <%y%> = <%(x * y)%>
then A16: y = 0. L by Th33;
 <%y%> = 0_. L by A15, POLYNOM4:5;
hence <%x%> *' <%y%> = 0_. L by POLYNOM3:34
.= <%(0. L)%> by Th34
.= <%(x * y)%> by A16, VECTSP_1:7 ;
::_thesis: verum
end;
end;
end;

theorem Th36: :: POLYNOM5:36
for L being non empty right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative well-unital distributive doubleLoopStr
for x being Element of L
for n being Element of NAT holds <%x%> `^ n = <%((power L) . (x,n))%>
proof
let L be non empty right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative well-unital distributive doubleLoopStr ; ::_thesis: for x being Element of L
for n being Element of NAT holds <%x%> `^ n = <%((power L) . (x,n))%>
let x be Element of L; ::_thesis: for n being Element of NAT holds <%x%> `^ n = <%((power L) . (x,n))%>
defpred S1[ Element of NAT ] means <%x%> `^ $1 = <%((power L) . (x,$1))%>;
A1: for n being Element of NAT st S1[n] holds
S1[n + 1]
proof
let n be Element of NAT ; ::_thesis: ( S1[n] implies S1[n + 1] )
assume  <%x%> `^ n = <%((power L) . (x,n))%> ; ::_thesis: S1[n + 1]
hence <%x%> `^ (n + 1) = <%((power L) . (x,n))%> *' <%x%> by Th19
.= <%(((power L) . (x,n)) * x)%> by Th35
.= <%((power L) . (x,(n + 1)))%> by GROUP_1:def_7 ;
::_thesis: verum
end;
<%x%> `^ 0 = 1_. L by Th15
.= (1. L) * (1_. L) by Th27
.= <%(1_ L)%> by Th29
.= <%((power L) . (x,0))%> by GROUP_1:def_7 ;
then A2: S1[ 0 ] ;
thus  for n being Element of NAT holds S1[n] from NAT_1:sch_1(A2, A1); ::_thesis: verum
end;

theorem :: POLYNOM5:37
for L being non empty right_complementable add-associative right_zeroed unital doubleLoopStr
for z0, x being Element of L holds eval (<%z0%>,x) = z0
proof
let L be non empty right_complementable add-associative right_zeroed unital doubleLoopStr ; ::_thesis: for z0, x being Element of L holds eval (<%z0%>,x) = z0
let z0, x be Element of L; ::_thesis: eval (<%z0%>,x) = z0
consider F being FinSequence of the carrier of L such that
A1: eval (<%z0%>,x) = Sum F and
A2: len F = len <%z0%> and
A3: for n being Element of NAT st n in dom F holds
F . n = (<%z0%> . (n -' 1)) * ((power L) . (x,(n -' 1))) by POLYNOM4:def_2;
A4: len F <= 1 by A2, ALGSEQ_1:def_5;
percases ( len F = 0 or len F = 1 ) by A4, NAT_1:25;
suppose len F = 0 ; ::_thesis: eval (<%z0%>,x) = z0
then A5: <%z0%> = 0_. L by A2, POLYNOM4:5;
hence  eval (<%z0%>,x) = 0. L by POLYNOM4:17
.= (0_. L) . 0 by FUNCOP_1:7
.= z0 by A5, Th32 ;
::_thesis: verum
end;
supposeA6: len F = 1 ; ::_thesis: eval (<%z0%>,x) = z0
then  0 + 1 in Seg (len F) by FINSEQ_1:4;
then  1 in dom F by FINSEQ_1:def_3;
then F . 1 = (<%z0%> . (1 -' 1)) * ((power L) . (x,(1 -' 1))) by A3
.= (<%z0%> . 0) * ((power L) . (x,(1 -' 1))) by XREAL_1:232
.= (<%z0%> . 0) * ((power L) . (x,0)) by XREAL_1:232
.= z0 * ((power L) . (x,0)) by Th32
.= z0 * (1_ L) by GROUP_1:def_7
.= z0 by GROUP_1:def_4 ;
then  F = <*z0*> by A6, FINSEQ_1:40;
hence  eval (<%z0%>,x) = z0 by A1, RLVECT_1:44; ::_thesis: verum
end;
end;
end;

theorem Th38: :: POLYNOM5:38
for L being non empty ZeroStr
for z0, z1 being Element of L holds
( <%z0,z1%> . 0 = z0 & <%z0,z1%> . 1 = z1 & ( for n being Nat st n >= 2 holds
<%z0,z1%> . n = 0. L ) )
proof
let L be non empty ZeroStr ; ::_thesis: for z0, z1 being Element of L holds
( <%z0,z1%> . 0 = z0 & <%z0,z1%> . 1 = z1 & ( for n being Nat st n >= 2 holds
<%z0,z1%> . n = 0. L ) )
let z0, z1 be Element of L; ::_thesis: ( <%z0,z1%> . 0 = z0 & <%z0,z1%> . 1 = z1 & ( for n being Nat st n >= 2 holds
<%z0,z1%> . n = 0. L ) )
 0 in NAT ;
then A1: 0 in dom (0_. L) by FUNCT_2:def_1;
thus <%z0,z1%> . 0 = ((0_. L) +* (0,z0)) . 0 by FUNCT_7:32
.= z0 by A1, FUNCT_7:31 ; ::_thesis: ( <%z0,z1%> . 1 = z1 & ( for n being Nat st n >= 2 holds
<%z0,z1%> . n = 0. L ) )
 1 in NAT ;
then  1 in dom ((0_. L) +* (0,z0)) by FUNCT_2:def_1;
hence  <%z0,z1%> . 1 = z1 by FUNCT_7:31; ::_thesis: for n being Nat st n >= 2 holds
<%z0,z1%> . n = 0. L
let n be Nat; ::_thesis: ( n >= 2 implies <%z0,z1%> . n = 0. L )
A2: n in NAT by ORDINAL1:def_12;
assume A3: n >= 2 ; ::_thesis: <%z0,z1%> . n = 0. L
then  n >= 1 + 1 ;
then  n > 0 + 1 by NAT_1:13;
hence <%z0,z1%> . n = ((0_. L) +* (0,z0)) . n by FUNCT_7:32
.= (0_. L) . n by A3, FUNCT_7:32
.= 0. L by A2, FUNCOP_1:7 ;
::_thesis: verum
end;

registration
let L be non empty ZeroStr ;
let z0, z1 be Element of L;
cluster<%z0,z1%> ->  finite-Support ;
coherence
 <%z0,z1%> is finite-Support
proof
take  2 ; :: according to ALGSEQ_1:def_1 ::_thesis: for b1 being set holds
( not 2 <= b1 or <%z0,z1%> . b1 = 0. L )
let n be Nat; ::_thesis: ( not 2 <= n or <%z0,z1%> . n = 0. L )
thus  ( not 2 <= n or <%z0,z1%> . n = 0. L ) by Th38; ::_thesis: verum
end;
end;

theorem Th39: :: POLYNOM5:39
for L being non empty ZeroStr
for z0, z1 being Element of L holds len <%z0,z1%> <= 2
proof
let L be non empty ZeroStr ; ::_thesis: for z0, z1 being Element of L holds len <%z0,z1%> <= 2
let z0, z1 be Element of L; ::_thesis: len <%z0,z1%> <= 2
 2 is_at_least_length_of <%z0,z1%>
proof
let n be Nat; :: according to ALGSEQ_1:def_2 ::_thesis: ( not 2 <= n or <%z0,z1%> . n = 0. L )
thus  ( not 2 <= n or <%z0,z1%> . n = 0. L ) by Th38; ::_thesis: verum
end;
hence  len <%z0,z1%> <= 2 by ALGSEQ_1:def_3; ::_thesis: verum
end;

theorem Th40: :: POLYNOM5:40
for L being non empty ZeroStr
for z0, z1 being Element of L st z1 <> 0. L holds
len <%z0,z1%> = 2
proof
let L be non empty ZeroStr ; ::_thesis: for z0, z1 being Element of L st z1 <> 0. L holds
len <%z0,z1%> = 2
let z0, z1 be Element of L; ::_thesis: ( z1 <> 0. L implies len <%z0,z1%> = 2 )
assume  z1 <> 0. L ; ::_thesis: len <%z0,z1%> = 2
then A1: <%z0,z1%> . 1 <> 0. L by Th38;
A2: now__::_thesis:_for_n_being_Nat_st_n_is_at_least_length_of_<%z0,z1%>_holds_
1_+_1_<=_n
let n be Nat; ::_thesis: ( n is_at_least_length_of <%z0,z1%> implies 1 + 1 <= n )
assume  n is_at_least_length_of <%z0,z1%> ; ::_thesis: 1 + 1 <= n
then  1 < n by A1, ALGSEQ_1:def_2;
hence  1 + 1 <= n by NAT_1:13; ::_thesis: verum
end;
 2 is_at_least_length_of <%z0,z1%>
proof
let n be Nat; :: according to ALGSEQ_1:def_2 ::_thesis: ( not 2 <= n or <%z0,z1%> . n = 0. L )
thus  ( not 2 <= n or <%z0,z1%> . n = 0. L ) by Th38; ::_thesis: verum
end;
hence  len <%z0,z1%> = 2 by A2, ALGSEQ_1:def_3; ::_thesis: verum
end;

theorem Th41: :: POLYNOM5:41
for L being non empty ZeroStr
for z0 being Element of L st z0 <> 0. L holds
len <%z0,(0. L)%> = 1
proof
let L be non empty ZeroStr ; ::_thesis: for z0 being Element of L st z0 <> 0. L holds
len <%z0,(0. L)%> = 1
let z0 be Element of L; ::_thesis: ( z0 <> 0. L implies len <%z0,(0. L)%> = 1 )
A1: 1 is_at_least_length_of <%z0,(0. L)%>
proof
let n be Nat; :: according to ALGSEQ_1:def_2 ::_thesis: ( not 1 <= n or <%z0,(0. L)%> . n = 0. L )
assume A2: n >= 1 ; ::_thesis: <%z0,(0. L)%> . n = 0. L
percases ( n = 1 or n > 1 ) by A2, XXREAL_0:1;
suppose n = 1 ; ::_thesis: <%z0,(0. L)%> . n = 0. L
hence  <%z0,(0. L)%> . n = 0. L by Th38; ::_thesis: verum
end;
suppose n > 1 ; ::_thesis: <%z0,(0. L)%> . n = 0. L
then  n >= 1 + 1 by NAT_1:13;
hence  <%z0,(0. L)%> . n = 0. L by Th38; ::_thesis: verum
end;
end;
end;
assume  z0 <> 0. L ; ::_thesis: len <%z0,(0. L)%> = 1
then A3: <%z0,(0. L)%> . 0 <> 0. L by Th38;
now__::_thesis:_for_n_being_Nat_st_n_is_at_least_length_of_<%z0,(0._L)%>_holds_
0_+_1_<=_n
let n be Nat; ::_thesis: ( n is_at_least_length_of <%z0,(0. L)%> implies 0 + 1 <= n )
assume  n is_at_least_length_of <%z0,(0. L)%> ; ::_thesis: 0 + 1 <= n
then  0 < n by A3, ALGSEQ_1:def_2;
hence  0 + 1 <= n by NAT_1:13; ::_thesis: verum
end;
hence  len <%z0,(0. L)%> = 1 by A1, ALGSEQ_1:def_3; ::_thesis: verum
end;

theorem Th42: :: POLYNOM5:42
for L being non empty ZeroStr holds <%(0. L),(0. L)%> = 0_. L
proof
let L be non empty ZeroStr ; ::_thesis: <%(0. L),(0. L)%> = 0_. L
 0 is_at_least_length_of <%(0. L),(0. L)%>
proof
let n be Nat; :: according to ALGSEQ_1:def_2 ::_thesis: ( not 0 <= n or <%(0. L),(0. L)%> . n = 0. L )
assume  n >= 0 ; ::_thesis: <%(0. L),(0. L)%> . n = 0. L
percases ( n = 0 or n > 0 ) ;
suppose n = 0 ; ::_thesis: <%(0. L),(0. L)%> . n = 0. L
hence  <%(0. L),(0. L)%> . n = 0. L by Th38; ::_thesis: verum
end;
suppose n > 0 ; ::_thesis: <%(0. L),(0. L)%> . n = 0. L
then A1: n >= 0 + 1 by NAT_1:13;
now__::_thesis:_<%(0._L),(0._L)%>_._n_=_0._L
percases ( n = 1 or n > 1 ) by A1, XXREAL_0:1;
suppose n = 1 ; ::_thesis: <%(0. L),(0. L)%> . n = 0. L
hence  <%(0. L),(0. L)%> . n = 0. L by Th38; ::_thesis: verum
end;
suppose n > 1 ; ::_thesis: <%(0. L),(0. L)%> . n = 0. L
then  n >= 1 + 1 by NAT_1:13;
hence  <%(0. L),(0. L)%> . n = 0. L by Th38; ::_thesis: verum
end;
end;
end;
hence  <%(0. L),(0. L)%> . n = 0. L ; ::_thesis: verum
end;
end;
end;
then  len <%(0. L),(0. L)%> = 0 by ALGSEQ_1:def_3;
hence  <%(0. L),(0. L)%> = 0_. L by POLYNOM4:5; ::_thesis: verum
end;

theorem :: POLYNOM5:43
for L being non empty ZeroStr
for z0 being Element of L holds <%z0,(0. L)%> = <%z0%>
proof
let L be non empty ZeroStr ; ::_thesis: for z0 being Element of L holds <%z0,(0. L)%> = <%z0%>
let z0 be Element of L; ::_thesis: <%z0,(0. L)%> = <%z0%>
percases ( z0 = 0. L or z0 <> 0. L ) ;
supposeA1: z0 = 0. L ; ::_thesis: <%z0,(0. L)%> = <%z0%>
hence <%z0,(0. L)%> = 0_. L by Th42
.= <%z0%> by A1, Th34 ;
::_thesis: verum
end;
supposeA2: z0 <> 0. L ; ::_thesis: <%z0,(0. L)%> = <%z0%>
then A3: len <%z0%> = 0 + 1 by Th33;
A4: now__::_thesis:_for_n_being_Nat_st_n_<_len_<%z0%>_holds_
<%z0,(0._L)%>_._n_=_<%z0%>_._n
let n be Nat; ::_thesis: ( n < len <%z0%> implies <%z0,(0. L)%> . n = <%z0%> . n )
assume  n < len <%z0%> ; ::_thesis: <%z0,(0. L)%> . n = <%z0%> . n
then A5: n = 0 by A3, NAT_1:13;
hence <%z0,(0. L)%> . n = z0 by Th38
.= <%z0%> . n by A5, ALGSEQ_1:def_5 ;
::_thesis: verum
end;
 len <%z0,(0. L)%> = 1 by A2, Th41;
hence  <%z0,(0. L)%> = <%z0%> by A2, A4, Th33, ALGSEQ_1:12; ::_thesis: verum
end;
end;
end;

theorem Th44: :: POLYNOM5:44
for L being non empty right_complementable add-associative right_zeroed unital left-distributive doubleLoopStr
for z0, z1, x being Element of L holds eval (<%z0,z1%>,x) = z0 + (z1 * x)
proof
let L be non empty right_complementable add-associative right_zeroed unital left-distributive doubleLoopStr ; ::_thesis: for z0, z1, x being Element of L holds eval (<%z0,z1%>,x) = z0 + (z1 * x)
let z0, z1, x be Element of L; ::_thesis: eval (<%z0,z1%>,x) = z0 + (z1 * x)
consider F being FinSequence of the carrier of L such that
A1: eval (<%z0,z1%>,x) = Sum F and
A2: len F = len <%z0,z1%> and
A3: for n being Element of NAT st n in dom F holds
F . n = (<%z0,z1%> . (n -' 1)) * ((power L) . (x,(n -' 1))) by POLYNOM4:def_2;
percases ( len F = 0 or len F = 1 or len F = 2 ) by A2, Th39, NAT_1:26;
suppose len F = 0 ; ::_thesis: eval (<%z0,z1%>,x) = z0 + (z1 * x)
then A4: <%z0,z1%> = 0_. L by A2, POLYNOM4:5;
hence  eval (<%z0,z1%>,x) = 0. L by POLYNOM4:17
.= (0_. L) . 0 by FUNCOP_1:7
.= z0 by A4, Th38
.= z0 + (0. L) by RLVECT_1:def_4
.= z0 + ((0. L) * x) by VECTSP_1:7
.= z0 + (((0_. L) . 1) * x) by FUNCOP_1:7
.= z0 + (z1 * x) by A4, Th38 ;
::_thesis: verum
end;
supposeA5: len F = 1 ; ::_thesis: eval (<%z0,z1%>,x) = z0 + (z1 * x)
then  0 + 1 in Seg (len F) by FINSEQ_1:4;
then  1 in dom F by FINSEQ_1:def_3;
then F . 1 = (<%z0,z1%> . (1 -' 1)) * ((power L) . (x,(1 -' 1))) by A3
.= (<%z0,z1%> . 0) * ((power L) . (x,(1 -' 1))) by XREAL_1:232
.= (<%z0,z1%> . 0) * ((power L) . (x,0)) by XREAL_1:232
.= z0 * ((power L) . (x,0)) by Th38
.= z0 * (1_ L) by GROUP_1:def_7
.= z0 by GROUP_1:def_4 ;
then  F = <*z0*> by A5, FINSEQ_1:40;
hence  eval (<%z0,z1%>,x) = z0 by A1, RLVECT_1:44
.= z0 + (0. L) by RLVECT_1:def_4
.= z0 + ((0. L) * x) by VECTSP_1:7
.= z0 + ((<%z0,z1%> . 1) * x) by A2, A5, ALGSEQ_1:8
.= z0 + (z1 * x) by Th38 ;
::_thesis: verum
end;
supposeA6: len F = 2 ; ::_thesis: eval (<%z0,z1%>,x) = z0 + (z1 * x)
then  1 in dom F by FINSEQ_3:25;
then A7: F . 1 = (<%z0,z1%> . (1 -' 1)) * ((power L) . (x,(1 -' 1))) by A3
.= (<%z0,z1%> . 0) * ((power L) . (x,(1 -' 1))) by XREAL_1:232
.= (<%z0,z1%> . 0) * ((power L) . (x,0)) by XREAL_1:232
.= z0 * ((power L) . (x,0)) by Th38
.= z0 * (1_ L) by GROUP_1:def_7
.= z0 by GROUP_1:def_4 ;
A8: 2 -' 1 = 2 - 1 by XREAL_0:def_2;
 2 in dom F by A6, FINSEQ_3:25;
then F . 2 = (<%z0,z1%> . (2 -' 1)) * ((power L) . (x,(2 -' 1))) by A3
.= z1 * ((power L) . (x,1)) by A8, Th38
.= z1 * x by GROUP_1:50 ;
then  F = <*z0,(z1 * x)*> by A6, A7, FINSEQ_1:44;
hence  eval (<%z0,z1%>,x) = z0 + (z1 * x) by A1, RLVECT_1:45; ::_thesis: verum
end;
end;
end;

theorem :: POLYNOM5:45
for L being non empty right_complementable add-associative right_zeroed left-distributive well-unital doubleLoopStr
for z0, z1, x being Element of L holds eval (<%z0,(0. L)%>,x) = z0
proof
let L be non empty right_complementable add-associative right_zeroed left-distributive well-unital doubleLoopStr ; ::_thesis: for z0, z1, x being Element of L holds eval (<%z0,(0. L)%>,x) = z0
let z0, z1, x be Element of L; ::_thesis: eval (<%z0,(0. L)%>,x) = z0
thus  eval (<%z0,(0. L)%>,x) = z0 + ((0. L) * x) by Th44
.= z0 + (0. L) by VECTSP_1:7
.= z0 by RLVECT_1:def_4 ; ::_thesis: verum
end;

theorem :: POLYNOM5:46
for L being non empty right_complementable add-associative right_zeroed unital left-distributive doubleLoopStr
for z0, z1, x being Element of L holds eval (<%(0. L),z1%>,x) = z1 * x
proof
let L be non empty right_complementable add-associative right_zeroed unital left-distributive doubleLoopStr ; ::_thesis: for z0, z1, x being Element of L holds eval (<%(0. L),z1%>,x) = z1 * x
let z0, z1, x be Element of L; ::_thesis: eval (<%(0. L),z1%>,x) = z1 * x
thus  eval (<%(0. L),z1%>,x) = (0. L) + (z1 * x) by Th44
.= z1 * x by RLVECT_1:4 ; ::_thesis: verum
end;

theorem Th47: :: POLYNOM5:47
for L being non empty right_complementable add-associative right_zeroed left-distributive well-unital doubleLoopStr
for z0, z1, x being Element of L holds eval (<%z0,(1. L)%>,x) = z0 + x
proof
let L be non empty right_complementable add-associative right_zeroed left-distributive well-unital doubleLoopStr ; ::_thesis: for z0, z1, x being Element of L holds eval (<%z0,(1. L)%>,x) = z0 + x
let z0, z1, x be Element of L; ::_thesis: eval (<%z0,(1. L)%>,x) = z0 + x
thus  eval (<%z0,(1. L)%>,x) = z0 + ((1. L) * x) by Th44
.= z0 + x by VECTSP_1:def_6 ; ::_thesis: verum
end;

theorem :: POLYNOM5:48
for L being non empty right_complementable add-associative right_zeroed left-distributive well-unital doubleLoopStr
for z0, z1, x being Element of L holds eval (<%(0. L),(1. L)%>,x) = x
proof
let L be non empty right_complementable add-associative right_zeroed left-distributive well-unital doubleLoopStr ; ::_thesis: for z0, z1, x being Element of L holds eval (<%(0. L),(1. L)%>,x) = x
let z0, z1, x be Element of L; ::_thesis: eval (<%(0. L),(1. L)%>,x) = x
thus  eval (<%(0. L),(1. L)%>,x) = (0. L) + ((1. L) * x) by Th44
.= (0. L) + x by VECTSP_1:def_8
.= x by RLVECT_1:4 ; ::_thesis: verum
end;

begin

definition
let L be non empty right_complementable Abelian add-associative right_zeroed commutative well-unital distributive doubleLoopStr ;
let p, q be Polynomial of L;
func Subst (p,q) ->  Polynomial of L means :Def5: :: POLYNOM5:def 5
 ex F being FinSequence of the carrier of (Polynom-Ring L) st
( it = Sum F & len F = len p & ( for n being Element of NAT st n in dom F holds
F . n = (p . (n -' 1)) * (q `^ (n -' 1)) ) );
existence
 ex b1 being Polynomial of L ex F being FinSequence of the carrier of (Polynom-Ring L) st
( b1 = Sum F & len F = len p & ( for n being Element of NAT st n in dom F holds
F . n = (p . (n -' 1)) * (q `^ (n -' 1)) ) )
proof
defpred S1[ Nat, set ] means $2 = (p . ($1 -' 1)) * (q `^ ($1 -' 1));
set k = len p;
A1: now__::_thesis:_for_n_being_Nat_st_n_in_Seg_(len_p)_holds_
ex_x_being_Element_of_(Polynom-Ring_L)_st_S1[n,x]
let n be Nat; ::_thesis: ( n in Seg (len p) implies ex x being Element of (Polynom-Ring L) st S1[n,x] )
assume  n in Seg (len p) ; ::_thesis: ex x being Element of (Polynom-Ring L) st S1[n,x]
reconsider x = (p . (n -' 1)) * (q `^ (n -' 1)) as Element of (Polynom-Ring L) by POLYNOM3:def_10;
take x = x; ::_thesis: S1[n,x]
thus  S1[n,x] ; ::_thesis: verum
end;
consider F being FinSequence of the carrier of (Polynom-Ring L) such that
A2: ( dom F = Seg (len p) & ( for n being Nat st n in Seg (len p) holds
S1[n,F . n] ) ) from FINSEQ_1:sch_5(A1);
reconsider r = Sum F as Polynomial of L by POLYNOM3:def_10;
take  r ; ::_thesis: ex F being FinSequence of the carrier of (Polynom-Ring L) st
( r = Sum F & len F = len p & ( for n being Element of NAT st n in dom F holds
F . n = (p . (n -' 1)) * (q `^ (n -' 1)) ) )
take  F ; ::_thesis: ( r = Sum F & len F = len p & ( for n being Element of NAT st n in dom F holds
F . n = (p . (n -' 1)) * (q `^ (n -' 1)) ) )
thus  ( r = Sum F & len F = len p & ( for n being Element of NAT st n in dom F holds
F . n = (p . (n -' 1)) * (q `^ (n -' 1)) ) ) by A2, FINSEQ_1:def_3; ::_thesis: verum
end;
uniqueness
 for b1, b2 being Polynomial of L st ex F being FinSequence of the carrier of (Polynom-Ring L) st
( b1 = Sum F & len F = len p & ( for n being Element of NAT st n in dom F holds
F . n = (p . (n -' 1)) * (q `^ (n -' 1)) ) ) & ex F being FinSequence of the carrier of (Polynom-Ring L) st
( b2 = Sum F & len F = len p & ( for n being Element of NAT st n in dom F holds
F . n = (p . (n -' 1)) * (q `^ (n -' 1)) ) ) holds
b1 = b2
proof
let y1, y2 be Polynomial of L; ::_thesis: ( ex F being FinSequence of the carrier of (Polynom-Ring L) st
( y1 = Sum F & len F = len p & ( for n being Element of NAT st n in dom F holds
F . n = (p . (n -' 1)) * (q `^ (n -' 1)) ) ) & ex F being FinSequence of the carrier of (Polynom-Ring L) st
( y2 = Sum F & len F = len p & ( for n being Element of NAT st n in dom F holds
F . n = (p . (n -' 1)) * (q `^ (n -' 1)) ) ) implies y1 = y2 )
given F1 being FinSequence of the carrier of (Polynom-Ring L) such that A3: y1 = Sum F1 and
A4: len F1 = len p and
A5: for n being Element of NAT st n in dom F1 holds
F1 . n = (p . (n -' 1)) * (q `^ (n -' 1)) ; ::_thesis: ( for F being FinSequence of the carrier of (Polynom-Ring L) holds
( not y2 = Sum F or not len F = len p or ex n being Element of NAT st
( n in dom F & not F . n = (p . (n -' 1)) * (q `^ (n -' 1)) ) ) or y1 = y2 )
given F2 being FinSequence of the carrier of (Polynom-Ring L) such that A6: y2 = Sum F2 and
A7: len F2 = len p and
A8: for n being Element of NAT st n in dom F2 holds
F2 . n = (p . (n -' 1)) * (q `^ (n -' 1)) ; ::_thesis: y1 = y2
A9: dom F1 = Seg (len F1) by FINSEQ_1:def_3;
now__::_thesis:_for_n_being_Nat_st_n_in_dom_F1_holds_
F1_._n_=_F2_._n
let n be Nat; ::_thesis: ( n in dom F1 implies F1 . n = F2 . n )
assume A10: n in dom F1 ; ::_thesis: F1 . n = F2 . n
then A11: n in dom F2 by A4, A7, A9, FINSEQ_1:def_3;
thus F1 . n = (p . (n -' 1)) * (q `^ (n -' 1)) by A5, A10
.= F2 . n by A8, A11 ; ::_thesis: verum
end;
hence  y1 = y2 by A3, A4, A6, A7, FINSEQ_2:9; ::_thesis: verum
end;
end;

:: deftheorem Def5 defines Subst POLYNOM5:def_5_:_
 for L being non empty right_complementable Abelian add-associative right_zeroed commutative well-unital distributive doubleLoopStr
for p, q, b4 being Polynomial of L holds
( b4 = Subst (p,q) iff ex F being FinSequence of the carrier of (Polynom-Ring L) st
( b4 = Sum F & len F = len p & ( for n being Element of NAT st n in dom F holds
F . n = (p . (n -' 1)) * (q `^ (n -' 1)) ) ) );

theorem Th49: :: POLYNOM5:49
for L being non empty right_complementable Abelian add-associative right_zeroed commutative well-unital distributive doubleLoopStr
for p being Polynomial of L holds Subst ((0_. L),p) = 0_. L
proof
let L be non empty right_complementable Abelian add-associative right_zeroed commutative well-unital distributive doubleLoopStr ; ::_thesis: for p being Polynomial of L holds Subst ((0_. L),p) = 0_. L
let p be Polynomial of L; ::_thesis: Subst ((0_. L),p) = 0_. L
consider F being FinSequence of the carrier of (Polynom-Ring L) such that
A1: Subst ((0_. L),p) = Sum F and
 len F = len (0_. L) and
A2: for n being Element of NAT st n in dom F holds
F . n = ((0_. L) . (n -' 1)) * (p `^ (n -' 1)) by Def5;
now__::_thesis:_for_n_being_Element_of_NAT_st_n_in_dom_F_holds_
F_._n_=_0._(Polynom-Ring_L)
let n be Element of NAT ; ::_thesis: ( n in dom F implies F . n = 0. (Polynom-Ring L) )
assume  n in dom F ; ::_thesis: F . n = 0. (Polynom-Ring L)
hence F . n = ((0_. L) . (n -' 1)) * (p `^ (n -' 1)) by A2
.= (0. L) * (p `^ (n -' 1)) by FUNCOP_1:7
.= 0_. L by Th26
.= 0. (Polynom-Ring L) by POLYNOM3:def_10 ;
::_thesis: verum
end;
hence  Subst ((0_. L),p) = 0. (Polynom-Ring L) by A1, POLYNOM3:1
.= 0_. L by POLYNOM3:def_10 ;
::_thesis: verum
end;

theorem :: POLYNOM5:50
for L being non empty right_complementable Abelian add-associative right_zeroed commutative well-unital distributive doubleLoopStr
for p being Polynomial of L holds Subst (p,(0_. L)) = <%(p . 0)%>
proof
let L be non empty right_complementable Abelian add-associative right_zeroed commutative well-unital distributive doubleLoopStr ; ::_thesis: for p being Polynomial of L holds Subst (p,(0_. L)) = <%(p . 0)%>
let p be Polynomial of L; ::_thesis: Subst (p,(0_. L)) = <%(p . 0)%>
consider F being FinSequence of the carrier of (Polynom-Ring L) such that
A1: Subst (p,(0_. L)) = Sum F and
A2: len F = len p and
A3: for n being Element of NAT st n in dom F holds
F . n = (p . (n -' 1)) * ((0_. L) `^ (n -' 1)) by Def5;
percases ( len F <> 0 or len F = 0 ) ;
suppose len F <> 0 ; ::_thesis: Subst (p,(0_. L)) = <%(p . 0)%>
then  0 + 1 <= len F by NAT_1:13;
then A4: 1 in dom F by FINSEQ_3:25;
now__::_thesis:_for_n_being_Element_of_NAT_st_n_in_dom_F_&_n_<>_1_holds_
F_/._n_=_0._(Polynom-Ring_L)
let n be Element of NAT ; ::_thesis: ( n in dom F & n <> 1 implies F /. n = 0. (Polynom-Ring L) )
assume that
A5: n in dom F and
A6: n <> 1 ; ::_thesis: F /. n = 0. (Polynom-Ring L)
 n >= 1 by A5, FINSEQ_3:25;
then A7: n > 0 + 1 by A6, XXREAL_0:1;
then  n >= 1 + 1 by NAT_1:13;
then A8: n - 2 >= (1 + 1) - 2 by XREAL_1:9;
 n - 1 >= 0 by A7, XREAL_1:19;
then A9: n -' 1 = (n - (1 + 1)) + 1 by XREAL_0:def_2
.= (n -' 2) + 1 by A8, XREAL_0:def_2 ;
thus F /. n = F . n by A5, PARTFUN1:def_6
.= (p . (n -' 1)) * ((0_. L) `^ (n -' 1)) by A3, A5
.= (p . (n -' 1)) * (0_. L) by A9, Th20
.= 0_. L by Th28
.= 0. (Polynom-Ring L) by POLYNOM3:def_10 ; ::_thesis: verum
end;
hence  Subst (p,(0_. L)) = F /. 1 by A1, A4, POLYNOM2:3
.= F . 1 by A4, PARTFUN1:def_6
.= (p . (1 -' 1)) * ((0_. L) `^ (1 -' 1)) by A3, A4
.= (p . (1 -' 1)) * ((0_. L) `^ 0) by XREAL_1:232
.= (p . 0) * ((0_. L) `^ 0) by XREAL_1:232
.= (p . 0) * (1_. L) by Th15
.= <%(p . 0)%> by Th29 ;
::_thesis: verum
end;
suppose len F = 0 ; ::_thesis: Subst (p,(0_. L)) = <%(p . 0)%>
then A10: p = 0_. L by A2, POLYNOM4:5;
hence  Subst (p,(0_. L)) = 0_. L by Th49
.= <%(0. L)%> by Th34
.= <%(p . 0)%> by A10, FUNCOP_1:7 ;
::_thesis: verum
end;
end;
end;

theorem :: POLYNOM5:51
for L being non empty right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative well-unital distributive doubleLoopStr
for p being Polynomial of L
for x being Element of L holds len (Subst (p,<%x%>)) <= 1
proof
let L be non empty right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative well-unital distributive doubleLoopStr ; ::_thesis: for p being Polynomial of L
for x being Element of L holds len (Subst (p,<%x%>)) <= 1
let p be Polynomial of L; ::_thesis: for x being Element of L holds len (Subst (p,<%x%>)) <= 1
let x be Element of L; ::_thesis: len (Subst (p,<%x%>)) <= 1
now__::_thesis:_len_(Subst_(p,<%x%>))_<=_1
now__::_thesis:_len_(Subst_(p,<%x%>))_<=_1
consider F being FinSequence of the carrier of (Polynom-Ring L) such that
A1: Subst (p,<%x%>) = Sum F and
 len F = len p and
A2: for n being Element of NAT st n in dom F holds
F . n = (p . (n -' 1)) * (<%x%> `^ (n -' 1)) by Def5;
defpred S1[ Nat] means  for p being Polynomial of L st p = Sum (F | $1) holds
len p <= 1;
A3: for n being Element of NAT st S1[n] holds
S1[n + 1]
proof
let n be Element of NAT ; ::_thesis: ( S1[n] implies S1[n + 1] )
reconsider F1 = Sum (F | n) as Polynomial of L by POLYNOM3:def_10;
reconsider maxFq = max ((len F1),(len ((p . n) * (<%x%> `^ n)))) as Element of NAT by FINSEQ_2:1;
A4: len ((p . n) * (<%x%> `^ n)) <= 1
proof
percases ( p . n <> 0. L or p . n = 0. L ) ;
suppose p . n <> 0. L ; ::_thesis: len ((p . n) * (<%x%> `^ n)) <= 1
then  len ((p . n) * (<%x%> `^ n)) = len (<%x%> `^ n) by Th25
.= len <%((power L) . (x,n))%> by Th36 ;
hence  len ((p . n) * (<%x%> `^ n)) <= 1 by ALGSEQ_1:def_5; ::_thesis: verum
end;
suppose p . n = 0. L ; ::_thesis: len ((p . n) * (<%x%> `^ n)) <= 1
hence  len ((p . n) * (<%x%> `^ n)) <= 1 by Th24; ::_thesis: verum
end;
end;
end;
assume A5: for q being Polynomial of L st q = Sum (F | n) holds
len q <= 1 ; ::_thesis: S1[n + 1]
then  len F1 <= 1 ;
then A6: maxFq <= 1 by A4, XXREAL_0:28;
let q be Polynomial of L; ::_thesis: ( q = Sum (F | (n + 1)) implies len q <= 1 )
assume A7: q = Sum (F | (n + 1)) ; ::_thesis: len q <= 1
A8: ( maxFq >= len F1 & maxFq >= len ((p . n) * (<%x%> `^ n)) ) by XXREAL_0:25;
now__::_thesis:_len_q_<=_1
percases ( n + 1 <= len F or n + 1 > len F ) ;
supposeA9: n + 1 <= len F ; ::_thesis: len q <= 1
 n + 1 >= 1 by NAT_1:11;
then A10: n + 1 in dom F by A9, FINSEQ_3:25;
then A11: F /. (n + 1) = F . (n + 1) by PARTFUN1:def_6
.= (p . ((n + 1) -' 1)) * (<%x%> `^ ((n + 1) -' 1)) by A2, A10
.= (p . n) * (<%x%> `^ ((n + 1) -' 1)) by NAT_D:34
.= (p . n) * (<%x%> `^ n) by NAT_D:34 ;
 F | (n + 1) = (F | n) ^ <*(F /. (n + 1))*> by A9, FINSEQ_5:82;
then q = (Sum (F | n)) + (F /. (n + 1)) by A7, FVSUM_1:71
.= F1 + ((p . n) * (<%x%> `^ n)) by A11, POLYNOM3:def_10 ;
then  len q <= maxFq by A8, POLYNOM4:6;
hence  len q <= 1 by A6, XXREAL_0:2; ::_thesis: verum
end;
supposeA12: n + 1 > len F ; ::_thesis: len q <= 1
then  n >= len F by NAT_1:13;
then A13: F | n = F by FINSEQ_1:58;
 F | (n + 1) = F by A12, FINSEQ_1:58;
hence  len q <= 1 by A5, A7, A13; ::_thesis: verum
end;
end;
end;
hence  len q <= 1 ; ::_thesis: verum
end;
A14: F | (len F) = F by FINSEQ_1:58;
A15: S1[ 0 ]
proof
let p be Polynomial of L; ::_thesis: ( p = Sum (F | 0) implies len p <= 1 )
A16: F | 0 = <*> the carrier of (Polynom-Ring L) ;
assume  p = Sum (F | 0) ; ::_thesis: len p <= 1
then p = 0. (Polynom-Ring L) by A16, RLVECT_1:43
.= 0_. L by POLYNOM3:def_10 ;
hence  len p <= 1 by POLYNOM4:3; ::_thesis: verum
end;
 for n being Element of NAT holds S1[n] from NAT_1:sch_1(A15, A3);
hence  len (Subst (p,<%x%>)) <= 1 by A1, A14; ::_thesis: verum
end;
hence  len (Subst (p,<%x%>)) <= 1 ; ::_thesis: verum
end;
hence  len (Subst (p,<%x%>)) <= 1 ; ::_thesis: verum
end;

theorem Th52: :: POLYNOM5:52
for L being Field
for p, q being Polynomial of L st len p <> 0 & len q > 1 holds
len (Subst (p,q)) = ((((len p) * (len q)) - (len p)) - (len q)) + 2
proof
let L be Field; ::_thesis: for p, q being Polynomial of L st len p <> 0 & len q > 1 holds
len (Subst (p,q)) = ((((len p) * (len q)) - (len p)) - (len q)) + 2
let p, q be Polynomial of L; ::_thesis: ( len p <> 0 & len q > 1 implies len (Subst (p,q)) = ((((len p) * (len q)) - (len p)) - (len q)) + 2 )
assume that
A1: len p <> 0 and
A2: len q > 1 ; ::_thesis: len (Subst (p,q)) = ((((len p) * (len q)) - (len p)) - (len q)) + 2
consider F being FinSequence of the carrier of (Polynom-Ring L) such that
A3: Subst (p,q) = Sum F and
A4: len F = len p and
A5: for n being Element of NAT st n in dom F holds
F . n = (p . (n -' 1)) * (q `^ (n -' 1)) by Def5;
A6: 0 + 1 <= len F by A1, A4, NAT_1:13;
then A7: 1 in dom F by FINSEQ_3:25;
reconsider k = ((((len p) * (len q)) - (len p)) - (len q)) + 1 as Element of NAT by A1, A2, Th1, INT_1:3;
 len p >= 0 + 1 by A1, NAT_1:13;
then A8: (len p) - 1 >= 0 by XREAL_1:19;
A9: len (q `^ ((len F) -' 1)) = ((((len p) -' 1) * (len q)) - ((len p) -' 1)) + 1 by A2, A4, Th23
.= ((((len p) -' 1) * (len q)) - ((len p) - 1)) + 1 by A8, XREAL_0:def_2
.= ((((len p) - 1) * (len q)) - ((len p) - 1)) + 1 by A8, XREAL_0:def_2
.= ((((len p) * (len q)) - (len p)) - (len q)) + (1 + 1) ;
A10: len (Subst (p,q)) >= ((((len p) * (len q)) - (len p)) - (len q)) + (1 + 1)
proof
set lF1 = (len F) -' 1;
set F1 = F | ((len F) -' 1);
reconsider sF1 = Sum (F | ((len F) -' 1)) as Polynomial of L by POLYNOM3:def_10;
A11: len F = ((len F) -' 1) + 1 by A6, XREAL_1:235;
then A12: F = (F | ((len F) -' 1)) ^ <*(F /. (len F))*> by FINSEQ_5:21;
then A13: Sum F = (Sum (F | ((len F) -' 1))) + (F /. (len F)) by FVSUM_1:71;
A14: len F = (len (F | ((len F) -' 1))) + 1 by A12, FINSEQ_2:16;
assume A15: len (Subst (p,q)) < ((((len p) * (len q)) - (len p)) - (len q)) + (1 + 1) ; ::_thesis: contradiction
then  len (Subst (p,q)) < k + 1 ;
then  len (Subst (p,q)) <= k by NAT_1:13;
then A16: (Subst (p,q)) . k = 0. L by ALGSEQ_1:8;
now__::_thesis:_contradiction
percases ( len (F | ((len F) -' 1)) <> {} or len (F | ((len F) -' 1)) = {} ) ;
supposeA17: len (F | ((len F) -' 1)) <> {} ; ::_thesis: contradiction
defpred S1[ Nat] means  for F2 being Polynomial of L st F2 = Sum ((F | ((len F) -' 1)) | $1) holds
len F2 <= ((($1 * (len q)) - (len q)) - $1) + 2;
A18: (F | ((len F) -' 1)) | (len (F | ((len F) -' 1))) = F | ((len F) -' 1) by FINSEQ_1:58;
A19: for n being non empty Nat st S1[n] holds
S1[n + 1]
proof
let n be non empty Nat; ::_thesis: ( S1[n] implies S1[n + 1] )
assume A20: for F2 being Polynomial of L st F2 = Sum ((F | ((len F) -' 1)) | n) holds
len F2 <= (((n * (len q)) - (len q)) - n) + 2 ; ::_thesis: S1[n + 1]
 len q >= 0 + (1 + 1) by A2, NAT_1:13;
then  (len q) - 2 >= 0 by XREAL_1:19;
then  (((n * (len q)) - n) + 1) + 0 <= (((n * (len q)) - n) + 1) + ((len q) - 2) by XREAL_1:7;
then  ( ((((n * (len q)) - (len q)) - n) + 2) + 0 <= ((((n * (len q)) - (len q)) - n) + 2) + 1 & (((n * (len q)) - n) + 1) - ((len q) - 2) <= ((n * (len q)) - n) + 1 ) by XREAL_1:6, XREAL_1:20;
then A21: (((n * (len q)) - (len q)) - n) + 2 <= ((n * (len q)) - n) + 1 by XXREAL_0:2;
reconsider F3 = Sum ((F | ((len F) -' 1)) | n) as Polynomial of L by POLYNOM3:def_10;
let F2 be Polynomial of L; ::_thesis: ( F2 = Sum ((F | ((len F) -' 1)) | (n + 1)) implies len F2 <= ((((n + 1) * (len q)) - (len q)) - (n + 1)) + 2 )
assume A22: F2 = Sum ((F | ((len F) -' 1)) | (n + 1)) ; ::_thesis: len F2 <= ((((n + 1) * (len q)) - (len q)) - (n + 1)) + 2
 len F3 <= (((n * (len q)) - (len q)) - n) + 2 by A20;
then A23: len F3 <= ((n * (len q)) - n) + 1 by A21, XXREAL_0:2;
now__::_thesis:_len_F2_<=_((((n_+_1)_*_(len_q))_-_(len_q))_-_(n_+_1))_+_2
percases ( n + 1 <= len (F | ((len F) -' 1)) or n + 1 > len (F | ((len F) -' 1)) ) ;
supposeA24: n + 1 <= len (F | ((len F) -' 1)) ; ::_thesis: len F2 <= ((((n + 1) * (len q)) - (len q)) - (n + 1)) + 2
reconsider nn = n as Element of NAT by ORDINAL1:def_12;
A25: n + 1 >= 1 by NAT_1:11;
reconsider maxFq = max ((len F3),(len ((p . nn) * (q `^ nn)))) as Element of NAT by FINSEQ_2:1;
A26: ( maxFq >= len F3 & maxFq >= len ((p . nn) * (q `^ nn)) ) by XXREAL_0:25;
 len ((p . nn) * (q `^ nn)) <= ((n * (len q)) - n) + 1
proof
percases ( p . n <> 0. L or p . n = 0. L ) ;
suppose p . n <> 0. L ; ::_thesis: len ((p . nn) * (q `^ nn)) <= ((n * (len q)) - n) + 1
then  len ((p . nn) * (q `^ nn)) = len (q `^ nn) by Th25;
hence  len ((p . nn) * (q `^ nn)) <= ((n * (len q)) - n) + 1 by A2, Th23; ::_thesis: verum
end;
supposeA27: p . n = 0. L ; ::_thesis: len ((p . nn) * (q `^ nn)) <= ((n * (len q)) - n) + 1
 len q >= 0 + 1 by A2;
then  (len q) - 1 >= 0 by XREAL_1:19;
then A28: n * ((len q) - 1) >= 0 ;
 n * (len q) <= (n * (len q)) + 1 by NAT_1:11;
then  (n * (len q)) - n <= ((n * (len q)) + 1) - n by XREAL_1:9;
hence  len ((p . nn) * (q `^ nn)) <= ((n * (len q)) - n) + 1 by A27, A28, Th24; ::_thesis: verum
end;
end;
end;
then A29: maxFq <= ((n * (len q)) - n) + 1 by A23, XXREAL_0:28;
 len (F | ((len F) -' 1)) <= len F by A14, NAT_1:11;
then  n + 1 <= len F by A24, XXREAL_0:2;
then A30: n + 1 in dom F by A25, FINSEQ_3:25;
A31: n + 1 in dom (F | ((len F) -' 1)) by A24, A25, FINSEQ_3:25;
then A32: (F | ((len F) -' 1)) /. (n + 1) = (F | ((len F) -' 1)) . (n + 1) by PARTFUN1:def_6
.= F . (n + 1) by A12, A31, FINSEQ_1:def_7
.= (p . ((n + 1) -' 1)) * (q `^ ((n + 1) -' 1)) by A5, A30
.= (p . nn) * (q `^ ((n + 1) -' 1)) by NAT_D:34
.= (p . nn) * (q `^ nn) by NAT_D:34 ;
 (F | ((len F) -' 1)) | (nn + 1) = ((F | ((len F) -' 1)) | nn) ^ <*((F | ((len F) -' 1)) /. (nn + 1))*> by A24, FINSEQ_5:82;
then F2 = (Sum ((F | ((len F) -' 1)) | n)) + ((F | ((len F) -' 1)) /. (n + 1)) by A22, FVSUM_1:71
.= F3 + ((p . nn) * (q `^ nn)) by A32, POLYNOM3:def_10 ;
then  len F2 <= maxFq by A26, POLYNOM4:6;
hence  len F2 <= ((((n + 1) * (len q)) - (len q)) - (n + 1)) + 2 by A29, XXREAL_0:2; ::_thesis: verum
end;
supposeA33: n + 1 > len (F | ((len F) -' 1)) ; ::_thesis: len F2 <= ((((n + 1) * (len q)) - (len q)) - (n + 1)) + 2
 - (len q) <= - 1 by A2, XREAL_1:24;
then  ((n * (len q)) - n) + (- (len q)) <= ((n * (len q)) - n) + (- 1) by XREAL_1:6;
then A34: (((n * (len q)) - (len q)) - n) + 2 <= ((((n + 1) * (len q)) - (len q)) - (n + 1)) + 2 by XREAL_1:6;
 n >= len (F | ((len F) -' 1)) by A33, NAT_1:13;
then A35: (F | ((len F) -' 1)) | n = F | ((len F) -' 1) by FINSEQ_1:58;
 (F | ((len F) -' 1)) | (n + 1) = F | ((len F) -' 1) by A33, FINSEQ_1:58;
then  len F2 <= (((n * (len q)) - (len q)) - n) + 2 by A20, A22, A35;
hence  len F2 <= ((((n + 1) * (len q)) - (len q)) - (n + 1)) + 2 by A34, XXREAL_0:2; ::_thesis: verum
end;
end;
end;
hence  len F2 <= ((((n + 1) * (len q)) - (len q)) - (n + 1)) + 2 ; ::_thesis: verum
end;
 0 + (len q) >= 1 + 1 by A2, NAT_1:13;
then  2 - (len q) <= 0 by XREAL_1:20;
then A36: (2 - (len q)) + k <= 0 + k by XREAL_1:6;
 0 + 1 <= len (F | ((len F) -' 1)) by A17, NAT_1:13;
then A37: 1 in dom (F | ((len F) -' 1)) by FINSEQ_3:25;
A38: S1[1]
proof
let F2 be Polynomial of L; ::_thesis: ( F2 = Sum ((F | ((len F) -' 1)) | 1) implies len F2 <= (((1 * (len q)) - (len q)) - 1) + 2 )
 (F | ((len F) -' 1)) | 1 = <*((F | ((len F) -' 1)) /. 1)*> by A17, CARD_1:27, FINSEQ_5:20;
then A39: Sum ((F | ((len F) -' 1)) | 1) = (F | ((len F) -' 1)) /. 1 by RLVECT_1:44
.= (F | ((len F) -' 1)) . 1 by A37, PARTFUN1:def_6
.= F . 1 by A12, A37, FINSEQ_1:def_7
.= (p . (1 -' 1)) * (q `^ (1 -' 1)) by A5, A7
.= (p . 0) * (q `^ (1 -' 1)) by XREAL_1:232
.= (p . 0) * (q `^ 0) by XREAL_1:232
.= (p . 0) * (1_. L) by Th15
.= <%(p . 0)%> by Th29 ;
assume  F2 = Sum ((F | ((len F) -' 1)) | 1) ; ::_thesis: len F2 <= (((1 * (len q)) - (len q)) - 1) + 2
hence  len F2 <= (((1 * (len q)) - (len q)) - 1) + 2 by A39, ALGSEQ_1:def_5; ::_thesis: verum
end;
 for n being non empty Nat holds S1[n] from NAT_1:sch_10(A38, A19);
then  len sF1 <= ((((len (F | ((len F) -' 1))) * (len q)) - (len q)) - (len (F | ((len F) -' 1)))) + 2 by A17, A18;
then A40: sF1 . k = 0. L by A4, A14, A36, ALGSEQ_1:8, XXREAL_0:2;
A41: len F in dom F by A6, FINSEQ_3:25;
then F /. (len F) = F . (len F) by PARTFUN1:def_6
.= (p . ((len F) -' 1)) * (q `^ ((len F) -' 1)) by A5, A41 ;
then  Subst (p,q) = sF1 + ((p . ((len F) -' 1)) * (q `^ ((len F) -' 1))) by A3, A13, POLYNOM3:def_10;
then A42: (Subst (p,q)) . k = (sF1 . k) + (((p . ((len F) -' 1)) * (q `^ ((len F) -' 1))) . k) by NORMSP_1:def_2
.= ((p . ((len F) -' 1)) * (q `^ ((len F) -' 1))) . k by A40, RLVECT_1:def_4
.= (p . ((len F) -' 1)) * ((q `^ ((len F) -' 1)) . k) by Def3 ;
 len (q `^ ((len F) -' 1)) = k + 1 by A9;
then A43: (q `^ ((len F) -' 1)) . k <> 0. L by ALGSEQ_1:10;
 p . ((len F) -' 1) <> 0. L by A4, A11, ALGSEQ_1:10;
hence  contradiction by A16, A42, A43, VECTSP_1:12; ::_thesis: verum
end;
supposeA44: len (F | ((len F) -' 1)) = {} ; ::_thesis: contradiction
A45: F /. 1 = F . 1 by A7, PARTFUN1:def_6
.= (p . (1 -' 1)) * (q `^ (1 -' 1)) by A5, A7
.= (p . 0) * (q `^ (1 -' 1)) by XREAL_1:232
.= (p . 0) * (q `^ 0) by XREAL_1:232
.= (p . 0) * (1_. L) by Th15
.= <%(p . 0)%> by Th29 ;
A46: 0. (Polynom-Ring L) = 0_. L by POLYNOM3:def_10;
A47: len F = 0 + 1 by A12, A44, FINSEQ_2:16;
then A48: p . 0 <> 0. L by A4, ALGSEQ_1:10;
 F | ((len F) -' 1) = <*> the carrier of (Polynom-Ring L) by A44;
then  Sum F = (0. (Polynom-Ring L)) + (F /. 1) by A13, A47, RLVECT_1:43
.= (0_. L) + <%(p . 0)%> by A45, A46, POLYNOM3:def_10
.= <%(p . 0)%> by POLYNOM3:28 ;
hence  contradiction by A3, A4, A15, A47, A48, Th33; ::_thesis: verum
end;
end;
end;
hence  contradiction ; ::_thesis: verum
end;
defpred S1[ Nat] means  for F1 being Polynomial of L st F1 = Sum (F | $1) holds
len F1 <= len (q `^ ($1 -' 1));
A49: for n being non empty Nat st S1[n] holds
S1[n + 1]
proof
let n be non empty Nat; ::_thesis: ( S1[n] implies S1[n + 1] )
assume A50: for F1 being Polynomial of L st F1 = Sum (F | n) holds
len F1 <= len (q `^ (n -' 1)) ; ::_thesis: S1[n + 1]
reconsider nn = n as Element of NAT by ORDINAL1:def_12;
reconsider F2 = Sum (F | n) as Polynomial of L by POLYNOM3:def_10;
let F1 be Polynomial of L; ::_thesis: ( F1 = Sum (F | (n + 1)) implies len F1 <= len (q `^ ((n + 1) -' 1)) )
assume A51: F1 = Sum (F | (n + 1)) ; ::_thesis: len F1 <= len (q `^ ((n + 1) -' 1))
 (n * (len q)) + ((len q) -' 1) >= n * (len q) by NAT_1:11;
then A52: (n * (len q)) - ((len q) -' 1) <= n * (len q) by XREAL_1:20;
 len q >= 0 + 1 by A2;
then  (len q) - 1 >= 0 by XREAL_1:19;
then  (n * (len q)) - ((len q) - 1) <= n * (len q) by A52, XREAL_0:def_2;
then  (((n * (len q)) - (len q)) + 1) - n <= (n * (len q)) - n by XREAL_1:9;
then A53: ((((n * (len q)) - (len q)) - n) + 1) + 1 <= ((n * (len q)) - n) + 1 by XREAL_1:6;
 n >= 0 + 1 by NAT_1:13;
then A54: n - 1 >= 0 by XREAL_1:19;
len (q `^ (n -' 1)) = (((n -' 1) * (len q)) - (n -' 1)) + 1 by A2, Th23
.= (((n - 1) * (len q)) - (n -' 1)) + 1 by A54, XREAL_0:def_2
.= (((n * (len q)) - (1 * (len q))) - (n - 1)) + 1 by A54, XREAL_0:def_2
.= ((((n * (len q)) - (len q)) - n) + 1) + 1 ;
then A55: len (q `^ (n -' 1)) <= len (q `^ nn) by A2, A53, Th23;
percases ( n + 1 <= len F or n + 1 > len F ) ;
supposeA56: n + 1 <= len F ; ::_thesis: len F1 <= len (q `^ ((n + 1) -' 1))
reconsider maxFq = max ((len F2),(len ((p . nn) * (q `^ nn)))) as Element of NAT by FINSEQ_2:1;
A57: len ((p . nn) * (q `^ nn)) <= len (q `^ nn)
proof
percases ( p . n <> 0. L or p . n = 0. L ) ;
suppose p . n <> 0. L ; ::_thesis: len ((p . nn) * (q `^ nn)) <= len (q `^ nn)
hence  len ((p . nn) * (q `^ nn)) <= len (q `^ nn) by Th25; ::_thesis: verum
end;
suppose p . n = 0. L ; ::_thesis: len ((p . nn) * (q `^ nn)) <= len (q `^ nn)
hence  len ((p . nn) * (q `^ nn)) <= len (q `^ nn) by Th24; ::_thesis: verum
end;
end;
end;
 len F2 <= len (q `^ (n -' 1)) by A50;
then  len F2 <= len (q `^ nn) by A55, XXREAL_0:2;
then A58: maxFq <= len (q `^ nn) by A57, XXREAL_0:28;
 F | (n + 1) = (F | n) ^ <*(F /. (nn + 1))*> by A56, FINSEQ_5:82;
then A59: F1 = (Sum (F | n)) + (F /. (n + 1)) by A51, FVSUM_1:71;
 n + 1 >= 1 by NAT_1:11;
then A60: n + 1 in dom F by A56, FINSEQ_3:25;
then F /. (n + 1) = F . (n + 1) by PARTFUN1:def_6
.= (p . ((n + 1) -' 1)) * (q `^ ((n + 1) -' 1)) by A5, A60
.= (p . nn) * (q `^ ((n + 1) -' 1)) by NAT_D:34
.= (p . nn) * (q `^ nn) by NAT_D:34 ;
then A61: F1 = F2 + ((p . nn) * (q `^ nn)) by A59, POLYNOM3:def_10;
 ( maxFq >= len F2 & maxFq >= len ((p . nn) * (q `^ nn)) ) by XXREAL_0:25;
then  len F1 <= maxFq by A61, POLYNOM4:6;
then  len F1 <= len (q `^ nn) by A58, XXREAL_0:2;
hence  len F1 <= len (q `^ ((n + 1) -' 1)) by NAT_D:34; ::_thesis: verum
end;
supposeA62: n + 1 > len F ; ::_thesis: len F1 <= len (q `^ ((n + 1) -' 1))
then  n >= len F by NAT_1:13;
then A63: F | n = F by FINSEQ_1:58;
 F | (n + 1) = F by A62, FINSEQ_1:58;
then  len F1 <= len (q `^ (n -' 1)) by A50, A51, A63;
then  len F1 <= len (q `^ nn) by A55, XXREAL_0:2;
hence  len F1 <= len (q `^ ((n + 1) -' 1)) by NAT_D:34; ::_thesis: verum
end;
end;
end;
A64: F | (len F) = F by FINSEQ_1:58;
A65: S1[1]
proof
let F1 be Polynomial of L; ::_thesis: ( F1 = Sum (F | 1) implies len F1 <= len (q `^ (1 -' 1)) )
 F | 1 = <*(F /. 1)*> by A1, A4, CARD_1:27, FINSEQ_5:20;
then A66: Sum (F | 1) = F /. 1 by RLVECT_1:44
.= F . 1 by A7, PARTFUN1:def_6
.= (p . (1 -' 1)) * (q `^ (1 -' 1)) by A5, A7
.= (p . 0) * (q `^ (1 -' 1)) by XREAL_1:232
.= (p . 0) * (q `^ 0) by XREAL_1:232
.= (p . 0) * (1_. L) by Th15
.= <%(p . 0)%> by Th29 ;
assume  F1 = Sum (F | 1) ; ::_thesis: len F1 <= len (q `^ (1 -' 1))
then  len F1 <= 1 by A66, ALGSEQ_1:def_5;
then  len F1 <= len (1_. L) by POLYNOM4:4;
then  len F1 <= len (q `^ 0) by Th15;
hence  len F1 <= len (q `^ (1 -' 1)) by XREAL_1:232; ::_thesis: verum
end;
 for n being non empty Nat holds S1[n] from NAT_1:sch_10(A65, A49);
then  len (Subst (p,q)) <= len (q `^ ((len F) -' 1)) by A1, A3, A4, A64;
hence  len (Subst (p,q)) = ((((len p) * (len q)) - (len p)) - (len q)) + 2 by A9, A10, XXREAL_0:1; ::_thesis: verum
end;

theorem Th53: :: POLYNOM5:53
for L being Field
for p, q being Polynomial of L
for x being Element of L holds eval ((Subst (p,q)),x) = eval (p,(eval (q,x)))
proof
let L be Field; ::_thesis: for p, q being Polynomial of L
for x being Element of L holds eval ((Subst (p,q)),x) = eval (p,(eval (q,x)))
let p, q be Polynomial of L; ::_thesis: for x being Element of L holds eval ((Subst (p,q)),x) = eval (p,(eval (q,x)))
let x be Element of L; ::_thesis: eval ((Subst (p,q)),x) = eval (p,(eval (q,x)))
consider F1 being FinSequence of the carrier of L such that
A1: eval (p,(eval (q,x))) = Sum F1 and
A2: len F1 = len p and
A3: for n being Element of NAT st n in dom F1 holds
F1 . n = (p . (n -' 1)) * ((power L) . ((eval (q,x)),(n -' 1))) by POLYNOM4:def_2;
consider F being FinSequence of the carrier of (Polynom-Ring L) such that
A4: Subst (p,q) = Sum F and
A5: len F = len p and
A6: for n being Element of NAT st n in dom F holds
F . n = (p . (n -' 1)) * (q `^ (n -' 1)) by Def5;
defpred S1[ Element of NAT ] means  for r being Polynomial of L st r = Sum (F | $1) holds
eval (r,x) = Sum (F1 | $1);
A7: for n being Element of NAT st S1[n] holds
S1[n + 1]
proof
let n be Element of NAT ; ::_thesis: ( S1[n] implies S1[n + 1] )
assume A8: for r being Polynomial of L st r = Sum (F | n) holds
eval (r,x) = Sum (F1 | n) ; ::_thesis: S1[n + 1]
let r be Polynomial of L; ::_thesis: ( r = Sum (F | (n + 1)) implies eval (r,x) = Sum (F1 | (n + 1)) )
assume A9: r = Sum (F | (n + 1)) ; ::_thesis: eval (r,x) = Sum (F1 | (n + 1))
percases ( n + 1 <= len F or n + 1 > len F ) ;
supposeA10: n + 1 <= len F ; ::_thesis: eval (r,x) = Sum (F1 | (n + 1))
then A11: F1 | (n + 1) = (F1 | n) ^ <*(F1 /. (n + 1))*> by A5, A2, FINSEQ_5:82;
 F | (n + 1) = (F | n) ^ <*(F /. (n + 1))*> by A10, FINSEQ_5:82;
then A12: r = (Sum (F | n)) + (F /. (n + 1)) by A9, FVSUM_1:71;
reconsider r1 = Sum (F | n) as Polynomial of L by POLYNOM3:def_10;
 n + 1 >= 1 by NAT_1:11;
then A13: n + 1 in dom F by A10, FINSEQ_3:25;
A14: dom F = dom F1 by A5, A2, FINSEQ_3:29;
then A15: (p . ((n + 1) -' 1)) * ((power L) . ((eval (q,x)),((n + 1) -' 1))) = F1 . (n + 1) by A3, A13
.= F1 /. (n + 1) by A13, A14, PARTFUN1:def_6 ;
F /. (n + 1) = F . (n + 1) by A13, PARTFUN1:def_6
.= (p . ((n + 1) -' 1)) * (q `^ ((n + 1) -' 1)) by A6, A13
.= (p . n) * (q `^ ((n + 1) -' 1)) by NAT_D:34
.= (p . n) * (q `^ n) by NAT_D:34 ;
then  r = r1 + ((p . n) * (q `^ n)) by A12, POLYNOM3:def_10;
hence  eval (r,x) = (eval (r1,x)) + (eval (((p . n) * (q `^ n)),x)) by POLYNOM4:19
.= (Sum (F1 | n)) + (eval (((p . n) * (q `^ n)),x)) by A8
.= (Sum (F1 | n)) + ((p . n) * (eval ((q `^ n),x))) by Th30
.= (Sum (F1 | n)) + ((p . n) * ((power L) . ((eval (q,x)),n))) by Th22
.= (Sum (F1 | n)) + ((p . ((n + 1) -' 1)) * ((power L) . ((eval (q,x)),n))) by NAT_D:34
.= (Sum (F1 | n)) + (F1 /. (n + 1)) by A15, NAT_D:34
.= Sum (F1 | (n + 1)) by A11, FVSUM_1:71 ;
::_thesis: verum
end;
supposeA16: n + 1 > len F ; ::_thesis: eval (r,x) = Sum (F1 | (n + 1))
then  n >= len F by NAT_1:13;
then A17: ( F | n = F & F1 | n = F1 ) by A5, A2, FINSEQ_1:58;
 ( F | (n + 1) = F & F1 | (n + 1) = F1 ) by A5, A2, A16, FINSEQ_1:58;
hence  eval (r,x) = Sum (F1 | (n + 1)) by A8, A9, A17; ::_thesis: verum
end;
end;
end;
A18: ( F | (len F) = F & F1 | (len F1) = F1 ) by FINSEQ_1:58;
A19: S1[ 0 ]
proof
let r be Polynomial of L; ::_thesis: ( r = Sum (F | 0) implies eval (r,x) = Sum (F1 | 0) )
A20: F | 0 = <*> the carrier of (Polynom-Ring L) ;
A21: F1 | 0 = <*> the carrier of L ;
assume  r = Sum (F | 0) ; ::_thesis: eval (r,x) = Sum (F1 | 0)
then r = 0. (Polynom-Ring L) by A20, RLVECT_1:43
.= 0_. L by POLYNOM3:def_10 ;
hence  eval (r,x) = 0. L by POLYNOM4:17
.= Sum (F1 | 0) by A21, RLVECT_1:43 ;
::_thesis: verum
end;
 for n being Element of NAT holds S1[n] from NAT_1:sch_1(A19, A7);
hence  eval ((Subst (p,q)),x) = eval (p,(eval (q,x))) by A4, A5, A1, A2, A18; ::_thesis: verum
end;

begin

definition
let L be non empty unital doubleLoopStr ;
let p be Polynomial of L;
let x be Element of L;
predx is_a_root_of p means :Def6: :: POLYNOM5:def 6
 eval (p,x) = 0. L;
end;

:: deftheorem Def6 defines is_a_root_of POLYNOM5:def_6_:_
 for L being non empty unital doubleLoopStr
for p being Polynomial of L
for x being Element of L holds
( x is_a_root_of p iff eval (p,x) = 0. L );

definition
let L be non empty unital doubleLoopStr ;
let p be Polynomial of L;
attrp is with_roots  means :Def7: :: POLYNOM5:def 7
 ex x being Element of L st x is_a_root_of p;
end;

:: deftheorem Def7 defines with_roots POLYNOM5:def_7_:_
 for L being non empty unital doubleLoopStr
for p being Polynomial of L holds
( p is with_roots iff ex x being Element of L st x is_a_root_of p );

theorem Th54: :: POLYNOM5:54
for L being non empty unital doubleLoopStr holds 0_. L is with_roots
proof
let L be non empty unital doubleLoopStr ; ::_thesis: 0_. L is with_roots
set x = the Element of L;
take  the Element of L ; :: according to POLYNOM5:def_7 ::_thesis: the Element of L is_a_root_of 0_. L
thus  eval ((0_. L), the Element of L) = 0. L by POLYNOM4:17; :: according to POLYNOM5:def_6 ::_thesis: verum
end;

registration
let L be non empty unital doubleLoopStr ;
cluster 0_. L ->  with_roots ;
coherence
 0_. L is with_roots by Th54;
end;

theorem :: POLYNOM5:55
for L being non empty unital doubleLoopStr
for x being Element of L holds x is_a_root_of 0_. L
proof
let L be non empty unital doubleLoopStr ; ::_thesis: for x being Element of L holds x is_a_root_of 0_. L
let x be Element of L; ::_thesis: x is_a_root_of 0_. L
thus  eval ((0_. L),x) = 0. L by POLYNOM4:17; :: according to POLYNOM5:def_6 ::_thesis: verum
end;

registration
let L be non empty unital doubleLoopStr ;
cluster Relation-like NAT -defined the carrier of L -valued Function-like non empty total quasi_total finite-Support with_roots for Element of K27(K28(NAT, the carrier of L));
existence
 ex b1 being Polynomial of L st b1 is with_roots
proof
take  0_. L ; ::_thesis: 0_. L is with_roots
thus  0_. L is with_roots ; ::_thesis: verum
end;
end;

definition
let L be non empty unital doubleLoopStr ;
attrL is algebraic-closed  means :Def8: :: POLYNOM5:def 8
 for p being Polynomial of L st len p > 1 holds
p is with_roots ;
end;

:: deftheorem Def8 defines algebraic-closed POLYNOM5:def_8_:_
 for L being non empty unital doubleLoopStr holds
( L is algebraic-closed iff for p being Polynomial of L st len p > 1 holds
p is with_roots );

definition
let L be non empty unital doubleLoopStr ;
let p be Polynomial of L;
func Roots p ->  Subset of L means :Def9: :: POLYNOM5:def 9
 for x being Element of L holds
( x in it iff x is_a_root_of p );
existence
 ex b1 being Subset of L st
for x being Element of L holds
( x in b1 iff x is_a_root_of p )
proof
  {  x where x is Element of L : x is_a_root_of p  }  c= the carrier of L
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in  {  x where x is Element of L : x is_a_root_of p  }  or y in the carrier of L )
assume  y in  {  x where x is Element of L : x is_a_root_of p  }  ; ::_thesis: y in the carrier of L
then  ex x being Element of L st
( x = y & x is_a_root_of p ) ;
hence  y in the carrier of L ; ::_thesis: verum
end;
then reconsider X =  {  x where x is Element of L : x is_a_root_of p  }  as Subset of L ;
take  X ; ::_thesis: for x being Element of L holds
( x in X iff x is_a_root_of p )
let x be Element of L; ::_thesis: ( x in X iff x is_a_root_of p )
thus  ( x in X implies x is_a_root_of p ) ::_thesis: ( x is_a_root_of p implies x in X )
proof
assume  x in X ; ::_thesis: x is_a_root_of p
then  ex y being Element of L st
( x = y & y is_a_root_of p ) ;
hence  x is_a_root_of p ; ::_thesis: verum
end;
assume  x is_a_root_of p ; ::_thesis: x in X
hence  x in X ; ::_thesis: verum
end;
uniqueness
 for b1, b2 being Subset of L st ( for x being Element of L holds
( x in b1 iff x is_a_root_of p ) ) & ( for x being Element of L holds
( x in b2 iff x is_a_root_of p ) ) holds
b1 = b2
proof
let X1, X2 be Subset of L; ::_thesis: ( ( for x being Element of L holds
( x in X1 iff x is_a_root_of p ) ) & ( for x being Element of L holds
( x in X2 iff x is_a_root_of p ) ) implies X1 = X2 )
assume that
A1: for x being Element of L holds
( x in X1 iff x is_a_root_of p ) and
A2: for x being Element of L holds
( x in X2 iff x is_a_root_of p ) ; ::_thesis: X1 = X2
thus  X1 c= X2 :: according to XBOOLE_0:def_10 ::_thesis: X2 c= X1
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in X1 or x in X2 )
assume A3: x in X1 ; ::_thesis: x in X2
then reconsider y = x as Element of L ;
 y is_a_root_of p by A1, A3;
hence  x in X2 by A2; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in X2 or x in X1 )
assume A4: x in X2 ; ::_thesis: x in X1
then reconsider y = x as Element of L ;
 y is_a_root_of p by A2, A4;
hence  x in X1 by A1; ::_thesis: verum
end;
end;

:: deftheorem Def9 defines Roots POLYNOM5:def_9_:_
 for L being non empty unital doubleLoopStr
for p being Polynomial of L
for b3 being Subset of L holds
( b3 = Roots p iff for x being Element of L holds
( x in b3 iff x is_a_root_of p ) );

definition
let L be non empty almost_left_invertible associative commutative well-unital distributive doubleLoopStr ;
let p be Polynomial of L;
func NormPolynomial p ->  sequence of L means :Def10: :: POLYNOM5:def 10
 for n being Element of NAT holds it . n = (p . n) / (p . ((len p) -' 1));
existence
 ex b1 being sequence of L st
for n being Element of NAT holds b1 . n = (p . n) / (p . ((len p) -' 1))
proof
deffunc H1( Element of NAT ) ->  Element of the carrier of L = (p . $1) / (p . ((len p) -' 1));
consider q being sequence of L such that
A1: for n being Element of NAT holds q . n = H1(n) from FUNCT_2:sch_4();
take  q ; ::_thesis: for n being Element of NAT holds q . n = (p . n) / (p . ((len p) -' 1))
thus  for n being Element of NAT holds q . n = (p . n) / (p . ((len p) -' 1)) by A1; ::_thesis: verum
end;
uniqueness
 for b1, b2 being sequence of L st ( for n being Element of NAT holds b1 . n = (p . n) / (p . ((len p) -' 1)) ) & ( for n being Element of NAT holds b2 . n = (p . n) / (p . ((len p) -' 1)) ) holds
b1 = b2
proof
let p1, p2 be sequence of L; ::_thesis: ( ( for n being Element of NAT holds p1 . n = (p . n) / (p . ((len p) -' 1)) ) & ( for n being Element of NAT holds p2 . n = (p . n) / (p . ((len p) -' 1)) ) implies p1 = p2 )
assume that
A2: for n being Element of NAT holds p1 . n = (p . n) / (p . ((len p) -' 1)) and
A3: for n being Element of NAT holds p2 . n = (p . n) / (p . ((len p) -' 1)) ; ::_thesis: p1 = p2
now__::_thesis:_for_n_being_Element_of_NAT_holds_p1_._n_=_p2_._n
let n be Element of NAT ; ::_thesis: p1 . n = p2 . n
thus p1 . n = (p . n) / (p . ((len p) -' 1)) by A2
.= p2 . n by A3 ; ::_thesis: verum
end;
hence  p1 = p2 by FUNCT_2:63; ::_thesis: verum
end;
end;

:: deftheorem Def10 defines NormPolynomial POLYNOM5:def_10_:_
 for L being non empty almost_left_invertible associative commutative well-unital distributive doubleLoopStr
for p being Polynomial of L
for b3 being sequence of L holds
( b3 = NormPolynomial p iff for n being Element of NAT holds b3 . n = (p . n) / (p . ((len p) -' 1)) );

registration
let L be non empty right_complementable almost_left_invertible add-associative right_zeroed associative commutative well-unital distributive doubleLoopStr ;
let p be Polynomial of L;
cluster NormPolynomial p ->  finite-Support ;
coherence
 NormPolynomial p is finite-Support
proof
now__::_thesis:_for_n_being_Nat_st_n_>=_len_p_holds_
(NormPolynomial_p)_._n_=_0._L
let n be Nat; ::_thesis: ( n >= len p implies (NormPolynomial p) . n = 0. L )
assume A1: n >= len p ; ::_thesis: (NormPolynomial p) . n = 0. L
reconsider nn = n as Element of NAT by ORDINAL1:def_12;
thus (NormPolynomial p) . n = (p . nn) / (p . ((len p) -' 1)) by Def10
.= (0. L) / (p . ((len p) -' 1)) by A1, ALGSEQ_1:8
.= (0. L) * ((p . ((len p) -' 1)) ") by VECTSP_1:def_11
.= 0. L by VECTSP_1:7 ; ::_thesis: verum
end;
hence  NormPolynomial p is finite-Support by ALGSEQ_1:def_1; ::_thesis: verum
end;
end;

theorem Th56: :: POLYNOM5:56
for L being non empty almost_left_invertible associative commutative well-unital distributive doubleLoopStr
for p being Polynomial of L st len p <> 0 holds
(NormPolynomial p) . ((len p) -' 1) = 1. L
proof
let L be non empty almost_left_invertible associative commutative well-unital distributive doubleLoopStr ; ::_thesis: for p being Polynomial of L st len p <> 0 holds
(NormPolynomial p) . ((len p) -' 1) = 1. L
let p be Polynomial of L; ::_thesis: ( len p <> 0 implies (NormPolynomial p) . ((len p) -' 1) = 1. L )
assume  len p <> 0 ; ::_thesis: (NormPolynomial p) . ((len p) -' 1) = 1. L
then  len p >= 0 + 1 by NAT_1:13;
then  len p = ((len p) -' 1) + 1 by XREAL_1:235;
then A1: p . ((len p) -' 1) <> 0. L by ALGSEQ_1:10;
thus (NormPolynomial p) . ((len p) -' 1) = (p . ((len p) -' 1)) / (p . ((len p) -' 1)) by Def10
.= (p . ((len p) -' 1)) * ((p . ((len p) -' 1)) ") by VECTSP_1:def_11
.= 1. L by A1, VECTSP_1:def_10 ; ::_thesis: verum
end;

theorem Th57: :: POLYNOM5:57
for L being Field
for p being Polynomial of L st len p <> 0 holds
len (NormPolynomial p) = len p
proof
let L be Field; ::_thesis: for p being Polynomial of L st len p <> 0 holds
len (NormPolynomial p) = len p
let p be Polynomial of L; ::_thesis: ( len p <> 0 implies len (NormPolynomial p) = len p )
assume  len p <> 0 ; ::_thesis: len (NormPolynomial p) = len p
then  len p >= 0 + 1 by NAT_1:13;
then  len p = ((len p) -' 1) + 1 by XREAL_1:235;
then  p . ((len p) -' 1) <> 0. L by ALGSEQ_1:10;
then A1: (p . ((len p) -' 1)) " <> 0. L by VECTSP_1:25;
A2: now__::_thesis:_for_n_being_Nat_st_n_is_at_least_length_of_NormPolynomial_p_holds_
len_p_<=_n
let n be Nat; ::_thesis: ( n is_at_least_length_of NormPolynomial p implies len p <= n )
assume A3: n is_at_least_length_of NormPolynomial p ; ::_thesis: len p <= n
 n is_at_least_length_of p
proof
let i be Nat; :: according to ALGSEQ_1:def_2 ::_thesis: ( not n <= i or p . i = 0. L )
reconsider ii = i as Element of NAT by ORDINAL1:def_12;
assume  i >= n ; ::_thesis: p . i = 0. L
then  (NormPolynomial p) . i = 0. L by A3, ALGSEQ_1:def_2;
then  (p . ii) / (p . ((len p) -' 1)) = 0. L by Def10;
then  (p . ii) * ((p . ((len p) -' 1)) ") = 0. L by VECTSP_1:def_11;
hence  p . i = 0. L by A1, VECTSP_1:12; ::_thesis: verum
end;
hence  len p <= n by ALGSEQ_1:def_3; ::_thesis: verum
end;
 len p is_at_least_length_of NormPolynomial p
proof
let n be Nat; :: according to ALGSEQ_1:def_2 ::_thesis: ( not len p <= n or (NormPolynomial p) . n = 0. L )
assume A4: n >= len p ; ::_thesis: (NormPolynomial p) . n = 0. L
reconsider nn = n as Element of NAT by ORDINAL1:def_12;
thus (NormPolynomial p) . n = (p . nn) / (p . ((len p) -' 1)) by Def10
.= (0. L) / (p . ((len p) -' 1)) by A4, ALGSEQ_1:8
.= (0. L) * ((p . ((len p) -' 1)) ") by VECTSP_1:def_11
.= 0. L by VECTSP_1:7 ; ::_thesis: verum
end;
hence  len (NormPolynomial p) = len p by A2, ALGSEQ_1:def_3; ::_thesis: verum
end;

theorem Th58: :: POLYNOM5:58
for L being Field
for p being Polynomial of L st len p <> 0 holds
for x being Element of L holds eval ((NormPolynomial p),x) = (eval (p,x)) / (p . ((len p) -' 1))
proof
let L be Field; ::_thesis: for p being Polynomial of L st len p <> 0 holds
for x being Element of L holds eval ((NormPolynomial p),x) = (eval (p,x)) / (p . ((len p) -' 1))
let p be Polynomial of L; ::_thesis: ( len p <> 0 implies for x being Element of L holds eval ((NormPolynomial p),x) = (eval (p,x)) / (p . ((len p) -' 1)) )
assume A1: len p <> 0 ; ::_thesis: for x being Element of L holds eval ((NormPolynomial p),x) = (eval (p,x)) / (p . ((len p) -' 1))
set NPp = NormPolynomial p;
let x be Element of L; ::_thesis: eval ((NormPolynomial p),x) = (eval (p,x)) / (p . ((len p) -' 1))
consider F1 being FinSequence of the carrier of L such that
A2: eval (p,x) = Sum F1 and
A3: len F1 = len p and
A4: for n being Element of NAT st n in dom F1 holds
F1 . n = (p . (n -' 1)) * ((power L) . (x,(n -' 1))) by POLYNOM4:def_2;
consider F2 being FinSequence of the carrier of L such that
A5: eval ((NormPolynomial p),x) = Sum F2 and
A6: len F2 = len (NormPolynomial p) and
A7: for n being Element of NAT st n in dom F2 holds
F2 . n = ((NormPolynomial p) . (n -' 1)) * ((power L) . (x,(n -' 1))) by POLYNOM4:def_2;
 len F1 = len F2 by A1, A3, A6, Th57;
then A8: dom F1 = dom F2 by FINSEQ_3:29;
now__::_thesis:_for_i_being_set_st_i_in_dom_F1_holds_
F2_/._i_=_(F1_/._i)_*_((p_._((len_p)_-'_1))_")
let i be set ; ::_thesis: ( i in dom F1 implies F2 /. i = (F1 /. i) * ((p . ((len p) -' 1)) ") )
assume A9: i in dom F1 ; ::_thesis: F2 /. i = (F1 /. i) * ((p . ((len p) -' 1)) ")
then reconsider i1 = i as Element of NAT ;
A10: (p . (i1 -' 1)) * ((power L) . (x,(i1 -' 1))) = F1 . i by A4, A9
.= F1 /. i by A9, PARTFUN1:def_6 ;
thus F2 /. i = F2 . i by A8, A9, PARTFUN1:def_6
.= ((NormPolynomial p) . (i1 -' 1)) * ((power L) . (x,(i1 -' 1))) by A7, A8, A9
.= ((p . (i1 -' 1)) / (p . ((len p) -' 1))) * ((power L) . (x,(i1 -' 1))) by Def10
.= ((p . (i1 -' 1)) * ((p . ((len p) -' 1)) ")) * ((power L) . (x,(i1 -' 1))) by VECTSP_1:def_11
.= (F1 /. i) * ((p . ((len p) -' 1)) ") by A10, GROUP_1:def_3 ; ::_thesis: verum
end;
then  F2 = F1 * ((p . ((len p) -' 1)) ") by A8, POLYNOM1:def_2;
then  eval ((NormPolynomial p),x) = (eval (p,x)) * ((p . ((len p) -' 1)) ") by A2, A5, POLYNOM1:13;
hence  eval ((NormPolynomial p),x) = (eval (p,x)) / (p . ((len p) -' 1)) by VECTSP_1:def_11; ::_thesis: verum
end;

theorem Th59: :: POLYNOM5:59
for L being Field
for p being Polynomial of L st len p <> 0 holds
for x being Element of L holds
( x is_a_root_of p iff x is_a_root_of NormPolynomial p )
proof
let L be Field; ::_thesis: for p being Polynomial of L st len p <> 0 holds
for x being Element of L holds
( x is_a_root_of p iff x is_a_root_of NormPolynomial p )
let p be Polynomial of L; ::_thesis: ( len p <> 0 implies for x being Element of L holds
( x is_a_root_of p iff x is_a_root_of NormPolynomial p ) )
assume A1: len p <> 0 ; ::_thesis: for x being Element of L holds
( x is_a_root_of p iff x is_a_root_of NormPolynomial p )
then  len p >= 0 + 1 by NAT_1:13;
then  len p = ((len p) -' 1) + 1 by XREAL_1:235;
then  p . ((len p) -' 1) <> 0. L by ALGSEQ_1:10;
then A2: (p . ((len p) -' 1)) " <> 0. L by VECTSP_1:25;
let x be Element of L; ::_thesis: ( x is_a_root_of p iff x is_a_root_of NormPolynomial p )
thus  ( x is_a_root_of p implies x is_a_root_of NormPolynomial p ) ::_thesis: ( x is_a_root_of NormPolynomial p implies x is_a_root_of p )
proof
assume  x is_a_root_of p ; ::_thesis: x is_a_root_of NormPolynomial p
then  eval (p,x) = 0. L by Def6;
then  eval ((NormPolynomial p),x) = (0. L) / (p . ((len p) -' 1)) by A1, Th58
.= (0. L) * ((p . ((len p) -' 1)) ") by VECTSP_1:def_11
.= 0. L by VECTSP_1:7 ;
hence  x is_a_root_of NormPolynomial p by Def6; ::_thesis: verum
end;
assume  x is_a_root_of NormPolynomial p ; ::_thesis: x is_a_root_of p
then  0. L = eval ((NormPolynomial p),x) by Def6
.= (eval (p,x)) / (p . ((len p) -' 1)) by A1, Th58
.= (eval (p,x)) * ((p . ((len p) -' 1)) ") by VECTSP_1:def_11 ;
then  eval (p,x) = 0. L by A2, VECTSP_1:12;
hence  x is_a_root_of p by Def6; ::_thesis: verum
end;

theorem Th60: :: POLYNOM5:60
for L being Field
for p being Polynomial of L st len p <> 0 holds
( p is with_roots iff NormPolynomial p is with_roots )
proof
let L be Field; ::_thesis: for p being Polynomial of L st len p <> 0 holds
( p is with_roots iff NormPolynomial p is with_roots )
let p be Polynomial of L; ::_thesis: ( len p <> 0 implies ( p is with_roots iff NormPolynomial p is with_roots ) )
assume A1: len p <> 0 ; ::_thesis: ( p is with_roots iff NormPolynomial p is with_roots )
thus  ( p is with_roots implies NormPolynomial p is with_roots ) ::_thesis: ( NormPolynomial p is with_roots implies p is with_roots )
proof
assume  p is with_roots ; ::_thesis: NormPolynomial p is with_roots
then consider x being Element of L such that
A2: x is_a_root_of p by Def7;
 x is_a_root_of NormPolynomial p by A1, A2, Th59;
hence  NormPolynomial p is with_roots by Def7; ::_thesis: verum
end;
assume  NormPolynomial p is with_roots ; ::_thesis: p is with_roots
then consider x being Element of L such that
A3: x is_a_root_of NormPolynomial p by Def7;
 x is_a_root_of p by A1, A3, Th59;
hence  p is with_roots by Def7; ::_thesis: verum
end;

theorem :: POLYNOM5:61
for L being Field
for p being Polynomial of L st len p <> 0 holds
Roots p = Roots (NormPolynomial p)
proof
let L be Field; ::_thesis: for p being Polynomial of L st len p <> 0 holds
Roots p = Roots (NormPolynomial p)
let p be Polynomial of L; ::_thesis: ( len p <> 0 implies Roots p = Roots (NormPolynomial p) )
assume A1: len p <> 0 ; ::_thesis: Roots p = Roots (NormPolynomial p)
thus  Roots p c= Roots (NormPolynomial p) :: according to XBOOLE_0:def_10 ::_thesis: Roots (NormPolynomial p) c= Roots p
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Roots p or x in Roots (NormPolynomial p) )
assume A2: x in Roots p ; ::_thesis: x in Roots (NormPolynomial p)
then reconsider x1 = x as Element of L ;
 x1 is_a_root_of p by A2, Def9;
then  x1 is_a_root_of NormPolynomial p by A1, Th59;
hence  x in Roots (NormPolynomial p) by Def9; ::_thesis: verum
end;
thus  Roots (NormPolynomial p) c= Roots p ::_thesis: verum
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Roots (NormPolynomial p) or x in Roots p )
assume A3: x in Roots (NormPolynomial p) ; ::_thesis: x in Roots p
then reconsider x1 = x as Element of L ;
 x1 is_a_root_of NormPolynomial p by A3, Def9;
then  x1 is_a_root_of p by A1, Th59;
hence  x in Roots p by Def9; ::_thesis: verum
end;
end;

theorem Th62: :: POLYNOM5:62
id COMPLEX is_continuous_on COMPLEX
proof
A1: now__::_thesis:_for_x_being_Element_of_COMPLEX_
for_r_being_Real_st_x_in_COMPLEX_&_0_<_r_holds_
ex_s_being_Real_st_
(_0_<_s_&_(_for_y_being_Element_of_COMPLEX_st_y_in_COMPLEX_&_|.(y_-_x).|_<_s_holds_
|.(((id_COMPLEX)_/._y)_-_((id_COMPLEX)_/._x)).|_<_r_)_)
let x be Element of COMPLEX ; ::_thesis: for r being Real st x in COMPLEX & 0 < r holds
ex s being Real st
( 0 < s & ( for y being Element of COMPLEX st y in COMPLEX & |.(y - x).| < s holds
|.(((id COMPLEX) /. y) - ((id COMPLEX) /. x)).| < r ) )
let r be Real; ::_thesis: ( x in COMPLEX & 0 < r implies ex s being Real st
( 0 < s & ( for y being Element of COMPLEX st y in COMPLEX & |.(y - x).| < s holds
|.(((id COMPLEX) /. y) - ((id COMPLEX) /. x)).| < r ) ) )
assume that
 x in COMPLEX and
A2: 0 < r ; ::_thesis: ex s being Real st
( 0 < s & ( for y being Element of COMPLEX st y in COMPLEX & |.(y - x).| < s holds
|.(((id COMPLEX) /. y) - ((id COMPLEX) /. x)).| < r ) )
take s = r; ::_thesis: ( 0 < s & ( for y being Element of COMPLEX st y in COMPLEX & |.(y - x).| < s holds
|.(((id COMPLEX) /. y) - ((id COMPLEX) /. x)).| < r ) )
thus  0 < s by A2; ::_thesis: for y being Element of COMPLEX st y in COMPLEX & |.(y - x).| < s holds
|.(((id COMPLEX) /. y) - ((id COMPLEX) /. x)).| < r
let y be Element of COMPLEX ; ::_thesis: ( y in COMPLEX & |.(y - x).| < s implies |.(((id COMPLEX) /. y) - ((id COMPLEX) /. x)).| < r )
assume that
 y in COMPLEX and
A3: |.(y - x).| < s ; ::_thesis: |.(((id COMPLEX) /. y) - ((id COMPLEX) /. x)).| < r
 (id COMPLEX) /. x = x by FUNCT_1:18;
hence  |.(((id COMPLEX) /. y) - ((id COMPLEX) /. x)).| < r by A3, FUNCT_1:18; ::_thesis: verum
end;
 dom (id COMPLEX) = COMPLEX by FUNCT_2:def_1;
hence  id COMPLEX is_continuous_on COMPLEX by A1, CFCONT_1:39; ::_thesis: verum
end;

theorem Th63: :: POLYNOM5:63
for x being Element of COMPLEX holds COMPLEX --> x is_continuous_on COMPLEX
proof
let x be Element of COMPLEX ; ::_thesis: COMPLEX --> x is_continuous_on COMPLEX
A1: now__::_thesis:_for_x1_being_Element_of_COMPLEX_
for_r_being_Real_st_x1_in_COMPLEX_&_0_<_r_holds_
ex_s_being_Real_st_
(_0_<_s_&_(_for_x2_being_Element_of_COMPLEX_st_x2_in_COMPLEX_&_|.(x2_-_x1).|_<_s_holds_
|.(((COMPLEX_-->_x)_/._x2)_-_((COMPLEX_-->_x)_/._x1)).|_<_r_)_)
let x1 be Element of COMPLEX ; ::_thesis: for r being Real st x1 in COMPLEX & 0 < r holds
ex s being Real st
( 0 < s & ( for x2 being Element of COMPLEX st x2 in COMPLEX & |.(x2 - x1).| < s holds
|.(((COMPLEX --> x) /. x2) - ((COMPLEX --> x) /. x1)).| < r ) )
let r be Real; ::_thesis: ( x1 in COMPLEX & 0 < r implies ex s being Real st
( 0 < s & ( for x2 being Element of COMPLEX st x2 in COMPLEX & |.(x2 - x1).| < s holds
|.(((COMPLEX --> x) /. x2) - ((COMPLEX --> x) /. x1)).| < r ) ) )
assume that
 x1 in COMPLEX and
A2: 0 < r ; ::_thesis: ex s being Real st
( 0 < s & ( for x2 being Element of COMPLEX st x2 in COMPLEX & |.(x2 - x1).| < s holds
|.(((COMPLEX --> x) /. x2) - ((COMPLEX --> x) /. x1)).| < r ) )
take s = r; ::_thesis: ( 0 < s & ( for x2 being Element of COMPLEX st x2 in COMPLEX & |.(x2 - x1).| < s holds
|.(((COMPLEX --> x) /. x2) - ((COMPLEX --> x) /. x1)).| < r ) )
thus  0 < s by A2; ::_thesis: for x2 being Element of COMPLEX st x2 in COMPLEX & |.(x2 - x1).| < s holds
|.(((COMPLEX --> x) /. x2) - ((COMPLEX --> x) /. x1)).| < r
let x2 be Element of COMPLEX ; ::_thesis: ( x2 in COMPLEX & |.(x2 - x1).| < s implies |.(((COMPLEX --> x) /. x2) - ((COMPLEX --> x) /. x1)).| < r )
assume that
 x2 in COMPLEX and
 |.(x2 - x1).| < s ; ::_thesis: |.(((COMPLEX --> x) /. x2) - ((COMPLEX --> x) /. x1)).| < r
 ( (COMPLEX --> x) /. x1 = x & (COMPLEX --> x) /. x2 = x ) by FUNCOP_1:7;
hence  |.(((COMPLEX --> x) /. x2) - ((COMPLEX --> x) /. x1)).| < r by A2, COMPLEX1:44; ::_thesis: verum
end;
 dom (COMPLEX --> x) = COMPLEX by FUNCOP_1:13;
hence  COMPLEX --> x is_continuous_on COMPLEX by A1, CFCONT_1:39; ::_thesis: verum
end;

definition
let L be non empty unital multMagma ;
let x be Element of L;
let n be Element of NAT ;
func FPower (x,n) ->  Function of L,L means :Def11: :: POLYNOM5:def 11
 for y being Element of L holds it . y = x * ((power L) . (y,n));
existence
 ex b1 being Function of L,L st
for y being Element of L holds b1 . y = x * ((power L) . (y,n))
proof
deffunc H1( Element of L) ->  Element of the carrier of L = x * ((power L) . ($1,n));
consider f being Function of the carrier of L, the carrier of L such that
A1: for y being Element of L holds f . y = H1(y) from FUNCT_2:sch_4();
reconsider f = f as Function of L,L ;
take  f ; ::_thesis: for y being Element of L holds f . y = x * ((power L) . (y,n))
thus  for y being Element of L holds f . y = x * ((power L) . (y,n)) by A1; ::_thesis: verum
end;
uniqueness
 for b1, b2 being Function of L,L st ( for y being Element of L holds b1 . y = x * ((power L) . (y,n)) ) & ( for y being Element of L holds b2 . y = x * ((power L) . (y,n)) ) holds
b1 = b2
proof
let f1, f2 be Function of L,L; ::_thesis: ( ( for y being Element of L holds f1 . y = x * ((power L) . (y,n)) ) & ( for y being Element of L holds f2 . y = x * ((power L) . (y,n)) ) implies f1 = f2 )
assume that
A2: for y being Element of L holds f1 . y = x * ((power L) . (y,n)) and
A3: for y being Element of L holds f2 . y = x * ((power L) . (y,n)) ; ::_thesis: f1 = f2
now__::_thesis:_for_y_being_Element_of_L_holds_f1_._y_=_f2_._y
let y be Element of L; ::_thesis: f1 . y = f2 . y
thus f1 . y = x * ((power L) . (y,n)) by A2
.= f2 . y by A3 ; ::_thesis: verum
end;
hence  f1 = f2 by FUNCT_2:63; ::_thesis: verum
end;
end;

:: deftheorem Def11 defines FPower POLYNOM5:def_11_:_
 for L being non empty unital multMagma
for x being Element of L
for n being Element of NAT
for b4 being Function of L,L holds
( b4 = FPower (x,n) iff for y being Element of L holds b4 . y = x * ((power L) . (y,n)) );

theorem :: POLYNOM5:64
for L being non empty unital multMagma holds FPower ((1_ L),1) = id the carrier of L
proof
let L be non empty unital multMagma ; ::_thesis: FPower ((1_ L),1) = id the carrier of L
A1: now__::_thesis:_for_x_being_set_st_x_in_the_carrier_of_L_holds_
(FPower_((1__L),1))_._x_=_x
let x be set ; ::_thesis: ( x in the carrier of L implies (FPower ((1_ L),1)) . x = x )
assume  x in the carrier of L ; ::_thesis: (FPower ((1_ L),1)) . x = x
then reconsider x1 = x as Element of L ;
(FPower ((1_ L),1)) . x1 = (1_ L) * ((power L) . (x1,1)) by Def11
.= (power L) . (x1,1) by GROUP_1:def_4 ;
hence  (FPower ((1_ L),1)) . x = x by GROUP_1:50; ::_thesis: verum
end;
 dom (FPower ((1_ L),1)) = the carrier of L by FUNCT_2:def_1;
hence  FPower ((1_ L),1) = id the carrier of L by A1, FUNCT_1:17; ::_thesis: verum
end;

theorem :: POLYNOM5:65
FPower ((1_ F_Complex),2) = (id COMPLEX) (#) (id COMPLEX)
proof
 the carrier of F_Complex = COMPLEX by COMPLFLD:def_1;
then reconsider f = (id COMPLEX) (#) (id COMPLEX) as Function of F_Complex,F_Complex ;
now__::_thesis:_for_x_being_Element_of_F_Complex_holds_f_._x_=_(1__F_Complex)_*_((power_F_Complex)_._(x,2))
let x be Element of F_Complex; ::_thesis: f . x = (1_ F_Complex) * ((power F_Complex) . (x,2))
reconsider x1 = x as Element of COMPLEX by COMPLFLD:def_1;
 ( (id COMPLEX) /. x1 = x1 & dom ((id COMPLEX) (#) (id COMPLEX)) = COMPLEX ) by FUNCT_1:18, FUNCT_2:def_1;
hence f . x = x * x by VALUED_1:def_4
.= (power F_Complex) . (x,2) by GROUP_1:51
.= (1_ F_Complex) * ((power F_Complex) . (x,2)) by VECTSP_1:def_8 ;
::_thesis: verum
end;
hence  FPower ((1_ F_Complex),2) = (id COMPLEX) (#) (id COMPLEX) by Def11; ::_thesis: verum
end;

theorem Th66: :: POLYNOM5:66
for L being non empty unital multMagma
for x being Element of L holds FPower (x,0) = the carrier of L --> x
proof
let L be non empty unital multMagma ; ::_thesis: for x being Element of L holds FPower (x,0) = the carrier of L --> x
let x be Element of L; ::_thesis: FPower (x,0) = the carrier of L --> x
reconsider f = the carrier of L --> x as Function of L,L ;
now__::_thesis:_for_y_being_Element_of_L_holds_f_._y_=_x_*_((power_L)_._(y,0))
let y be Element of L; ::_thesis: f . y = x * ((power L) . (y,0))
thus f . y = x by FUNCOP_1:7
.= x * (1_ L) by GROUP_1:def_4
.= x * ((power L) . (y,0)) by GROUP_1:def_7 ; ::_thesis: verum
end;
hence  FPower (x,0) = the carrier of L --> x by Def11; ::_thesis: verum
end;

theorem :: POLYNOM5:67
for x being Element of F_Complex ex x1 being Element of COMPLEX st
( x = x1 & FPower (x,1) = x1 (#) (id COMPLEX) )
proof
let x be Element of F_Complex; ::_thesis: ex x1 being Element of COMPLEX st
( x = x1 & FPower (x,1) = x1 (#) (id COMPLEX) )
reconsider x1 = x as Element of COMPLEX by COMPLFLD:def_1;
take  x1 ; ::_thesis: ( x = x1 & FPower (x,1) = x1 (#) (id COMPLEX) )
thus  x = x1 ; ::_thesis: FPower (x,1) = x1 (#) (id COMPLEX)
 the carrier of F_Complex = COMPLEX by COMPLFLD:def_1;
then reconsider f = x1 (#) (id COMPLEX) as Function of F_Complex,F_Complex ;
now__::_thesis:_for_y_being_Element_of_F_Complex_holds_f_._y_=_x_*_((power_F_Complex)_._(y,1))
let y be Element of F_Complex; ::_thesis: f . y = x * ((power F_Complex) . (y,1))
reconsider y1 = y as Element of COMPLEX by COMPLFLD:def_1;
thus f . y = x1 * ((id COMPLEX) . y1) by VALUED_1:6
.= x * y by FUNCT_1:18
.= x * ((power F_Complex) . (y,1)) by GROUP_1:50 ; ::_thesis: verum
end;
hence  FPower (x,1) = x1 (#) (id COMPLEX) by Def11; ::_thesis: verum
end;

theorem :: POLYNOM5:68
for x being Element of F_Complex ex x1 being Element of COMPLEX st
( x = x1 & FPower (x,2) = x1 (#) ((id COMPLEX) (#) (id COMPLEX)) )
proof
let x be Element of F_Complex; ::_thesis: ex x1 being Element of COMPLEX st
( x = x1 & FPower (x,2) = x1 (#) ((id COMPLEX) (#) (id COMPLEX)) )
reconsider x1 = x as Element of COMPLEX by COMPLFLD:def_1;
take  x1 ; ::_thesis: ( x = x1 & FPower (x,2) = x1 (#) ((id COMPLEX) (#) (id COMPLEX)) )
thus  x = x1 ; ::_thesis: FPower (x,2) = x1 (#) ((id COMPLEX) (#) (id COMPLEX))
 the carrier of F_Complex = COMPLEX by COMPLFLD:def_1;
then reconsider f = x1 (#) ((id COMPLEX) (#) (id COMPLEX)) as Function of F_Complex,F_Complex ;
now__::_thesis:_for_y_being_Element_of_F_Complex_holds_f_._y_=_x_*_((power_F_Complex)_._(y,2))
let y be Element of F_Complex; ::_thesis: f . y = x * ((power F_Complex) . (y,2))
reconsider y1 = y as Element of COMPLEX by COMPLFLD:def_1;
thus f . y = x1 * (((id COMPLEX) (#) (id COMPLEX)) . y1) by VALUED_1:6
.= x1 * (((id COMPLEX) . y1) * ((id COMPLEX) . y1)) by VALUED_1:5
.= x1 * (y1 * ((id COMPLEX) . y1)) by FUNCT_1:18
.= x * (y * y) by FUNCT_1:18
.= x * ((power F_Complex) . (y,2)) by GROUP_1:51 ; ::_thesis: verum
end;
hence  FPower (x,2) = x1 (#) ((id COMPLEX) (#) (id COMPLEX)) by Def11; ::_thesis: verum
end;

theorem Th69: :: POLYNOM5:69
for x being Element of F_Complex
for n being Element of NAT ex f being Function of COMPLEX,COMPLEX st
( f = FPower (x,n) & FPower (x,(n + 1)) = f (#) (id COMPLEX) )
proof
let x be Element of F_Complex; ::_thesis: for n being Element of NAT ex f being Function of COMPLEX,COMPLEX st
( f = FPower (x,n) & FPower (x,(n + 1)) = f (#) (id COMPLEX) )
let n be Element of NAT ; ::_thesis: ex f being Function of COMPLEX,COMPLEX st
( f = FPower (x,n) & FPower (x,(n + 1)) = f (#) (id COMPLEX) )
A1: the carrier of F_Complex = COMPLEX by COMPLFLD:def_1;
then reconsider f = FPower (x,n) as Function of COMPLEX,COMPLEX ;
reconsider g = f (#) (id COMPLEX) as Function of F_Complex,F_Complex by A1;
take  f ; ::_thesis: ( f = FPower (x,n) & FPower (x,(n + 1)) = f (#) (id COMPLEX) )
thus  f = FPower (x,n) ; ::_thesis: FPower (x,(n + 1)) = f (#) (id COMPLEX)
now__::_thesis:_for_y_being_Element_of_F_Complex_holds_g_._y_=_x_*_((power_F_Complex)_._(y,(n_+_1)))
let y be Element of F_Complex; ::_thesis: g . y = x * ((power F_Complex) . (y,(n + 1)))
reconsider y1 = y as Element of COMPLEX by COMPLFLD:def_1;
thus g . y = (f . y1) * ((id COMPLEX) . y1) by VALUED_1:5
.= ((FPower (x,n)) . y) * y by FUNCT_1:18
.= (x * ((power F_Complex) . (y,n))) * y by Def11
.= x * (((power F_Complex) . (y,n)) * y)
.= x * ((power F_Complex) . (y,(n + 1))) by GROUP_1:def_7 ; ::_thesis: verum
end;
hence  FPower (x,(n + 1)) = f (#) (id COMPLEX) by Def11; ::_thesis: verum
end;

theorem Th70: :: POLYNOM5:70
for x being Element of F_Complex
for n being Element of NAT ex f being Function of COMPLEX,COMPLEX st
( f = FPower (x,n) & f is_continuous_on COMPLEX )
proof
let x be Element of F_Complex; ::_thesis: for n being Element of NAT ex f being Function of COMPLEX,COMPLEX st
( f = FPower (x,n) & f is_continuous_on COMPLEX )
defpred S1[ Element of NAT ] means  ex f being Function of COMPLEX,COMPLEX st
( f = FPower (x,$1) & f is_continuous_on COMPLEX );
A1: the carrier of F_Complex = COMPLEX by COMPLFLD:def_1;
A2: for n being Element of NAT st S1[n] holds
S1[n + 1]
proof
let n be Element of NAT ; ::_thesis: ( S1[n] implies S1[n + 1] )
reconsider g = FPower (x,(n + 1)) as Function of COMPLEX,COMPLEX by A1;
given f being Function of COMPLEX,COMPLEX such that A3: ( f = FPower (x,n) & f is_continuous_on COMPLEX ) ; ::_thesis: S1[n + 1]
take  g ; ::_thesis: ( g = FPower (x,(n + 1)) & g is_continuous_on COMPLEX )
thus  g = FPower (x,(n + 1)) ; ::_thesis: g is_continuous_on COMPLEX
 ex f1 being Function of COMPLEX,COMPLEX st
( f1 = FPower (x,n) & FPower (x,(n + 1)) = f1 (#) (id COMPLEX) ) by Th69;
hence  g is_continuous_on COMPLEX by A3, Th62, CFCONT_1:43; ::_thesis: verum
end;
A4: S1[ 0 ]
proof
reconsider f = FPower (x,0) as Function of COMPLEX,COMPLEX by A1;
take  f ; ::_thesis: ( f = FPower (x,0) & f is_continuous_on COMPLEX )
thus  f = FPower (x,0) ; ::_thesis: f is_continuous_on COMPLEX
 f = the carrier of F_Complex --> x by Th66;
hence  f is_continuous_on COMPLEX by A1, Th63; ::_thesis: verum
end;
thus  for n being Element of NAT holds S1[n] from NAT_1:sch_1(A4, A2); ::_thesis: verum
end;

definition
let L be non empty well-unital doubleLoopStr ;
let p be Polynomial of L;
func Polynomial-Function (L,p) ->  Function of L,L means :Def12: :: POLYNOM5:def 12
 for x being Element of L holds it . x = eval (p,x);
existence
 ex b1 being Function of L,L st
for x being Element of L holds b1 . x = eval (p,x)
proof
deffunc H1( Element of L) ->  Element of the carrier of L = eval (p,$1);
consider f being Function of the carrier of L, the carrier of L such that
A1: for x being Element of L holds f . x = H1(x) from FUNCT_2:sch_4();
reconsider f = f as Function of L,L ;
take  f ; ::_thesis: for x being Element of L holds f . x = eval (p,x)
thus  for x being Element of L holds f . x = eval (p,x) by A1; ::_thesis: verum
end;
uniqueness
 for b1, b2 being Function of L,L st ( for x being Element of L holds b1 . x = eval (p,x) ) & ( for x being Element of L holds b2 . x = eval (p,x) ) holds
b1 = b2
proof
let f1, f2 be Function of L,L; ::_thesis: ( ( for x being Element of L holds f1 . x = eval (p,x) ) & ( for x being Element of L holds f2 . x = eval (p,x) ) implies f1 = f2 )
assume that
A2: for x being Element of L holds f1 . x = eval (p,x) and
A3: for x being Element of L holds f2 . x = eval (p,x) ; ::_thesis: f1 = f2
now__::_thesis:_for_x_being_Element_of_L_holds_f1_._x_=_f2_._x
let x be Element of L; ::_thesis: f1 . x = f2 . x
thus f1 . x = eval (p,x) by A2
.= f2 . x by A3 ; ::_thesis: verum
end;
hence  f1 = f2 by FUNCT_2:63; ::_thesis: verum
end;
end;

:: deftheorem Def12 defines Polynomial-Function POLYNOM5:def_12_:_
 for L being non empty well-unital doubleLoopStr
for p being Polynomial of L
for b3 being Function of L,L holds
( b3 = Polynomial-Function (L,p) iff for x being Element of L holds b3 . x = eval (p,x) );

theorem Th71: :: POLYNOM5:71
for p being Polynomial of F_Complex ex f being Function of COMPLEX,COMPLEX st
( f = Polynomial-Function (F_Complex,p) & f is_continuous_on COMPLEX )
proof
set FuFF = Funcs (COMPLEX,COMPLEX);
let p be Polynomial of F_Complex; ::_thesis: ex f being Function of COMPLEX,COMPLEX st
( f = Polynomial-Function (F_Complex,p) & f is_continuous_on COMPLEX )
reconsider fzero = COMPLEX --> 0c as Element of Funcs (COMPLEX,COMPLEX) by FUNCT_2:9;
defpred S1[ Nat, set ] means $2 = FPower ((p . ($1 -' 1)),($1 -' 1));
A1: the carrier of F_Complex = COMPLEX by COMPLFLD:def_1;
then reconsider f = Polynomial-Function (F_Complex,p) as Function of COMPLEX,COMPLEX ;
deffunc H1( Element of Funcs (COMPLEX,COMPLEX), Element of Funcs (COMPLEX,COMPLEX)) ->  Element of K27(K28(COMPLEX,COMPLEX)) = $1 + $2;
take  f ; ::_thesis: ( f = Polynomial-Function (F_Complex,p) & f is_continuous_on COMPLEX )
thus  f = Polynomial-Function (F_Complex,p) ; ::_thesis: f is_continuous_on COMPLEX
A2: for x, y being Element of Funcs (COMPLEX,COMPLEX) holds H1(x,y) in Funcs (COMPLEX,COMPLEX) by FUNCT_2:8;
consider fadd being BinOp of (Funcs (COMPLEX,COMPLEX)) such that
A3: for x, y being Element of Funcs (COMPLEX,COMPLEX) holds fadd . (x,y) = H1(x,y) from FUNCT_7:sch_1(A2);
reconsider L = addLoopStr(# (Funcs (COMPLEX,COMPLEX)),fadd,fzero #) as non empty addLoopStr ;
A4: now__::_thesis:_for_u,_v,_w_being_Element_of_L_holds_(u_+_v)_+_w_=_u_+_(v_+_w)
let u, v, w be Element of L; ::_thesis: (u + v) + w = u + (v + w)
reconsider u1 = u, v1 = v, w1 = w as Function of COMPLEX,COMPLEX by FUNCT_2:66;
A5: u1 + v1 in Funcs (COMPLEX,COMPLEX) by FUNCT_2:9;
A6: v1 + w1 in Funcs (COMPLEX,COMPLEX) by FUNCT_2:9;
thus (u + v) + w = fadd . ((u1 + v1),w) by A3
.= (u1 + v1) + w1 by A3, A5
.= u1 + (v1 + w1) by CFUNCT_1:13
.= fadd . (u,(v1 + w1)) by A3, A6
.= u + (v + w) by A3 ; ::_thesis: verum
end;
A7: now__::_thesis:_for_v_being_Element_of_L_holds_v_+_(0._L)_=_v
let v be Element of L; ::_thesis: v + (0. L) = v
reconsider v1 = v as Function of COMPLEX,COMPLEX by FUNCT_2:66;
A8: now__::_thesis:_for_x_being_Element_of_COMPLEX_holds_(v1_+_fzero)_._x_=_v1_._x
let x be Element of COMPLEX ; ::_thesis: (v1 + fzero) . x = v1 . x
thus (v1 + fzero) . x = (v1 . x) + (fzero . x) by VALUED_1:1
.= (v1 . x) + 0c by FUNCOP_1:7
.= v1 . x ; ::_thesis: verum
end;
thus v + (0. L) = v1 + fzero by A3
.= v by A8, FUNCT_2:63 ; ::_thesis: verum
end;
 L is right_complementable
proof
let v be Element of L; :: according to ALGSTR_0:def_16 ::_thesis: v is right_complementable
reconsider v1 = v as Function of COMPLEX,COMPLEX by FUNCT_2:66;
reconsider w = - v1 as Element of L by FUNCT_2:9;
take  w ; :: according to ALGSTR_0:def_11 ::_thesis: v + w = 0. L
A9: now__::_thesis:_for_x_being_Element_of_COMPLEX_holds_(v1_+_(-_v1))_._x_=_fzero_._x
let x be Element of COMPLEX ; ::_thesis: (v1 + (- v1)) . x = fzero . x
thus (v1 + (- v1)) . x = (v1 . x) + ((- v1) . x) by VALUED_1:1
.= (v1 . x) + (- (v1 . x)) by VALUED_1:8
.= fzero . x by FUNCOP_1:7 ; ::_thesis: verum
end;
thus v + w = v1 + (- v1) by A3
.= 0. L by A9, FUNCT_2:63 ; ::_thesis: verum
end;
then reconsider L = L as non empty right_complementable add-associative right_zeroed addLoopStr by A4, A7, RLVECT_1:def_3, RLVECT_1:def_4;
A10: now__::_thesis:_for_n_being_Nat_st_n_in_Seg_(len_p)_holds_
ex_x_being_Element_of_L_st_S1[n,x]
let n be Nat; ::_thesis: ( n in Seg (len p) implies ex x being Element of L st S1[n,x] )
reconsider x = FPower ((p . (n -' 1)),(n -' 1)) as Element of L by A1, FUNCT_2:9;
assume  n in Seg (len p) ; ::_thesis: ex x being Element of L st S1[n,x]
take x = x; ::_thesis: S1[n,x]
thus  S1[n,x] ; ::_thesis: verum
end;
consider F being FinSequence of the carrier of L such that
A11: dom F = Seg (len p) and
A12: for n being Nat st n in Seg (len p) holds
S1[n,F . n] from FINSEQ_1:sch_5(A10);
A13: F | (len F) = F by FINSEQ_1:58;
reconsider SF = Sum F as Function of COMPLEX,COMPLEX by FUNCT_2:66;
A14: now__::_thesis:_for_x_being_Element_of_COMPLEX_holds_f_._x_=_SF_._x
let x be Element of COMPLEX ; ::_thesis: f . x = SF . x
reconsider x1 = x as Element of F_Complex by COMPLFLD:def_1;
consider H being FinSequence of the carrier of F_Complex such that
A15: eval (p,x1) = Sum H and
A16: len H = len p and
A17: for n being Element of NAT st n in dom H holds
H . n = (p . (n -' 1)) * ((power F_Complex) . (x1,(n -' 1))) by POLYNOM4:def_2;
defpred S2[ Element of NAT ] means  for SFk being Function of COMPLEX,COMPLEX st SFk = Sum (F | $1) holds
Sum (H | $1) = SFk . x;
A18: len F = len p by A11, FINSEQ_1:def_3;
A19: for k being Element of NAT st S2[k] holds
S2[k + 1]
proof
let k be Element of NAT ; ::_thesis: ( S2[k] implies S2[k + 1] )
assume A20: for SFk being Function of COMPLEX,COMPLEX st SFk = Sum (F | k) holds
Sum (H | k) = SFk . x ; ::_thesis: S2[k + 1]
reconsider SFk1 = Sum (F | k) as Function of COMPLEX,COMPLEX by FUNCT_2:66;
let SFk be Function of COMPLEX,COMPLEX; ::_thesis: ( SFk = Sum (F | (k + 1)) implies Sum (H | (k + 1)) = SFk . x )
assume A21: SFk = Sum (F | (k + 1)) ; ::_thesis: Sum (H | (k + 1)) = SFk . x
percases ( len F > k or len F <= k ) ;
supposeA22: len F > k ; ::_thesis: Sum (H | (k + 1)) = SFk . x
reconsider g2 = FPower ((p . k),k) as Function of COMPLEX,COMPLEX by A1;
A23: k + 1 >= 1 by NAT_1:11;
 k + 1 <= len F by A22, NAT_1:13;
then A24: k + 1 in dom F by A23, FINSEQ_3:25;
then A25: F /. (k + 1) = F . (k + 1) by PARTFUN1:def_6
.= FPower ((p . ((k + 1) -' 1)),((k + 1) -' 1)) by A11, A12, A24
.= FPower ((p . k),((k + 1) -' 1)) by NAT_D:34
.= FPower ((p . k),k) by NAT_D:34 ;
F | (k + 1) = (F | k) ^ <*(F . (k + 1))*> by A22, POLYNOM3:19
.= (F | k) ^ <*(F /. (k + 1))*> by A24, PARTFUN1:def_6 ;
then A26: SFk = (Sum (F | k)) + (F /. (k + 1)) by A21, FVSUM_1:71
.= SFk1 + g2 by A3, A25 ;
A27: Sum (H | k) = SFk1 . x by A20;
A28: dom F = dom H by A11, A16, FINSEQ_1:def_3;
then A29: H /. (k + 1) = H . (k + 1) by A24, PARTFUN1:def_6
.= (p . ((k + 1) -' 1)) * ((power F_Complex) . (x1,((k + 1) -' 1))) by A17, A28, A24
.= (p . k) * ((power F_Complex) . (x1,((k + 1) -' 1))) by NAT_D:34
.= (p . k) * ((power F_Complex) . (x1,k)) by NAT_D:34
.= (FPower ((p . k),k)) . x by Def11 ;
H | (k + 1) = (H | k) ^ <*(H . (k + 1))*> by A16, A18, A22, POLYNOM3:19
.= (H | k) ^ <*(H /. (k + 1))*> by A28, A24, PARTFUN1:def_6 ;
hence  Sum (H | (k + 1)) = (Sum (H | k)) + (H /. (k + 1)) by FVSUM_1:71
.= SFk . x by A29, A26, A27, VALUED_1:1 ;
::_thesis: verum
end;
supposeA30: len F <= k ; ::_thesis: Sum (H | (k + 1)) = SFk . x
 k <= k + 1 by NAT_1:11;
then A31: ( F | (k + 1) = F & H | (k + 1) = H ) by A16, A18, A30, FINSEQ_1:58, XXREAL_0:2;
 ( F | k = F & H | k = H ) by A16, A18, A30, FINSEQ_1:58;
hence  Sum (H | (k + 1)) = SFk . x by A20, A21, A31; ::_thesis: verum
end;
end;
end;
A32: S2[ 0 ]
proof
let SFk be Function of COMPLEX,COMPLEX; ::_thesis: ( SFk = Sum (F | 0) implies Sum (H | 0) = SFk . x )
A33: F | 0 = <*> the carrier of L ;
assume  SFk = Sum (F | 0) ; ::_thesis: Sum (H | 0) = SFk . x
then A34: SFk = 0. L by A33, RLVECT_1:43
.= COMPLEX --> 0c ;
 H | 0 = <*> the carrier of F_Complex ;
hence  Sum (H | 0) = 0. F_Complex by RLVECT_1:43
.= SFk . x by A34, COMPLFLD:7, FUNCOP_1:7 ;
::_thesis: verum
end;
A35: for k being Element of NAT holds S2[k] from NAT_1:sch_1(A32, A19);
A36: Sum (F | (len F)) = SF by FINSEQ_1:58;
thus f . x = Sum H by A15, Def12
.= Sum (H | (len H)) by FINSEQ_1:58
.= SF . x by A16, A18, A35, A36 ; ::_thesis: verum
end;
defpred S2[ Element of NAT ] means  for g being PartFunc of COMPLEX,COMPLEX st g = Sum (F | $1) holds
g is_continuous_on COMPLEX ;
A37: for k being Element of NAT st S2[k] holds
S2[k + 1]
proof
let k be Element of NAT ; ::_thesis: ( S2[k] implies S2[k + 1] )
reconsider g1 = Sum (F | k) as Function of COMPLEX,COMPLEX by FUNCT_2:66;
assume A38: for g being PartFunc of COMPLEX,COMPLEX st g = Sum (F | k) holds
g is_continuous_on COMPLEX ; ::_thesis: S2[k + 1]
then A39: g1 is_continuous_on COMPLEX ;
let g be PartFunc of COMPLEX,COMPLEX; ::_thesis: ( g = Sum (F | (k + 1)) implies g is_continuous_on COMPLEX )
assume A40: g = Sum (F | (k + 1)) ; ::_thesis: g is_continuous_on COMPLEX
percases ( len F > k or len F <= k ) ;
supposeA41: len F > k ; ::_thesis: g is_continuous_on COMPLEX
A42: k + 1 >= 1 by NAT_1:11;
 k + 1 <= len F by A41, NAT_1:13;
then A43: k + 1 in dom F by A42, FINSEQ_3:25;
then A44: F /. (k + 1) = F . (k + 1) by PARTFUN1:def_6
.= FPower ((p . ((k + 1) -' 1)),((k + 1) -' 1)) by A11, A12, A43
.= FPower ((p . k),((k + 1) -' 1)) by NAT_D:34
.= FPower ((p . k),k) by NAT_D:34 ;
consider g2 being Function of COMPLEX,COMPLEX such that
A45: g2 = FPower ((p . k),k) and
A46: g2 is_continuous_on COMPLEX by Th70;
F | (k + 1) = (F | k) ^ <*(F . (k + 1))*> by A41, POLYNOM3:19
.= (F | k) ^ <*(F /. (k + 1))*> by A43, PARTFUN1:def_6 ;
then g = (Sum (F | k)) + (F /. (k + 1)) by A40, FVSUM_1:71
.= g1 + g2 by A3, A44, A45 ;
hence  g is_continuous_on COMPLEX by A39, A46, CFCONT_1:43; ::_thesis: verum
end;
supposeA47: len F <= k ; ::_thesis: g is_continuous_on COMPLEX
 k <= k + 1 by NAT_1:11;
then F | (k + 1) = F by A47, FINSEQ_1:58, XXREAL_0:2
.= F | k by A47, FINSEQ_1:58 ;
hence  g is_continuous_on COMPLEX by A38, A40; ::_thesis: verum
end;
end;
end;
A48: S2[ 0 ]
proof
let g be PartFunc of COMPLEX,COMPLEX; ::_thesis: ( g = Sum (F | 0) implies g is_continuous_on COMPLEX )
A49: F | 0 = <*> the carrier of L ;
assume  g = Sum (F | 0) ; ::_thesis: g is_continuous_on COMPLEX
then g = 0. L by A49, RLVECT_1:43
.= COMPLEX --> 0c ;
hence  g is_continuous_on COMPLEX by Th63; ::_thesis: verum
end;
 for k being Element of NAT holds S2[k] from NAT_1:sch_1(A48, A37);
hence  f is_continuous_on COMPLEX by A13, A14, FUNCT_2:63; ::_thesis: verum
end;

theorem Th72: :: POLYNOM5:72
for p being Polynomial of F_Complex st len p > 2 & |.(p . ((len p) -' 1)).| = 1 holds
for F being FinSequence of REAL st len F = len p & ( for n being Element of NAT st n in dom F holds
F . n = |.(p . (n -' 1)).| ) holds
for z being Element of F_Complex st |.z.| > Sum F holds
|.(eval (p,z)).| > |.(p . 0).| + 1
proof
let p be Polynomial of F_Complex; ::_thesis: ( len p > 2 & |.(p . ((len p) -' 1)).| = 1 implies for F being FinSequence of REAL st len F = len p & ( for n being Element of NAT st n in dom F holds
F . n = |.(p . (n -' 1)).| ) holds
for z being Element of F_Complex st |.z.| > Sum F holds
|.(eval (p,z)).| > |.(p . 0).| + 1 )
assume that
A1: len p > 2 and
A2: |.(p . ((len p) -' 1)).| = 1 ; ::_thesis: for F being FinSequence of REAL st len F = len p & ( for n being Element of NAT st n in dom F holds
F . n = |.(p . (n -' 1)).| ) holds
for z being Element of F_Complex st |.z.| > Sum F holds
|.(eval (p,z)).| > |.(p . 0).| + 1
let F be FinSequence of REAL ; ::_thesis: ( len F = len p & ( for n being Element of NAT st n in dom F holds
F . n = |.(p . (n -' 1)).| ) implies for z being Element of F_Complex st |.z.| > Sum F holds
|.(eval (p,z)).| > |.(p . 0).| + 1 )
assume that
A3: len F = len p and
A4: for n being Element of NAT st n in dom F holds
F . n = |.(p . (n -' 1)).| ; ::_thesis: for z being Element of F_Complex st |.z.| > Sum F holds
|.(eval (p,z)).| > |.(p . 0).| + 1
set lF1 = (len F) -' 1;
A5: ((len F) -' 1) + 1 = len F by A1, A3, XREAL_1:235, XXREAL_0:2;
then A6: F = F | (((len F) -' 1) + 1) by FINSEQ_1:58
.= (F | ((len F) -' 1)) ^ <*(F /. (((len F) -' 1) + 1))*> by A5, FINSEQ_5:82 ;
A7: len p > 1 by A1, XXREAL_0:2;
then A8: 1 in dom F by A3, FINSEQ_3:25;
A9: now__::_thesis:_for_n_being_Element_of_NAT_st_n_in_dom_(F_|_((len_F)_-'_1))_holds_
(F_|_((len_F)_-'_1))_._n_>=_0
let n be Element of NAT ; ::_thesis: ( n in dom (F | ((len F) -' 1)) implies (F | ((len F) -' 1)) . n >= 0 )
A10: dom (F | ((len F) -' 1)) c= dom F by FINSEQ_5:18;
assume A11: n in dom (F | ((len F) -' 1)) ; ::_thesis: (F | ((len F) -' 1)) . n >= 0
then (F | ((len F) -' 1)) . n = (F | ((len F) -' 1)) /. n by PARTFUN1:def_6
.= F /. n by A11, FINSEQ_4:70
.= F . n by A11, A10, PARTFUN1:def_6
.= |.(p . (n -' 1)).| by A4, A11, A10 ;
hence  (F | ((len F) -' 1)) . n >= 0 by COMPLEX1:46; ::_thesis: verum
end;
A12: len (F | ((len F) -' 1)) = (len F) -' 1 by A5, FINSEQ_1:59, NAT_1:11;
 |.(p . 0).| >= 0 by COMPLEX1:46;
then A13: |.(p . 0).| + 1 >= 0 + 1 by XREAL_1:6;
let z be Element of F_Complex; ::_thesis: ( |.z.| > Sum F implies |.(eval (p,z)).| > |.(p . 0).| + 1 )
consider G being FinSequence of the carrier of F_Complex such that
A14: eval (p,z) = Sum G and
A15: len G = len p and
A16: for n being Element of NAT st n in dom G holds
G . n = (p . (n -' 1)) * ((power F_Complex) . (z,(n -' 1))) by POLYNOM4:def_2;
set lF2 = (len F) -' 2;
assume A17: |.z.| > Sum F ; ::_thesis: |.(eval (p,z)).| > |.(p . 0).| + 1
A18: len F in dom F by A7, A3, FINSEQ_3:25;
then F /. (((len F) -' 1) + 1) = F . (((len F) -' 1) + 1) by A5, PARTFUN1:def_6
.= 1 by A2, A3, A4, A5, A18 ;
then A19: Sum F = (Sum (F | ((len F) -' 1))) + 1 by A6, RVSUM_1:74;
A20: len F >= (1 + 1) + 0 by A1, A3;
then  (len F) -' 1 >= 1 by A5, XREAL_1:6;
then A21: 1 in dom (F | ((len F) -' 1)) by A12, FINSEQ_3:25;
then (F | ((len F) -' 1)) . 1 = (F | ((len F) -' 1)) /. 1 by PARTFUN1:def_6
.= F /. 1 by A21, FINSEQ_4:70
.= F . 1 by A8, PARTFUN1:def_6
.= |.(p . (1 -' 1)).| by A4, A8
.= |.(p . 0).| by XREAL_1:232 ;
then  Sum (F | ((len F) -' 1)) >= |.(p . 0).| by A21, A9, Th4;
then A22: Sum F >= |.(p . 0).| + 1 by A19, XREAL_1:6;
then A23: z <> 0. F_Complex by A17, A13, COMPLFLD:59;
G = G | (((len F) -' 1) + 1) by A3, A15, A5, FINSEQ_1:58
.= (G | ((len F) -' 1)) ^ <*(G /. (((len F) -' 1) + 1))*> by A3, A15, A5, FINSEQ_5:82 ;
then A24: Sum G = (Sum (G | ((len F) -' 1))) + (G /. (((len F) -' 1) + 1)) by FVSUM_1:71;
A25: dom F = dom G by A3, A15, FINSEQ_3:29;
then G /. (((len F) -' 1) + 1) = G . (((len F) -' 1) + 1) by A5, A18, PARTFUN1:def_6
.= (p . ((len F) -' 1)) * ((power F_Complex) . (z,((len F) -' 1))) by A16, A5, A18, A25 ;
then  |.(G /. (((len F) -' 1) + 1)).| = 1 * |.((power F_Complex) . (z,((len F) -' 1))).| by A2, A3, COMPLFLD:71;
then A26: |.(eval (p,z)).| >= |.((power F_Complex) . (z,((len F) -' 1))).| - |.(Sum (G | ((len F) -' 1))).| by A14, A24, COMPLFLD:64;
 1 = 1 + 0 ;
then A27: (len F) - 1 >= 0 by A7, A3, XREAL_1:19;
A28: len (F | ((len F) -' 1)) = (len F) -' 1 by A5, FINSEQ_1:59, NAT_1:11
.= len (G | ((len F) -' 1)) by A3, A15, A5, FINSEQ_1:59, NAT_1:11 ;
then A29: ( (F | ((len F) -' 1)) | (len (F | ((len F) -' 1))) = F | ((len F) -' 1) & (G | ((len F) -' 1)) | (len (F | ((len F) -' 1))) = G | ((len F) -' 1) ) by FINSEQ_1:58;
defpred S1[ Element of NAT ] means |.(Sum ((G | ((len F) -' 1)) | $1)).| <= (Sum ((F | ((len F) -' 1)) | $1)) * |.((power F_Complex) . (z,((len F) -' 2))).|;
 (len F) - 2 >= 0 by A20, XREAL_1:19;
then A30: ((len F) -' 2) + 1 = ((len F) - 2) + 1 by XREAL_0:def_2
.= (len F) -' 1 by A27, XREAL_0:def_2 ;
then  (power F_Complex) . (z,((len F) -' 1)) = ((power F_Complex) . (z,((len F) -' 2))) * z by GROUP_1:def_7;
then A31: |.((power F_Complex) . (z,((len F) -' 1))).| - (|.((power F_Complex) . (z,((len F) -' 2))).| * (Sum (F | ((len F) -' 1)))) = (|.((power F_Complex) . (z,((len F) -' 2))).| * |.z.|) - (|.((power F_Complex) . (z,((len F) -' 2))).| * (Sum (F | ((len F) -' 1)))) by COMPLFLD:71
.= |.((power F_Complex) . (z,((len F) -' 2))).| * (|.z.| - (Sum (F | ((len F) -' 1)))) ;
A32: |.z.| > |.(p . 0).| + 1 by A17, A22, XXREAL_0:2;
then A33: |.z.| > 1 by A13, XXREAL_0:2;
A34: dom (F | ((len F) -' 1)) = dom (G | ((len F) -' 1)) by A28, FINSEQ_3:29;
A35: for n being Element of NAT st S1[n] holds
S1[n + 1]
proof
let n be Element of NAT ; ::_thesis: ( S1[n] implies S1[n + 1] )
assume A36: |.(Sum ((G | ((len F) -' 1)) | n)).| <= (Sum ((F | ((len F) -' 1)) | n)) * |.((power F_Complex) . (z,((len F) -' 2))).| ; ::_thesis: S1[n + 1]
then A37: |.(Sum ((G | ((len F) -' 1)) | n)).| + |.((G | ((len F) -' 1)) /. (n + 1)).| <= ((Sum ((F | ((len F) -' 1)) | n)) * |.((power F_Complex) . (z,((len F) -' 2))).|) + |.((G | ((len F) -' 1)) /. (n + 1)).| by XREAL_1:6;
percases ( n + 1 <= len (G | ((len F) -' 1)) or n + 1 > len (G | ((len F) -' 1)) ) ;
supposeA38: n + 1 <= len (G | ((len F) -' 1)) ; ::_thesis: S1[n + 1]
then  n + 1 <= ((len F) -' 2) + 1 by A3, A15, A5, A30, FINSEQ_1:59, NAT_1:11;
then  n <= (len F) -' 2 by XREAL_1:6;
then  |.z.| to_power n <= |.z.| to_power ((len F) -' 2) by A33, PRE_FF:8;
then  |.z.| to_power n <= |.((power F_Complex) . (z,((len F) -' 2))).| by A23, Th7;
then A39: ( |.(p . n).| >= 0 & |.((power F_Complex) . (z,n)).| <= |.((power F_Complex) . (z,((len F) -' 2))).| ) by A23, Th7, COMPLEX1:46;
 (G | ((len F) -' 1)) | (n + 1) = ((G | ((len F) -' 1)) | n) ^ <*((G | ((len F) -' 1)) /. (n + 1))*> by A38, FINSEQ_5:82;
then  Sum ((G | ((len F) -' 1)) | (n + 1)) = (Sum ((G | ((len F) -' 1)) | n)) + ((G | ((len F) -' 1)) /. (n + 1)) by FVSUM_1:71;
then  |.(Sum ((G | ((len F) -' 1)) | (n + 1))).| <= |.(Sum ((G | ((len F) -' 1)) | n)).| + |.((G | ((len F) -' 1)) /. (n + 1)).| by COMPLFLD:62;
then A40: |.(Sum ((G | ((len F) -' 1)) | (n + 1))).| <= ((Sum ((F | ((len F) -' 1)) | n)) * |.((power F_Complex) . (z,((len F) -' 2))).|) + |.((G | ((len F) -' 1)) /. (n + 1)).| by A37, XXREAL_0:2;
A41: dom (G | ((len F) -' 1)) c= dom G by FINSEQ_5:18;
 n + 1 >= 1 by NAT_1:11;
then A42: n + 1 in dom (G | ((len F) -' 1)) by A38, FINSEQ_3:25;
then A43: (F | ((len F) -' 1)) /. (n + 1) = F /. (n + 1) by A34, FINSEQ_4:70
.= F . (n + 1) by A25, A42, A41, PARTFUN1:def_6
.= |.(p . ((n + 1) -' 1)).| by A4, A25, A42, A41
.= |.(p . n).| by NAT_D:34 ;
(G | ((len F) -' 1)) /. (n + 1) = G /. (n + 1) by A42, FINSEQ_4:70
.= G . (n + 1) by A42, A41, PARTFUN1:def_6
.= (p . ((n + 1) -' 1)) * ((power F_Complex) . (z,((n + 1) -' 1))) by A16, A42, A41
.= (p . n) * ((power F_Complex) . (z,((n + 1) -' 1))) by NAT_D:34
.= (p . n) * ((power F_Complex) . (z,n)) by NAT_D:34 ;
then  |.((G | ((len F) -' 1)) /. (n + 1)).| = ((F | ((len F) -' 1)) /. (n + 1)) * |.((power F_Complex) . (z,n)).| by A43, COMPLFLD:71;
then  |.((G | ((len F) -' 1)) /. (n + 1)).| <= ((F | ((len F) -' 1)) /. (n + 1)) * |.((power F_Complex) . (z,((len F) -' 2))).| by A43, A39, XREAL_1:64;
then A44: ((Sum ((F | ((len F) -' 1)) | n)) * |.((power F_Complex) . (z,((len F) -' 2))).|) + |.((G | ((len F) -' 1)) /. (n + 1)).| <= ((Sum ((F | ((len F) -' 1)) | n)) * |.((power F_Complex) . (z,((len F) -' 2))).|) + (((F | ((len F) -' 1)) /. (n + 1)) * |.((power F_Complex) . (z,((len F) -' 2))).|) by XREAL_1:6;
 (F | ((len F) -' 1)) | (n + 1) = ((F | ((len F) -' 1)) | n) ^ <*((F | ((len F) -' 1)) /. (n + 1))*> by A28, A38, FINSEQ_5:82;
then  Sum ((F | ((len F) -' 1)) | (n + 1)) = (Sum ((F | ((len F) -' 1)) | n)) + ((F | ((len F) -' 1)) /. (n + 1)) by RVSUM_1:74;
hence  S1[n + 1] by A40, A44, XXREAL_0:2; ::_thesis: verum
end;
supposeA45: n + 1 > len (G | ((len F) -' 1)) ; ::_thesis: S1[n + 1]
then  n >= len (G | ((len F) -' 1)) by NAT_1:13;
then A46: ( (G | ((len F) -' 1)) | n = G | ((len F) -' 1) & (F | ((len F) -' 1)) | n = F | ((len F) -' 1) ) by A28, FINSEQ_1:58;
 (G | ((len F) -' 1)) | (n + 1) = G | ((len F) -' 1) by A45, FINSEQ_1:58;
hence  S1[n + 1] by A28, A36, A45, A46, FINSEQ_1:58; ::_thesis: verum
end;
end;
end;
 (G | ((len F) -' 1)) | 0 = <*> the carrier of F_Complex ;
then A47: S1[ 0 ] by COMPLFLD:57, RLVECT_1:43, RVSUM_1:72;
 for n being Element of NAT holds S1[n] from NAT_1:sch_1(A47, A35);
then  |.(Sum (G | ((len F) -' 1))).| <= (Sum (F | ((len F) -' 1))) * |.((power F_Complex) . (z,((len F) -' 2))).| by A29;
then  |.((power F_Complex) . (z,((len F) -' 1))).| - |.(Sum (G | ((len F) -' 1))).| >= |.((power F_Complex) . (z,((len F) -' 1))).| - ((Sum (F | ((len F) -' 1))) * |.((power F_Complex) . (z,((len F) -' 2))).|) by XREAL_1:13;
then A48: |.(eval (p,z)).| >= |.((power F_Complex) . (z,((len F) -' 1))).| - (|.((power F_Complex) . (z,((len F) -' 2))).| * (Sum (F | ((len F) -' 1)))) by A26, XXREAL_0:2;
 len F >= 2 + 1 by A1, A3, NAT_1:13;
then  (len F) - 2 >= 1 by XREAL_1:19;
then  (len F) -' 2 >= 1 by XREAL_0:def_2;
then  |.z.| to_power ((len F) -' 2) >= |.z.| to_power 1 by A33, PRE_FF:8;
then  |.((power F_Complex) . (z,((len F) -' 2))).| >= |.z.| to_power 1 by A23, Th7;
then  |.((power F_Complex) . (z,((len F) -' 2))).| >= |.((power F_Complex) . (z,1)).| by A23, Th7;
then A49: |.((power F_Complex) . (z,((len F) -' 2))).| >= |.z.| by GROUP_1:50;
 ( |.((power F_Complex) . (z,((len F) -' 2))).| >= 0 & |.z.| - (Sum (F | ((len F) -' 1))) > 1 ) by A17, A19, COMPLEX1:46, XREAL_1:20;
then  |.((power F_Complex) . (z,((len F) -' 2))).| * (|.z.| - (Sum (F | ((len F) -' 1)))) >= |.((power F_Complex) . (z,((len F) -' 2))).| * 1 by XREAL_1:64;
then  |.(eval (p,z)).| >= |.((power F_Complex) . (z,((len F) -' 2))).| by A48, A31, XXREAL_0:2;
then  |.(eval (p,z)).| >= |.z.| by A49, XXREAL_0:2;
hence  |.(eval (p,z)).| > |.(p . 0).| + 1 by A32, XXREAL_0:2; ::_thesis: verum
end;

theorem Th73: :: POLYNOM5:73
for p being Polynomial of F_Complex st len p > 2 holds
ex z0 being Element of F_Complex st
for z being Element of F_Complex holds |.(eval (p,z)).| >= |.(eval (p,z0)).|
proof
defpred S1[ set ] means verum;
let p be Polynomial of F_Complex; ::_thesis: ( len p > 2 implies ex z0 being Element of F_Complex st
for z being Element of F_Complex holds |.(eval (p,z)).| >= |.(eval (p,z0)).| )
set np = NormPolynomial p;
deffunc H1( Element of F_Complex) ->  Element of REAL = |.(eval ((NormPolynomial p),$1)).|;
reconsider D =  {  H1(z) where z is Element of F_Complex : S1[z]  }  as Subset of REAL from DOMAIN_1:sch_8();
set q = lower_bound D;
A1: D is bounded_below
proof
take  0 ; :: according to XXREAL_2:def_9 ::_thesis: 0 is LowerBound of D
let b be ext-real number ; :: according to XXREAL_2:def_2 ::_thesis: ( not b in D or 0 <= b )
assume  b in D ; ::_thesis: 0 <= b
then  ex z being Element of F_Complex st b = |.(eval ((NormPolynomial p),z)).| ;
hence  0 <= b by COMPLEX1:46; ::_thesis: verum
end;
defpred S2[ Element of NAT , set ] means  ex g1 being Element of F_Complex st
( g1 = $2 & |.(eval ((NormPolynomial p),g1)).| < (lower_bound D) + (1 / ($1 + 1)) );
A2: |.(eval ((NormPolynomial p),(0. F_Complex))).| in D ;
A3: for n being Element of NAT ex g being Element of COMPLEX st S2[n,g]
proof
let n be Element of NAT ; ::_thesis: ex g being Element of COMPLEX st S2[n,g]
consider r being real number  such that
A4: r in D and
A5: r < (lower_bound D) + (1 / (n + 1)) by A2, A1, SEQ_4:def_2;
consider g1 being Element of F_Complex such that
A6: r = |.(eval ((NormPolynomial p),g1)).| by A4;
reconsider g = g1 as Element of COMPLEX by COMPLFLD:def_1;
take  g ; ::_thesis: S2[n,g]
take  g1 ; ::_thesis: ( g1 = g & |.(eval ((NormPolynomial p),g1)).| < (lower_bound D) + (1 / (n + 1)) )
thus  g1 = g ; ::_thesis: |.(eval ((NormPolynomial p),g1)).| < (lower_bound D) + (1 / (n + 1))
thus  |.(eval ((NormPolynomial p),g1)).| < (lower_bound D) + (1 / (n + 1)) by A5, A6; ::_thesis: verum
end;
consider G being Complex_Sequence such that
A7: for n being Element of NAT holds S2[n,G . n] from CFCONT_1:sch_1(A3);
deffunc H2( Nat) ->  Element of REAL = |.((NormPolynomial p) . ($1 -' 1)).|;
consider F being FinSequence of REAL  such that
A8: len F = len (NormPolynomial p) and
A9: for n being Nat st n in dom F holds
F . n = H2(n) from FINSEQ_2:sch_1();
 dom F = Seg (len (NormPolynomial p)) by A8, FINSEQ_1:def_3;
then A10: for n being Element of NAT st n in Seg (len (NormPolynomial p)) holds
F . n = H2(n) by A9;
assume A11: len p > 2 ; ::_thesis: ex z0 being Element of F_Complex st
for z being Element of F_Complex holds |.(eval (p,z)).| >= |.(eval (p,z0)).|
then A12: len p = ((len p) -' 1) + 1 by XREAL_1:235, XXREAL_0:2;
then  p . ((len p) -' 1) <> 0. F_Complex by ALGSEQ_1:10;
then A13: |.(p . ((len p) -' 1)).| > 0 by COMPLFLD:59;
A14: Seg (len (NormPolynomial p)) = dom F by A8, FINSEQ_1:def_3;
 G is bounded
proof
take r = (Sum F) + 1; :: according to COMSEQ_2:def_4 ::_thesis: for b1 being Element of NAT holds not r <= |.(G . b1).|
let n be Element of NAT ; ::_thesis: not r <= |.(G . n).|
consider Gn being Element of F_Complex such that
A15: Gn = G . n and
A16: |.(eval ((NormPolynomial p),Gn)).| < (lower_bound D) + (1 / (n + 1)) by A7;
 n + 1 >= 0 + 1 by XREAL_1:6;
then A17: 1 / (n + 1) <= 1 by XREAL_1:211;
A18: len (NormPolynomial p) = len p by A11, Th57;
then A19: (NormPolynomial p) . ((len (NormPolynomial p)) -' 1) = 1_ F_Complex by A11, Th56;
 |.(G . n).| <= Sum F
proof
 eval ((NormPolynomial p),(0. F_Complex)) = (NormPolynomial p) . 0 by Th31;
then  |.((NormPolynomial p) . 0).| in D ;
then  |.((NormPolynomial p) . 0).| >= lower_bound D by A1, SEQ_4:def_2;
then A20: |.((NormPolynomial p) . 0).| + 1 >= (lower_bound D) + (1 / (n + 1)) by A17, XREAL_1:7;
assume  |.(G . n).| > Sum F ; ::_thesis: contradiction
then  |.(eval ((NormPolynomial p),Gn)).| > |.((NormPolynomial p) . 0).| + 1 by A11, A8, A10, A14, A15, A18, A19, Th72, COMPLFLD:60;
hence  contradiction by A16, A20, XXREAL_0:2; ::_thesis: verum
end;
then  |.(G . n).| + 0 < r by XREAL_1:8;
hence  not r <= |.(G . n).| ; ::_thesis: verum
end;
then consider G1 being Complex_Sequence such that
A21: G1 is subsequence of G and
A22: G1 is convergent by COMSEQ_3:50;
defpred S3[ Element of NAT , set ] means  ex G1n being Element of F_Complex st
( G1n = G1 . $1 & $2 = eval ((NormPolynomial p),G1n) );
reconsider z0 = lim G1 as Element of F_Complex by COMPLFLD:def_1;
A23: for n being Element of NAT ex g being Element of COMPLEX st S3[n,g]
proof
let n be Element of NAT ; ::_thesis: ex g being Element of COMPLEX st S3[n,g]
reconsider G1n = G1 . n as Element of F_Complex by COMPLFLD:def_1;
reconsider g = eval ((NormPolynomial p),G1n) as Element of COMPLEX by COMPLFLD:def_1;
take  g ; ::_thesis: S3[n,g]
take  G1n ; ::_thesis: ( G1n = G1 . n & g = eval ((NormPolynomial p),G1n) )
thus  G1n = G1 . n ; ::_thesis: g = eval ((NormPolynomial p),G1n)
thus  g = eval ((NormPolynomial p),G1n) ; ::_thesis: verum
end;
consider H being Complex_Sequence such that
A24: for n being Element of NAT holds S3[n,H . n] from CFCONT_1:sch_1(A23);
reconsider enp0 = eval ((NormPolynomial p),z0) as Element of COMPLEX by COMPLFLD:def_1;
consider g being Element of COMPLEX  such that
A25: for p being Real st 0 < p holds
ex n being Element of NAT st
for m being Element of NAT st n <= m holds
|.((G1 . m) - g).| < p by A22, COMSEQ_2:def_5;
reconsider g1 = g as Element of F_Complex by COMPLFLD:def_1;
reconsider eg = eval ((NormPolynomial p),g1) as Element of COMPLEX by COMPLFLD:def_1;
now__::_thesis:_for_p_being_Real_st_0_<_p_holds_
ex_n_being_Element_of_NAT_st_
for_m_being_Element_of_NAT_st_n_<=_m_holds_
|.((H_._m)_-_eg).|_<_p
let p be Real; ::_thesis: ( 0 < p implies ex n being Element of NAT st
for m being Element of NAT st n <= m holds
|.((H . m) - eg).| < p )
consider fPF being Function of COMPLEX,COMPLEX such that
A26: fPF = Polynomial-Function (F_Complex,(NormPolynomial p)) and
A27: fPF is_continuous_on COMPLEX by Th71;
assume  0 < p ; ::_thesis: ex n being Element of NAT st
for m being Element of NAT st n <= m holds
|.((H . m) - eg).| < p
then consider p1 being Real such that
A28: 0 < p1 and
A29: for x1 being Element of COMPLEX st x1 in COMPLEX & |.(x1 - g).| < p1 holds
|.((fPF /. x1) - (fPF /. g)).| < p by A27, CFCONT_1:39;
consider n being Element of NAT  such that
A30: for m being Element of NAT st n <= m holds
|.((G1 . m) - g).| < p1 by A25, A28;
take n = n; ::_thesis: for m being Element of NAT st n <= m holds
|.((H . m) - eg).| < p
let m be Element of NAT ; ::_thesis: ( n <= m implies |.((H . m) - eg).| < p )
assume  n <= m ; ::_thesis: |.((H . m) - eg).| < p
then A31: |.((G1 . m) - g).| < p1 by A30;
 ex G1m being Element of F_Complex st
( G1m = G1 . m & H . m = eval ((NormPolynomial p),G1m) ) by A24;
then A32: H . m = fPF /. (G1 . m) by A26, Def12;
 eg = fPF /. g by A26, Def12;
hence  |.((H . m) - eg).| < p by A29, A31, A32; ::_thesis: verum
end;
then A33: H is convergent by COMSEQ_2:def_5;
consider PF being Function of COMPLEX,COMPLEX such that
A34: PF = Polynomial-Function (F_Complex,(NormPolynomial p)) and
A35: PF is_continuous_on COMPLEX by Th71;
now__::_thesis:_for_a_being_Real_st_0_<_a_holds_
ex_n_being_Element_of_NAT_st_
for_m_being_Element_of_NAT_st_n_<=_m_holds_
|.((H_._m)_-_enp0).|_<_a
let a be Real; ::_thesis: ( 0 < a implies ex n being Element of NAT st
for m being Element of NAT st n <= m holds
|.((H . m) - enp0).| < a )
assume  0 < a ; ::_thesis: ex n being Element of NAT st
for m being Element of NAT st n <= m holds
|.((H . m) - enp0).| < a
then consider s being Real such that
A36: 0 < s and
A37: for x1 being Element of COMPLEX st x1 in COMPLEX & |.(x1 - (lim G1)).| < s holds
|.((PF /. x1) - (PF /. (lim G1))).| < a by A35, CFCONT_1:39;
consider n being Element of NAT  such that
A38: for m being Element of NAT st n <= m holds
|.((G1 . m) - (lim G1)).| < s by A22, A36, COMSEQ_2:def_6;
take n = n; ::_thesis: for m being Element of NAT st n <= m holds
|.((H . m) - enp0).| < a
let m be Element of NAT ; ::_thesis: ( n <= m implies |.((H . m) - enp0).| < a )
assume  n <= m ; ::_thesis: |.((H . m) - enp0).| < a
then A39: |.((G1 . m) - (lim G1)).| < s by A38;
 ex G1m being Element of F_Complex st
( G1m = G1 . m & H . m = eval ((NormPolynomial p),G1m) ) by A24;
then A40: PF /. (G1 . m) = H . m by A34, Def12;
 PF /. (lim G1) = eval ((NormPolynomial p),z0) by A34, Def12;
hence  |.((H . m) - enp0).| < a by A37, A39, A40; ::_thesis: verum
end;
then A41: enp0 = lim H by A33, COMSEQ_2:def_6;
deffunc H3( Element of NAT ) ->  Element of REAL = 1 / ($1 + 1);
consider R being Real_Sequence such that
A42: for n being Element of NAT holds R . n = H3(n) from SEQ_1:sch_1();
take  z0 ; ::_thesis: for z being Element of F_Complex holds |.(eval (p,z)).| >= |.(eval (p,z0)).|
let z be Element of F_Complex; ::_thesis: |.(eval (p,z)).| >= |.(eval (p,z0)).|
reconsider Rcons = NAT --> |.(eval ((NormPolynomial p),z)).| as Real_Sequence ;
consider Nseq being V48() sequence of NAT such that
A43: G1 = G * Nseq by A21, VALUED_0:def_17;
 |.(eval ((NormPolynomial p),z)).| in D ;
then A44: |.(eval ((NormPolynomial p),z)).| >= lower_bound D by A1, SEQ_4:def_2;
A45: now__::_thesis:_for_n_being_Element_of_NAT_holds_Rcons_._n_>=_(|.H.|_-_R)_._n
let n be Element of NAT ; ::_thesis: Rcons . n >= (|.H.| - R) . n
consider G1n being Element of F_Complex such that
A46: G1n = G1 . n and
A47: H . n = eval ((NormPolynomial p),G1n) by A24;
consider gNn being Element of F_Complex such that
A48: gNn = G . (Nseq . n) and
A49: |.(eval ((NormPolynomial p),gNn)).| < (lower_bound D) + (1 / ((Nseq . n) + 1)) by A7;
 Nseq . n >= n by SEQM_3:14;
then  (Nseq . n) + 1 >= n + 1 by XREAL_1:6;
then  1 / ((Nseq . n) + 1) <= 1 / (n + 1) by XREAL_1:85;
then  (lower_bound D) + (1 / ((Nseq . n) + 1)) <= (lower_bound D) + (1 / (n + 1)) by XREAL_1:6;
then  |.(eval ((NormPolynomial p),gNn)).| < (lower_bound D) + (1 / (n + 1)) by A49, XXREAL_0:2;
then  lower_bound D > |.(eval ((NormPolynomial p),gNn)).| - (1 / (n + 1)) by XREAL_1:19;
then A50: ( Rcons . n = |.(eval ((NormPolynomial p),z)).| & |.(eval ((NormPolynomial p),z)).| > |.(eval ((NormPolynomial p),gNn)).| - (1 / (n + 1)) ) by A44, FUNCOP_1:7, XXREAL_0:2;
 dom (|.H.| - R) = NAT by FUNCT_2:def_1;
then (|.H.| - R) . n = (|.H.| . n) - (R . n) by VALUED_1:13
.= (|.H.| . n) - (1 / (n + 1)) by A42
.= |.(eval ((NormPolynomial p),G1n)).| - (1 / (n + 1)) by A47, VALUED_1:18 ;
hence  Rcons . n >= (|.H.| - R) . n by A43, A46, A48, A50, FUNCT_2:15; ::_thesis: verum
end;
A51: R is convergent by A42, SEQ_4:28;
then  |.H.| - R is convergent by A33;
then  ( Rcons . 0 = |.(eval ((NormPolynomial p),z)).| & lim (|.H.| - R) <= lim Rcons ) by A45, FUNCOP_1:7, SEQ_2:18;
then A52: lim (|.H.| - R) <= |.(eval ((NormPolynomial p),z)).| by SEQ_4:25;
lim (|.H.| - R) = (lim |.H.|) - (lim R) by A33, A51, SEQ_2:12
.= |.(lim H).| - (lim R) by A33, SEQ_2:27
.= |.(lim H).| - 0 by A42, SEQ_4:29 ;
then  |.((eval (p,z)) / (p . ((len p) -' 1))).| >= |.(eval ((NormPolynomial p),z0)).| by A11, A52, A41, Th58;
then  |.((eval (p,z)) / (p . ((len p) -' 1))).| >= |.((eval (p,z0)) / (p . ((len p) -' 1))).| by A11, Th58;
then  |.(eval (p,z)).| / |.(p . ((len p) -' 1)).| >= |.((eval (p,z0)) / (p . ((len p) -' 1))).| by A12, ALGSEQ_1:10, COMPLFLD:73;
then  |.(eval (p,z)).| / |.(p . ((len p) -' 1)).| >= |.(eval (p,z0)).| / |.(p . ((len p) -' 1)).| by A12, ALGSEQ_1:10, COMPLFLD:73;
hence  |.(eval (p,z)).| >= |.(eval (p,z0)).| by A13, XREAL_1:74; ::_thesis: verum
end;

theorem Th74: :: POLYNOM5:74
for p being Polynomial of F_Complex st len p > 1 holds
p is with_roots
proof
let p be Polynomial of F_Complex; ::_thesis: ( len p > 1 implies p is with_roots )
assume A1: len p > 1 ; ::_thesis: p is with_roots
then A2: len p >= 1 + 1 by NAT_1:13;
percases ( len p > 2 or len p = 2 ) by A2, XXREAL_0:1;
suppose len p > 2 ; ::_thesis: p is with_roots
then consider z0 being Element of F_Complex such that
A3: for z being Element of F_Complex holds |.(eval (p,z)).| >= |.(eval (p,z0)).| by Th73;
set q = Subst (p,<%z0,(1_ F_Complex)%>);
defpred S1[ Nat] means ( $1 >= 1 & (Subst (p,<%z0,(1_ F_Complex)%>)) . $1 <> 0. F_Complex );
 len <%z0,(1_ F_Complex)%> = 2 by Th40;
then A4: len (Subst (p,<%z0,(1_ F_Complex)%>)) = (((2 * (len p)) - (len p)) - 2) + 2 by A1, Th52
.= len p ;
A5: ex k being Nat st S1[k]
proof
 (len (Subst (p,<%z0,(1_ F_Complex)%>))) - 1 >= 1 - 1 by A1, A4, XREAL_1:9;
then  (len (Subst (p,<%z0,(1_ F_Complex)%>))) - 1 = (len (Subst (p,<%z0,(1_ F_Complex)%>))) -' 1 by XREAL_0:def_2;
then reconsider k = (len (Subst (p,<%z0,(1_ F_Complex)%>))) - 1 as Element of NAT ;
take  k ; ::_thesis: S1[k]
 len (Subst (p,<%z0,(1_ F_Complex)%>)) >= 1 + 1 by A1, A4, NAT_1:13;
hence  k >= 1 by XREAL_1:19; ::_thesis: (Subst (p,<%z0,(1_ F_Complex)%>)) . k <> 0. F_Complex
 len (Subst (p,<%z0,(1_ F_Complex)%>)) = k + 1 ;
hence  (Subst (p,<%z0,(1_ F_Complex)%>)) . k <> 0. F_Complex by ALGSEQ_1:10; ::_thesis: verum
end;
consider k being Nat such that
A6: S1[k] and
A7: for n being Nat st S1[n] holds
k <= n from NAT_1:sch_5(A5);
A8: k + 1 > 1 by A6, NAT_1:13;
reconsider k1 = k as non empty Element of NAT by A6, ORDINAL1:def_12;
set sq = the CRoot of k1, - (((Subst (p,<%z0,(1_ F_Complex)%>)) . 0) / ((Subst (p,<%z0,(1_ F_Complex)%>)) . k1));
deffunc H1( Nat) ->  Element of the carrier of F_Complex = ((Subst (p,<%z0,(1_ F_Complex)%>)) . (k1 + $1)) * ((power F_Complex) . ( the CRoot of k1, - (((Subst (p,<%z0,(1_ F_Complex)%>)) . 0) / ((Subst (p,<%z0,(1_ F_Complex)%>)) . k1)),(k1 + $1)));
consider F2 being FinSequence of the carrier of F_Complex such that
A9: len F2 = (len (Subst (p,<%z0,(1_ F_Complex)%>))) -' (k1 + 1) and
A10: for n being Nat st n in dom F2 holds
F2 . n = H1(n) from FINSEQ_2:sch_1();
 k1 < len (Subst (p,<%z0,(1_ F_Complex)%>)) by A6, ALGSEQ_1:8;
then A11: (k + 1) + 0 <= len (Subst (p,<%z0,(1_ F_Complex)%>)) by NAT_1:13;
then  (len (Subst (p,<%z0,(1_ F_Complex)%>))) - (k + 1) >= 0 by XREAL_1:19;
then A12: len F2 = (len (Subst (p,<%z0,(1_ F_Complex)%>))) - (k + 1) by A9, XREAL_0:def_2;
A13: eval (p,z0) = eval (p,(z0 + (0. F_Complex))) by RLVECT_1:def_4
.= eval (p,(eval (<%z0,(1_ F_Complex)%>,(0. F_Complex)))) by Th47
.= eval ((Subst (p,<%z0,(1_ F_Complex)%>)),(0. F_Complex)) by Th53 ;
A14: now__::_thesis:_for_z_being_Element_of_F_Complex_holds_|.(eval_((Subst_(p,<%z0,(1__F_Complex)%>)),z)).|_>=_|.((Subst_(p,<%z0,(1__F_Complex)%>))_._0).|
let z be Element of F_Complex; ::_thesis: |.(eval ((Subst (p,<%z0,(1_ F_Complex)%>)),z)).| >= |.((Subst (p,<%z0,(1_ F_Complex)%>)) . 0).|
eval ((Subst (p,<%z0,(1_ F_Complex)%>)),z) = eval (p,(eval (<%z0,(1_ F_Complex)%>,z))) by Th53
.= eval (p,(z0 + z)) by Th47 ;
then  |.(eval ((Subst (p,<%z0,(1_ F_Complex)%>)),z)).| >= |.(eval (p,z0)).| by A3;
hence  |.(eval ((Subst (p,<%z0,(1_ F_Complex)%>)),z)).| >= |.((Subst (p,<%z0,(1_ F_Complex)%>)) . 0).| by A13, Th31; ::_thesis: verum
end;
now__::_thesis:_for_c_being_Real_st_0_<_c_&_c_<_1_holds_
c_*_(Sum_|.F2.|)_>=_|.((Subst_(p,<%z0,(1__F_Complex)%>))_._0).|
let c be Real; ::_thesis: ( 0 < c & c < 1 implies c * (Sum |.F2.|) >= |.((Subst (p,<%z0,(1_ F_Complex)%>)) . 0).| )
assume that
A15: 0 < c and
A16: c < 1 ; ::_thesis: c * (Sum |.F2.|) >= |.((Subst (p,<%z0,(1_ F_Complex)%>)) . 0).|
set z1 = [**c,0**] * the CRoot of k1, - (((Subst (p,<%z0,(1_ F_Complex)%>)) . 0) / ((Subst (p,<%z0,(1_ F_Complex)%>)) . k1));
consider F1 being FinSequence of the carrier of F_Complex such that
A17: eval ((Subst (p,<%z0,(1_ F_Complex)%>)),([**c,0**] * the CRoot of k1, - (((Subst (p,<%z0,(1_ F_Complex)%>)) . 0) / ((Subst (p,<%z0,(1_ F_Complex)%>)) . k1)))) = Sum F1 and
A18: len F1 = len (Subst (p,<%z0,(1_ F_Complex)%>)) and
A19: for n being Element of NAT st n in dom F1 holds
F1 . n = ((Subst (p,<%z0,(1_ F_Complex)%>)) . (n -' 1)) * ((power F_Complex) . (([**c,0**] * the CRoot of k1, - (((Subst (p,<%z0,(1_ F_Complex)%>)) . 0) / ((Subst (p,<%z0,(1_ F_Complex)%>)) . k1))),(n -' 1))) by POLYNOM4:def_2;
A20: dom ((F1 /^ (k + 1)) * ([**(c to_power (k + 1)),0**] ")) = dom (F1 /^ (k + 1)) by POLYNOM1:def_2;
A21: k1 < len F1 by A6, A18, ALGSEQ_1:8;
 1 in Seg k by A6, FINSEQ_1:1;
then  1 in Seg (len (F1 | k)) by A21, FINSEQ_1:59;
then A22: 1 in dom (F1 | k) by FINSEQ_1:def_3;
A23: dom (F1 | k) c= dom F1 by FINSEQ_5:18;
now__::_thesis:_for_i_being_Element_of_NAT_st_i_in_dom_(F1_|_k)_&_i_<>_1_holds_
(F1_|_k1)_/._i_=_0._F_Complex
let i be Element of NAT ; ::_thesis: ( i in dom (F1 | k) & i <> 1 implies (F1 | k1) /. i = 0. F_Complex )
assume that
A24: i in dom (F1 | k) and
A25: i <> 1 ; ::_thesis: (F1 | k1) /. i = 0. F_Complex
A26: 0 + 1 <= i by A24, FINSEQ_3:25;
then  i > 1 by A25, XXREAL_0:1;
then  i >= 1 + 1 by NAT_1:13;
then  i - 1 >= (1 + 1) - 1 by XREAL_1:9;
then A27: i -' 1 >= 1 by XREAL_0:def_2;
 i <= len (F1 | k) by A24, FINSEQ_3:25;
then  i <= k by A21, FINSEQ_1:59;
then  i < k + 1 by NAT_1:13;
then A28: i - 1 < k by XREAL_1:19;
 i - 1 >= 0 by A26, XREAL_1:19;
then A29: i -' 1 < k by A28, XREAL_0:def_2;
thus (F1 | k1) /. i = F1 /. i by A24, FINSEQ_4:70
.= F1 . i by A23, A24, PARTFUN1:def_6
.= ((Subst (p,<%z0,(1_ F_Complex)%>)) . (i -' 1)) * ((power F_Complex) . (([**c,0**] * the CRoot of k1, - (((Subst (p,<%z0,(1_ F_Complex)%>)) . 0) / ((Subst (p,<%z0,(1_ F_Complex)%>)) . k1))),(i -' 1))) by A19, A23, A24
.= (0. F_Complex) * ((power F_Complex) . (([**c,0**] * the CRoot of k1, - (((Subst (p,<%z0,(1_ F_Complex)%>)) . 0) / ((Subst (p,<%z0,(1_ F_Complex)%>)) . k1))),(i -' 1))) by A7, A27, A29
.= 0. F_Complex by VECTSP_1:7 ; ::_thesis: verum
end;
then A30: Sum (F1 | k) = (F1 | k1) /. 1 by A22, POLYNOM2:3
.= F1 /. 1 by A22, FINSEQ_4:70
.= F1 . 1 by A22, A23, PARTFUN1:def_6
.= ((Subst (p,<%z0,(1_ F_Complex)%>)) . (1 -' 1)) * ((power F_Complex) . (([**c,0**] * the CRoot of k1, - (((Subst (p,<%z0,(1_ F_Complex)%>)) . 0) / ((Subst (p,<%z0,(1_ F_Complex)%>)) . k1))),(1 -' 1))) by A19, A22, A23
.= ((Subst (p,<%z0,(1_ F_Complex)%>)) . 0) * ((power F_Complex) . (([**c,0**] * the CRoot of k1, - (((Subst (p,<%z0,(1_ F_Complex)%>)) . 0) / ((Subst (p,<%z0,(1_ F_Complex)%>)) . k1))),(1 -' 1))) by XREAL_1:232
.= ((Subst (p,<%z0,(1_ F_Complex)%>)) . 0) * ((power F_Complex) . (([**c,0**] * the CRoot of k1, - (((Subst (p,<%z0,(1_ F_Complex)%>)) . 0) / ((Subst (p,<%z0,(1_ F_Complex)%>)) . k1))),0)) by XREAL_1:232
.= ((Subst (p,<%z0,(1_ F_Complex)%>)) . 0) * (1_ F_Complex) by GROUP_1:def_7
.= (Subst (p,<%z0,(1_ F_Complex)%>)) . 0 by GROUP_1:def_4 ;
 k + 1 in Seg (len F1) by A8, A11, A18, FINSEQ_1:1;
then A31: k + 1 in dom F1 by FINSEQ_1:def_3;
then A32: F1 . (k + 1) = F1 /. (k + 1) by PARTFUN1:def_6;
set gc = (Sum (F1 /^ (k + 1))) / [**(c to_power (k + 1)),0**];
A33: c to_power (k + 1) > 0 by A15, POWER:34;
then A34: Sum (F1 /^ (k + 1)) = ([**(c to_power (k + 1)),0**] * (Sum (F1 /^ (k + 1)))) / [**(c to_power (k + 1)),0**] by COMPLFLD:7, COMPLFLD:30
.= [**(c to_power (k + 1)),0**] * ((Sum (F1 /^ (k + 1))) / [**(c to_power (k + 1)),0**]) by A33, COMPLFLD:7, COMPLFLD:28 ;
A35: F1 /. (k + 1) = F1 . (k + 1) by A31, PARTFUN1:def_6
.= ((Subst (p,<%z0,(1_ F_Complex)%>)) . ((k + 1) -' 1)) * ((power F_Complex) . (([**c,0**] * the CRoot of k1, - (((Subst (p,<%z0,(1_ F_Complex)%>)) . 0) / ((Subst (p,<%z0,(1_ F_Complex)%>)) . k1))),((k + 1) -' 1))) by A19, A31
.= ((Subst (p,<%z0,(1_ F_Complex)%>)) . k1) * ((power F_Complex) . (([**c,0**] * the CRoot of k1, - (((Subst (p,<%z0,(1_ F_Complex)%>)) . 0) / ((Subst (p,<%z0,(1_ F_Complex)%>)) . k1))),((k + 1) -' 1))) by NAT_D:34
.= ((Subst (p,<%z0,(1_ F_Complex)%>)) . k1) * ((power F_Complex) . (([**c,0**] * the CRoot of k1, - (((Subst (p,<%z0,(1_ F_Complex)%>)) . 0) / ((Subst (p,<%z0,(1_ F_Complex)%>)) . k1))),k1)) by NAT_D:34
.= ((Subst (p,<%z0,(1_ F_Complex)%>)) . k1) * (((power F_Complex) . ([**c,0**],k1)) * ((power F_Complex) . ( the CRoot of k1, - (((Subst (p,<%z0,(1_ F_Complex)%>)) . 0) / ((Subst (p,<%z0,(1_ F_Complex)%>)) . k1)),k1))) by GROUP_1:52
.= ((Subst (p,<%z0,(1_ F_Complex)%>)) . k1) * (((power F_Complex) . ([**c,0**],k1)) * (- (((Subst (p,<%z0,(1_ F_Complex)%>)) . 0) / ((Subst (p,<%z0,(1_ F_Complex)%>)) . k1)))) by COMPLFLD:def_2
.= (((Subst (p,<%z0,(1_ F_Complex)%>)) . k1) * (- (((Subst (p,<%z0,(1_ F_Complex)%>)) . 0) / ((Subst (p,<%z0,(1_ F_Complex)%>)) . k1)))) * ((power F_Complex) . ([**c,0**],k1))
.= (((Subst (p,<%z0,(1_ F_Complex)%>)) . k1) * ((- ((Subst (p,<%z0,(1_ F_Complex)%>)) . 0)) / ((Subst (p,<%z0,(1_ F_Complex)%>)) . k1))) * ((power F_Complex) . ([**c,0**],k1)) by A6, COMPLFLD:42
.= ((((Subst (p,<%z0,(1_ F_Complex)%>)) . k1) * (- ((Subst (p,<%z0,(1_ F_Complex)%>)) . 0))) / ((Subst (p,<%z0,(1_ F_Complex)%>)) . k1)) * ((power F_Complex) . ([**c,0**],k1)) by A6, COMPLFLD:28
.= (- ((Subst (p,<%z0,(1_ F_Complex)%>)) . 0)) * ((power F_Complex) . ([**c,0**],k1)) by A6, COMPLFLD:30
.= (- ((Subst (p,<%z0,(1_ F_Complex)%>)) . 0)) * [**(c to_power k),0**] by A15, HAHNBAN1:29 ;
A36: |.((((Subst (p,<%z0,(1_ F_Complex)%>)) . 0) * ((1_ F_Complex) - [**(c to_power k),0**])) + ([**(c to_power (k + 1)),0**] * ((Sum (F1 /^ (k + 1))) / [**(c to_power (k + 1)),0**]))).| <= |.(((Subst (p,<%z0,(1_ F_Complex)%>)) . 0) * ((1_ F_Complex) - [**(c to_power k),0**])).| + |.([**(c to_power (k + 1)),0**] * ((Sum (F1 /^ (k + 1))) / [**(c to_power (k + 1)),0**])).| by COMPLFLD:62;
 F1 = ((F1 | ((k + 1) -' 1)) ^ <*(F1 . (k + 1))*>) ^ (F1 /^ (k + 1)) by A8, A11, A18, POLYNOM4:1;
then  Sum F1 = (Sum ((F1 | ((k + 1) -' 1)) ^ <*(F1 /. (k + 1))*>)) + (Sum (F1 /^ (k + 1))) by A32, RLVECT_1:41
.= ((Sum (F1 | ((k + 1) -' 1))) + (Sum <*(F1 /. (k + 1))*>)) + (Sum (F1 /^ (k + 1))) by RLVECT_1:41
.= ((Sum (F1 | k)) + (Sum <*(F1 /. (k + 1))*>)) + (Sum (F1 /^ (k + 1))) by NAT_D:34
.= (((Subst (p,<%z0,(1_ F_Complex)%>)) . 0) + ((- ((Subst (p,<%z0,(1_ F_Complex)%>)) . 0)) * [**(c to_power k),0**])) + (Sum (F1 /^ (k + 1))) by A30, A35, RLVECT_1:44
.= (((Subst (p,<%z0,(1_ F_Complex)%>)) . 0) + (- (((Subst (p,<%z0,(1_ F_Complex)%>)) . 0) * [**(c to_power k),0**]))) + (Sum (F1 /^ (k + 1))) by VECTSP_1:9
.= ((((Subst (p,<%z0,(1_ F_Complex)%>)) . 0) * (1_ F_Complex)) - (((Subst (p,<%z0,(1_ F_Complex)%>)) . 0) * [**(c to_power k),0**])) + (Sum (F1 /^ (k + 1))) by VECTSP_1:def_4
.= (((Subst (p,<%z0,(1_ F_Complex)%>)) . 0) * ((1_ F_Complex) - [**(c to_power k),0**])) + ([**(c to_power (k + 1)),0**] * ((Sum (F1 /^ (k + 1))) / [**(c to_power (k + 1)),0**])) by A34, VECTSP_1:11 ;
then  |.((((Subst (p,<%z0,(1_ F_Complex)%>)) . 0) * ((1_ F_Complex) - [**(c to_power k),0**])) + ([**(c to_power (k + 1)),0**] * ((Sum (F1 /^ (k + 1))) / [**(c to_power (k + 1)),0**]))).| >= |.((Subst (p,<%z0,(1_ F_Complex)%>)) . 0).| by A14, A17;
then  |.(((Subst (p,<%z0,(1_ F_Complex)%>)) . 0) * ((1_ F_Complex) - [**(c to_power k),0**])).| + |.([**(c to_power (k + 1)),0**] * ((Sum (F1 /^ (k + 1))) / [**(c to_power (k + 1)),0**])).| >= |.((Subst (p,<%z0,(1_ F_Complex)%>)) . 0).| by A36, XXREAL_0:2;
then  (|.((Subst (p,<%z0,(1_ F_Complex)%>)) . 0).| * |.((1_ F_Complex) - [**(c to_power k),0**]).|) + |.([**(c to_power (k + 1)),0**] * ((Sum (F1 /^ (k + 1))) / [**(c to_power (k + 1)),0**])).| >= |.((Subst (p,<%z0,(1_ F_Complex)%>)) . 0).| by COMPLFLD:71;
then A37: (|.((Subst (p,<%z0,(1_ F_Complex)%>)) . 0).| * |.((1_ F_Complex) - [**(c to_power k),0**]).|) + (|.[**(c to_power (k + 1)),0**].| * |.((Sum (F1 /^ (k + 1))) / [**(c to_power (k + 1)),0**]).|) >= |.((Subst (p,<%z0,(1_ F_Complex)%>)) . 0).| by COMPLFLD:71;
 0 + (c to_power k1) <= 1 by A15, A16, TBSP_1:2;
then A38: 1 - (c to_power k) >= 0 by XREAL_1:19;
A39: c to_power k > 0 by A15, POWER:34;
A40: len |.((F1 /^ (k + 1)) * ([**(c to_power (k + 1)),0**] ")).| = len ((F1 /^ (k + 1)) * ([**(c to_power (k + 1)),0**] ")) by Def1
.= len (F1 /^ (k + 1)) by A20, FINSEQ_3:29
.= (len F1) - (k + 1) by A11, A18, RFINSEQ:def_1
.= len |.F2.| by A12, A18, Def1 ;
now__::_thesis:_for_i_being_Element_of_NAT_st_i_in_dom_|.((F1_/^_(k_+_1))_*_([**(c_to_power_(k_+_1)),0**]_")).|_holds_
|.((F1_/^_(k_+_1))_*_([**(c_to_power_(k_+_1)),0**]_")).|_._i_<=_|.F2.|_._i
let i be Element of NAT ; ::_thesis: ( i in dom |.((F1 /^ (k + 1)) * ([**(c to_power (k + 1)),0**] ")).| implies |.((F1 /^ (k + 1)) * ([**(c to_power (k + 1)),0**] ")).| . i <= |.F2.| . i )
A41: ((k + 1) + i) -' 1 = ((k + i) + 1) - 1 by XREAL_0:def_2
.= k + i ;
assume A42: i in dom |.((F1 /^ (k + 1)) * ([**(c to_power (k + 1)),0**] ")).| ; ::_thesis: |.((F1 /^ (k + 1)) * ([**(c to_power (k + 1)),0**] ")).| . i <= |.F2.| . i
then A43: i in Seg (len |.((F1 /^ (k + 1)) * ([**(c to_power (k + 1)),0**] ")).|) by FINSEQ_1:def_3;
then  i <= len |.F2.| by A40, FINSEQ_1:1;
then  i <= (len F1) - (k + 1) by A12, A18, Def1;
then  ( (k + i) + 1 >= 0 + 1 & (k + 1) + i <= len F1 ) by XREAL_1:6, XREAL_1:19;
then A44: (k + 1) + i in dom F1 by FINSEQ_3:25;
 i >= 0 + 1 by A43, FINSEQ_1:1;
then A45: i - 1 >= 0 by XREAL_1:19;
 c to_power (i -' 1) <= 1 by A15, A16, TBSP_1:2;
then A46: c to_power (i - 1) <= 1 by A45, XREAL_0:def_2;
A47: c to_power (k + i) > 0 by A15, POWER:34;
A48: (k + i) - (k + 1) = i - 1 ;
 i in Seg (len ((F1 /^ (k + 1)) * ([**(c to_power (k + 1)),0**] "))) by A43, Def1;
then A49: i in dom ((F1 /^ (k + 1)) * ([**(c to_power (k + 1)),0**] ")) by FINSEQ_1:def_3;
then A50: (F1 /^ (k + 1)) /. i = (F1 /^ (k + 1)) . i by A20, PARTFUN1:def_6
.= F1 . ((k + 1) + i) by A11, A18, A20, A49, RFINSEQ:def_1
.= ((Subst (p,<%z0,(1_ F_Complex)%>)) . (((k + 1) + i) -' 1)) * ((power F_Complex) . (([**c,0**] * the CRoot of k1, - (((Subst (p,<%z0,(1_ F_Complex)%>)) . 0) / ((Subst (p,<%z0,(1_ F_Complex)%>)) . k1))),(((k + 1) + i) -' 1))) by A19, A44
.= ((Subst (p,<%z0,(1_ F_Complex)%>)) . (k + i)) * (((power F_Complex) . ( the CRoot of k1, - (((Subst (p,<%z0,(1_ F_Complex)%>)) . 0) / ((Subst (p,<%z0,(1_ F_Complex)%>)) . k1)),(k + i))) * ((power F_Complex) . ([**c,0**],(k + i)))) by A41, GROUP_1:52
.= (((Subst (p,<%z0,(1_ F_Complex)%>)) . (k + i)) * ((power F_Complex) . ( the CRoot of k1, - (((Subst (p,<%z0,(1_ F_Complex)%>)) . 0) / ((Subst (p,<%z0,(1_ F_Complex)%>)) . k1)),(k + i)))) * ((power F_Complex) . ([**c,0**],(k + i))) ;
A51: len F2 = len |.F2.| by Def1;
then A52: dom F2 = dom |.F2.| by FINSEQ_3:29;
A53: |.((F1 /^ (k + 1)) * ([**(c to_power (k + 1)),0**] ")).| . i = |.((F1 /^ (k + 1)) * ([**(c to_power (k + 1)),0**] ")).| /. i by A42, PARTFUN1:def_6
.= |.(((F1 /^ (k + 1)) * ([**(c to_power (k + 1)),0**] ")) /. i).| by A49, Def1
.= |.(((F1 /^ (k + 1)) /. i) * ([**(c to_power (k + 1)),0**] ")).| by A20, A49, POLYNOM1:def_2
.= |.((F1 /^ (k + 1)) /. i).| * |.([**(c to_power (k + 1)),0**] ").| by COMPLFLD:71
.= |.((((Subst (p,<%z0,(1_ F_Complex)%>)) . (k + i)) * ((power F_Complex) . ( the CRoot of k1, - (((Subst (p,<%z0,(1_ F_Complex)%>)) . 0) / ((Subst (p,<%z0,(1_ F_Complex)%>)) . k1)),(k + i)))) * ((power F_Complex) . ([**c,0**],(k + i)))).| * ((abs (c to_power (k + 1))) ") by A33, A50, COMPLFLD:7, COMPLFLD:72
.= (|.(((Subst (p,<%z0,(1_ F_Complex)%>)) . (k + i)) * ((power F_Complex) . ( the CRoot of k1, - (((Subst (p,<%z0,(1_ F_Complex)%>)) . 0) / ((Subst (p,<%z0,(1_ F_Complex)%>)) . k1)),(k + i)))).| * |.((power F_Complex) . ([**c,0**],(k + i))).|) * ((abs (c to_power (k + 1))) ") by COMPLFLD:71
.= (|.(((Subst (p,<%z0,(1_ F_Complex)%>)) . (k + i)) * ((power F_Complex) . ( the CRoot of k1, - (((Subst (p,<%z0,(1_ F_Complex)%>)) . 0) / ((Subst (p,<%z0,(1_ F_Complex)%>)) . k1)),(k + i)))).| * |.[**(c to_power (k + i)),0**].|) * ((abs (c to_power (k + 1))) ") by A15, HAHNBAN1:29
.= (|.(((Subst (p,<%z0,(1_ F_Complex)%>)) . (k + i)) * ((power F_Complex) . ( the CRoot of k1, - (((Subst (p,<%z0,(1_ F_Complex)%>)) . 0) / ((Subst (p,<%z0,(1_ F_Complex)%>)) . k1)),(k + i)))).| * (c to_power (k + i))) * ((abs (c to_power (k + 1))) ") by A47, ABSVALUE:def_1
.= (|.(((Subst (p,<%z0,(1_ F_Complex)%>)) . (k + i)) * ((power F_Complex) . ( the CRoot of k1, - (((Subst (p,<%z0,(1_ F_Complex)%>)) . 0) / ((Subst (p,<%z0,(1_ F_Complex)%>)) . k1)),(k + i)))).| * (c to_power (k + i))) * ((c to_power (k + 1)) ") by A33, ABSVALUE:def_1
.= |.(((Subst (p,<%z0,(1_ F_Complex)%>)) . (k + i)) * ((power F_Complex) . ( the CRoot of k1, - (((Subst (p,<%z0,(1_ F_Complex)%>)) . 0) / ((Subst (p,<%z0,(1_ F_Complex)%>)) . k1)),(k + i)))).| * ((c to_power (k + i)) * ((c to_power (k + 1)) "))
.= |.(((Subst (p,<%z0,(1_ F_Complex)%>)) . (k + i)) * ((power F_Complex) . ( the CRoot of k1, - (((Subst (p,<%z0,(1_ F_Complex)%>)) . 0) / ((Subst (p,<%z0,(1_ F_Complex)%>)) . k1)),(k + i)))).| * ((c to_power (k + i)) / (c to_power (k + 1)))
.= |.(((Subst (p,<%z0,(1_ F_Complex)%>)) . (k + i)) * ((power F_Complex) . ( the CRoot of k1, - (((Subst (p,<%z0,(1_ F_Complex)%>)) . 0) / ((Subst (p,<%z0,(1_ F_Complex)%>)) . k1)),(k + i)))).| * (c to_power (i - 1)) by A15, A48, POWER:29 ;
A54: i in dom F2 by A40, A43, A51, FINSEQ_1:def_3;
then ((Subst (p,<%z0,(1_ F_Complex)%>)) . (k + i)) * ((power F_Complex) . ( the CRoot of k1, - (((Subst (p,<%z0,(1_ F_Complex)%>)) . 0) / ((Subst (p,<%z0,(1_ F_Complex)%>)) . k1)),(k + i))) = F2 . i by A10
.= F2 /. i by A54, PARTFUN1:def_6 ;
then  |.((F1 /^ (k + 1)) * ([**(c to_power (k + 1)),0**] ")).| . i <= |.(F2 /. i).| by A46, A53, COMPLEX1:46, XREAL_1:153;
then  |.((F1 /^ (k + 1)) * ([**(c to_power (k + 1)),0**] ")).| . i <= |.F2.| /. i by A54, Def1;
hence  |.((F1 /^ (k + 1)) * ([**(c to_power (k + 1)),0**] ")).| . i <= |.F2.| . i by A52, A54, PARTFUN1:def_6; ::_thesis: verum
end;
then A55: Sum |.((F1 /^ (k + 1)) * ([**(c to_power (k + 1)),0**] ")).| <= Sum |.F2.| by A40, INTEGRA5:3;
|.((1_ F_Complex) - [**(c to_power k),0**]).| = |.([**1,0**] - [**(c to_power k),0**]).| by COMPLEX1:def_4, COMPLFLD:8
.= |.[**(1 - (c to_power k1)),(0 - 0)**].| by Th6
.= 1 - (c to_power k) by A38, ABSVALUE:def_1 ;
then  |.[**(c to_power (k + 1)),0**].| * |.((Sum (F1 /^ (k + 1))) / [**(c to_power (k + 1)),0**]).| >= (|.((Subst (p,<%z0,(1_ F_Complex)%>)) . 0).| * 1) - (|.((Subst (p,<%z0,(1_ F_Complex)%>)) . 0).| * (1 - (c to_power k))) by A37, XREAL_1:20;
then  (c to_power (k + 1)) * |.((Sum (F1 /^ (k + 1))) / [**(c to_power (k + 1)),0**]).| >= |.((Subst (p,<%z0,(1_ F_Complex)%>)) . 0).| * (c to_power k) by A33, ABSVALUE:def_1;
then  ((c to_power (k + 1)) * |.((Sum (F1 /^ (k + 1))) / [**(c to_power (k + 1)),0**]).|) / (c to_power k) >= (|.((Subst (p,<%z0,(1_ F_Complex)%>)) . 0).| * (c to_power k)) / (c to_power k) by A39, XREAL_1:72;
then  ((c to_power (k + 1)) / (c to_power k)) * |.((Sum (F1 /^ (k + 1))) / [**(c to_power (k + 1)),0**]).| >= |.((Subst (p,<%z0,(1_ F_Complex)%>)) . 0).| by A39, XCMPLX_1:89;
then  (c to_power ((k + 1) - k)) * |.((Sum (F1 /^ (k + 1))) / [**(c to_power (k + 1)),0**]).| >= |.((Subst (p,<%z0,(1_ F_Complex)%>)) . 0).| by A15, POWER:29;
then A56: c * |.((Sum (F1 /^ (k + 1))) / [**(c to_power (k + 1)),0**]).| >= |.((Subst (p,<%z0,(1_ F_Complex)%>)) . 0).| by POWER:25;
(Sum (F1 /^ (k + 1))) / [**(c to_power (k + 1)),0**] = (Sum (F1 /^ (k + 1))) * ([**(c to_power (k + 1)),0**] ") by VECTSP_1:def_11
.= Sum ((F1 /^ (k + 1)) * ([**(c to_power (k + 1)),0**] ")) by POLYNOM1:13 ;
then  |.((Sum (F1 /^ (k + 1))) / [**(c to_power (k + 1)),0**]).| <= Sum |.((F1 /^ (k + 1)) * ([**(c to_power (k + 1)),0**] ")).| by Th14;
then  |.((Sum (F1 /^ (k + 1))) / [**(c to_power (k + 1)),0**]).| <= Sum |.F2.| by A55, XXREAL_0:2;
then  c * |.((Sum (F1 /^ (k + 1))) / [**(c to_power (k + 1)),0**]).| <= c * (Sum |.F2.|) by A15, XREAL_1:64;
hence  c * (Sum |.F2.|) >= |.((Subst (p,<%z0,(1_ F_Complex)%>)) . 0).| by A56, XXREAL_0:2; ::_thesis: verum
end;
then  |.((Subst (p,<%z0,(1_ F_Complex)%>)) . 0).| <= 0 by Lm1;
then A57: (Subst (p,<%z0,(1_ F_Complex)%>)) . 0 = 0. F_Complex by COMPLFLD:59;
 ex x being Element of F_Complex st x is_a_root_of p
proof
take  z0 ; ::_thesis: z0 is_a_root_of p
 eval (p,z0) = 0. F_Complex by A13, A57, Th31;
hence  z0 is_a_root_of p by Def6; ::_thesis: verum
end;
hence  p is with_roots by Def7; ::_thesis: verum
end;
supposeA58: len p = 2 ; ::_thesis: p is with_roots
set np = NormPolynomial p;
A59: (len p) -' 1 = 2 - 1 by A58, XREAL_0:def_2;
A60: len (NormPolynomial p) = len p by A58, Th57;
A61: now__::_thesis:_for_k_being_Nat_st_k_<_len_(NormPolynomial_p)_holds_
(NormPolynomial_p)_._k_=_<%((NormPolynomial_p)_._0),(1__F_Complex)%>_._k
let k be Nat; ::_thesis: ( k < len (NormPolynomial p) implies (NormPolynomial p) . b1 = <%((NormPolynomial p) . 0),(1_ F_Complex)%> . b1 )
assume A62: k < len (NormPolynomial p) ; ::_thesis: (NormPolynomial p) . b1 = <%((NormPolynomial p) . 0),(1_ F_Complex)%> . b1
percases ( k = 0 or k = 1 ) by A58, A60, A62, NAT_1:23;
suppose k = 0 ; ::_thesis: (NormPolynomial p) . b1 = <%((NormPolynomial p) . 0),(1_ F_Complex)%> . b1
hence  (NormPolynomial p) . k = <%((NormPolynomial p) . 0),(1_ F_Complex)%> . k by Th38; ::_thesis: verum
end;
supposeA63: k = 1 ; ::_thesis: (NormPolynomial p) . b1 = <%((NormPolynomial p) . 0),(1_ F_Complex)%> . b1
hence (NormPolynomial p) . k = 1_ F_Complex by A58, A59, Th56
.= <%((NormPolynomial p) . 0),(1_ F_Complex)%> . k by A63, Th38 ;
::_thesis: verum
end;
end;
end;
 len <%((NormPolynomial p) . 0),(1_ F_Complex)%> = 2 by Th40;
then A64: NormPolynomial p = <%((NormPolynomial p) . 0),(1_ F_Complex)%> by A58, A61, Th57, ALGSEQ_1:12;
 ex x being Element of F_Complex st x is_a_root_of NormPolynomial p
proof
take z0 = - ((NormPolynomial p) . 0); ::_thesis: z0 is_a_root_of NormPolynomial p
eval ((NormPolynomial p),z0) = ((NormPolynomial p) . 0) + z0 by A64, Th47
.= 0. F_Complex by RLVECT_1:5 ;
hence  z0 is_a_root_of NormPolynomial p by Def6; ::_thesis: verum
end;
then  NormPolynomial p is with_roots by Def7;
hence  p is with_roots by A58, Th60; ::_thesis: verum
end;
end;
end;

registration
cluster F_Complex  ->  algebraic-closed ;
coherence
 F_Complex is algebraic-closed by Def8, Th74;
end;

registration
cluster non empty non degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right_unital well-unital distributive left_unital algebraic-closed for doubleLoopStr ;
existence
 ex b1 being non empty well-unital doubleLoopStr st
( b1 is algebraic-closed & b1 is add-associative & b1 is right_zeroed & b1 is right_complementable & b1 is Abelian & b1 is commutative & b1 is associative & b1 is distributive & b1 is almost_left_invertible & not b1 is degenerated )
proof
take  F_Complex ; ::_thesis: ( F_Complex is algebraic-closed & F_Complex is add-associative & F_Complex is right_zeroed & F_Complex is right_complementable & F_Complex is Abelian & F_Complex is commutative & F_Complex is associative & F_Complex is distributive & F_Complex is almost_left_invertible & not F_Complex is degenerated )
thus  ( F_Complex is algebraic-closed & F_Complex is add-associative & F_Complex is right_zeroed & F_Complex is right_complementable & F_Complex is Abelian & F_Complex is commutative & F_Complex is associative & F_Complex is distributive & F_Complex is almost_left_invertible & not F_Complex is degenerated ) ; ::_thesis: verum
end;
end;