polynom5.miz



    begin

    theorem :: POLYNOM5:1

    

     Th1: for n,m be Nat st n <> 0 & m <> 0 holds ((((n * m) - n) - m) + 1) >= 0

    proof

      let n,m be Nat;

      assume that

       A1: n <> 0 and

       A2: m <> 0 ;

      m >= ( 0 + 1) by A2, NAT_1: 13;

      then

       A3: (m - 1) >= (( 0 + 1) - 1);

      n >= ( 0 + 1) by A1, NAT_1: 13;

      then (n - 1) >= (( 0 + 1) - 1);

      then ((n - 1) * (m - 1)) >= 0 by A3;

      hence thesis;

    end;

    theorem :: POLYNOM5:2

    

     Th2: for x,y be Real st y > 0 holds (( min (x,y)) / ( max (x,y))) <= 1

    proof

      let x,y be Real;

      assume

       A1: y > 0 ;

      per cases ;

        suppose

         A2: x > 0 ;

        now

          per cases ;

            suppose

             A3: x >= y;

            then ( max (x,y)) = x & ( min (x,y)) = y by XXREAL_0:def 9, XXREAL_0:def 10;

            hence thesis by A1, A3, XREAL_1: 183;

          end;

            suppose

             A4: x < y;

            then ( max (x,y)) = y & ( min (x,y)) = x by XXREAL_0:def 9, XXREAL_0:def 10;

            hence thesis by A2, A4, XREAL_1: 183;

          end;

        end;

        hence thesis;

      end;

        suppose

         A5: x <= 0 ;

        then ( min (x,y)) = x & ( max (x,y)) = y by A1, XXREAL_0:def 9, XXREAL_0:def 10;

        hence thesis by A1, A5;

      end;

    end;

    theorem :: POLYNOM5:3

    

     Th3: for x,y be Real st for c be Real st c > 0 & c < 1 holds (c * x) >= y holds y <= 0

    proof

      let x,y be Real;

      assume

       A1: for c be Real st c > 0 & c < 1 holds (c * x) >= y;

      set ma = ( max (x,y));

      set mi = ( min (x,y));

      set c = (mi / (2 * ma));

      assume

       A2: y > 0 ;

      then

       A3: (y * 2) > y by XREAL_1: 155;

      per cases ;

        suppose

         A4: x > 0 ;

        then

         A5: mi > 0 & ma > 0 by A2, XXREAL_0: 15, XXREAL_0: 16;

        then ((mi / ma) * 2) > (mi / ma) by XREAL_1: 155;

        then (mi / ma) > ((mi / ma) / 2) by XREAL_1: 83;

        then

         A6: (mi / ma) > (mi / (ma * 2)) by XCMPLX_1: 78;

        (mi / ma) <= 1 by A4, Th2;

        then c < 1 by A6, XXREAL_0: 2;

        then

         A7: (c * x) >= y by A1, A5;

        now

          per cases ;

            suppose x >= y;

            then ma = x & mi = y by XXREAL_0:def 9, XXREAL_0:def 10;

            then (c * x) = (y / 2) by A4, XCMPLX_1: 92;

            hence contradiction by A3, A7, XREAL_1: 83;

          end;

            suppose

             A8: x < y;

            then ma = y & mi = x by XXREAL_0:def 9, XXREAL_0:def 10;

            then (c * x) < ((x / (2 * y)) * y) by A4, A8, XREAL_1: 98;

            then

             A9: (c * 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 (c * x) < (y / 2) by A9, XXREAL_0: 2;

            hence contradiction by A7, A10, XXREAL_0: 2;

          end;

        end;

        hence contradiction;

      end;

        suppose x <= 0 ;

        then ((1 / 2) * x) <= 0 ;

        hence contradiction by A1, A2;

      end;

    end;

    

     Lm1: for x,y be Real st for c be Real st c > 0 & c < 1 holds (c * x) >= y holds y <= 0 by Th3;

    theorem :: POLYNOM5:4

    

     Th4: for p be FinSequence of REAL st for n be Element of NAT st n in ( dom p) holds (p . n) >= 0 holds for i be Element of NAT st i in ( dom p) holds ( Sum p) >= (p . i)

    proof

      defpred Q[ FinSequence of REAL ] means (for n be Element of NAT st n in ( dom $1) holds ($1 . n) >= 0 ) implies for i be Element of NAT st i in ( dom $1) holds ( Sum $1) >= ($1 . i);

      

       A1: for p be FinSequence of REAL holds for x be Element of REAL st Q[p] holds Q[(p ^ <*x*>)]

      proof

        let p be FinSequence of REAL ;

        let x be Element of REAL ;

        assume

         A2: (for n be Element of NAT st n in ( dom p) holds (p . n) >= 0 ) implies for i be Element of NAT st i in ( dom p) holds ( Sum p) >= (p . i);

        defpred P[ Nat] means ( Sum (p | $1)) >= 0 ;

        assume

         A3: for n be Element of NAT st n in ( dom (p ^ <*x*>)) holds ((p ^ <*x*>) . n) >= 0 ;

        

         A4: ( dom p) c= ( dom (p ^ <*x*>)) by FINSEQ_1: 26;

         A5:

        now

          let n be Element of NAT ;

          assume

           A6: n in ( dom p);

          then ((p ^ <*x*>) . n) >= 0 by A3, A4;

          hence (p . n) >= 0 by A6, FINSEQ_1:def 7;

        end;

        

         A7: for j be Nat st P[j] holds P[(j + 1)]

        proof

          let j be Nat;

          assume

           A8: ( Sum (p | j)) >= 0 ;

          per cases ;

            suppose

             A9: (j + 1) <= ( len p);

            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 thesis by A8, A10;

          end;

            suppose

             A12: (j + 1) > ( len p);

            then j >= ( len p) by NAT_1: 13;

            then (p | j) = p by FINSEQ_1: 58;

            hence thesis by A8, A12, FINSEQ_1: 58;

          end;

        end;

        let i be Element of NAT ;

        (( 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: P[ 0 ] by RVSUM_1: 72;

        for j be Nat holds P[j] from NAT_1:sch 2( A16, A7);

        then

         A17: ( Sum p) >= 0 by A14;

        assume

         A18: i in ( dom (p ^ <*x*>));

        per cases by A18, A15, XBOOLE_0:def 3;

          suppose

           A19: i in ( dom p);

          

           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 thesis by A19, FINSEQ_1:def 7;

        end;

          suppose i in {(( len p) + 1)};

          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 thesis by RVSUM_1: 74;

        end;

      end;

      

       A21: Q[( <*> REAL )];

      thus for p be FinSequence of REAL holds Q[p] from FINSEQ_2:sch 2( A21, A1);

    end;

    theorem :: POLYNOM5:5

    

     Th5: for x,y be Real holds ( - [**x, y**]) = [**( - x), ( - y)**]

    proof

      let x,y be Real;

      

      thus ( - [**x, y**]) = ( - (x + (y * <i> ))) by COMPLFLD: 2

      .= [**( - x), ( - y)**];

    end;

    theorem :: POLYNOM5:6

    

     Th6: for x1,y1,x2,y2 be Real holds ( [**x1, y1**] - [**x2, y2**]) = [**(x1 - x2), (y1 - y2)**]

    proof

      let x1,y1,x2,y2 be Real;

      

      thus ( [**x1, y1**] - [**x2, y2**]) = ( [**x1, y1**] + [**( - x2), ( - y2)**]) by Th5

      .= [**(x1 - x2), (y1 - y2)**];

    end;

    definition

      let R be non empty multMagma;

      let z be Element of R, n be Nat;

      :: POLYNOM5:def1

      func power (z,n) -> Element of R equals (( power R) . (z,n));

      coherence ;

    end

    theorem :: POLYNOM5:7

    

     Th7: for z be Element of F_Complex st z <> ( 0. F_Complex ) holds for n be Nat holds |.( power (z,n)).| = ( |.z.| to_power n)

    proof

      let z be Element of F_Complex ;

      defpred P[ Nat] means |.( power (z,$1)).| = ( |.z.| to_power $1);

      assume z <> ( 0. F_Complex );

      then

       A1: |.z.| <> 0 by COMPLFLD: 58;

      

       A2: |.z.| >= 0 by COMPLEX1: 46;

      

       A3: for n be Nat st P[n] holds P[(n + 1)]

      proof

        let n be Nat;

        assume

         A4: |.( power (z,n)).| = ( |.z.| to_power n);

        

        thus |.( power (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;

      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: P[ 0 ];

      thus for n be Nat holds P[n] from NAT_1:sch 2( A5, A3);

    end;

    definition

      let p be complex-valued FinSequence;

      :: original: |.

      redefine

      :: POLYNOM5:def2

      func |.p.| -> FinSequence of REAL means

      : Def2: ( len it ) = ( len p) & for n be Nat st n in ( dom p) holds (it . n) = |.(p . n).|;

      coherence by RVSUM_1: 145;

      compatibility

      proof

        let f be FinSequence of REAL ;

        hereby

          assume

           A1: f = |.p.|;

          ( dom |.p.|) = ( dom p) by VALUED_1:def 11;

          hence ( len f) = ( len p) by A1, FINSEQ_3: 29;

          let n be Nat such that n in ( dom p);

          thus (f . n) = |.(p . n).| by A1, VALUED_1: 18;

        end;

        assume that

         A1: ( len f) = ( len p) and

         A2: for n be Nat st n in ( dom p) holds (f . n) = |.(p . n).|;

        

         A3: ( dom f) = ( dom p) by A1, FINSEQ_3: 29;

        then for c be object st c in ( dom f) holds (f . c) = |.(p . c).| by A2;

        hence f = |.p.| by A3, VALUED_1:def 11;

      end;

    end

    theorem :: POLYNOM5:8

    

     Th8: |.( <*> the carrier of F_Complex ).| = ( <*> REAL )

    proof

      ( len |.( <*> the carrier of F_Complex ).|) = ( len ( <*> the carrier of F_Complex )) by Def2

      .= 0 ;

      hence thesis;

    end;

    theorem :: POLYNOM5:9

    

     Th9: for x be Complex holds |. <*x*>.| = <* |.x.|*>

    proof

      let x be Complex;

      ( 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 Def2

      .= 1 by FINSEQ_1: 39;

      then

       A3: ( dom |. <*x*>.|) = ( Seg 1) by FINSEQ_1:def 3;

       A5:

      now

        let n be Nat;

        assume n in ( dom |. <*x*>.|);

        then

         A6: n = 1 by A3, FINSEQ_1: 2, TARSKI:def 1;

        

        hence ( |. <*x*>.| . n) = |.( <*x*> . 1).| by A1, Def2

        .= |.x.| by FINSEQ_1: 40

        .= ( <* |.x.|*> . n) by A6, FINSEQ_1: 40;

      end;

      ( len <* |.x.|*>) = 1 by FINSEQ_1: 39;

      hence thesis by A2, A5, FINSEQ_2: 9;

    end;

    theorem :: POLYNOM5:10

    for x,y be Complex holds |. <*x, y*>.| = <* |.x.|, |.y.|*>

    proof

      let x,y be Complex;

      

       A1: ( len |. <*x, y*>.|) = ( len <*x, y*>) by Def2

      .= 2 by FINSEQ_1: 44;

      then

       A2: ( dom |. <*x, y*>.|) = ( Seg 2) by FINSEQ_1:def 3;

       A3:

      now

        let n be Nat;

        assume

         A4: n in ( dom |. <*x, y*>.|);

        per cases by A2, A4, FINSEQ_1: 2, TARSKI:def 2;

          suppose

           A5: n = 1;

          then

           A6: 1 in ( dom <*x, y*>) by A2, A4, FINSEQ_1: 89;

          ( |. <*x, y*>.| . 1) = |.( <*x, y*> . 1).| by A6, Def2;

          then ( |. <*x, y*>.| . 1) = |.x.| by FINSEQ_1: 44;

          hence ( |. <*x, y*>.| . n) = ( <* |.x.|, |.y.|*> . n) by A5, FINSEQ_1: 44;

        end;

          suppose

           A7: n = 2;

          then

           A8: 2 in ( dom <*x, y*>) by A2, A4, FINSEQ_1: 89;

          ( |. <*x, y*>.| . 2) = |.( <*x, y*> . 2).| by A8, Def2;

          then ( |. <*x, y*>.| . 2) = |.y.| by FINSEQ_1: 44;

          hence ( |. <*x, y*>.| . n) = ( <* |.x.|, |.y.|*> . n) by A7, FINSEQ_1: 44;

        end;

      end;

      ( len <* |.x.|, |.y.|*>) = 2 by FINSEQ_1: 44;

      hence thesis by A1, A3, FINSEQ_2: 9;

    end;

    theorem :: POLYNOM5:11

    for x,y,z be Complex holds |. <*x, y, z*>.| = <* |.x.|, |.y.|, |.z.|*>

    proof

      let x,y,z be Complex;

      

       A1: ( len |. <*x, y, z*>.|) = ( len <*x, y, z*>) by Def2

      .= 3 by FINSEQ_1: 45;

      then

       A2: ( dom |. <*x, y, z*>.|) = ( Seg 3) by FINSEQ_1:def 3;

       A3:

      now

        let n be Nat;

        assume

         A4: n in ( dom |. <*x, y, z*>.|);

        per cases by A2, A4, ENUMSET1:def 1, FINSEQ_3: 1;

          suppose

           A5: n = 1;

          

           A6: 1 in ( dom <*x, y, z*>) by FINSEQ_1: 81;

          ( |. <*x, y, z*>.| . 1) = |.( <*x, y, z*> . 1).| by A6, Def2;

          then ( |. <*x, y, z*>.| . 1) = |.x.| by FINSEQ_1: 45;

          hence ( |. <*x, y, z*>.| . n) = ( <* |.x.|, |.y.|, |.z.|*> . n) by A5, FINSEQ_1: 45;

        end;

          suppose

           A7: n = 2;

          

           A8: 2 in ( dom <*x, y, z*>) by FINSEQ_1: 81;

          ( |. <*x, y, z*>.| . 2) = |.( <*x, y, z*> . 2).| by A8, Def2;

          then ( |. <*x, y, z*>.| . 2) = |.y.| by FINSEQ_1: 45;

          hence ( |. <*x, y, z*>.| . n) = ( <* |.x.|, |.y.|, |.z.|*> . n) by A7, FINSEQ_1: 45;

        end;

          suppose

           A9: n = 3;

          

           A10: 3 in ( dom <*x, y, z*>) by FINSEQ_1: 81;

          ( |. <*x, y, z*>.| . 3) = |.( <*x, y, z*> . 3).| by A10, Def2;

          then ( |. <*x, y, z*>.| . 3) = |.z.| by FINSEQ_1: 45;

          hence ( |. <*x, y, z*>.| . n) = ( <* |.x.|, |.y.|, |.z.|*> . n) by A9, FINSEQ_1: 45;

        end;

      end;

      ( len <* |.x.|, |.y.|, |.z.|*>) = 3 by FINSEQ_1: 45;

      hence thesis by A1, A3, FINSEQ_2: 9;

    end;

    theorem :: POLYNOM5:12

    

     Th12: for p,q be complex-valued FinSequence holds |.(p ^ q).| = ( |.p.| ^ |.q.|)

    proof

      let p,q be complex-valued FinSequence;

      

       A1: ( dom |.(p ^ q).|) = ( Seg ( len |.(p ^ q).|)) by FINSEQ_1:def 3;

       A2:

      now

        let n be Nat;

        

         A3: ( len |.p.|) = ( len p) by Def2;

        assume

         A4: n in ( dom |.(p ^ q).|);

        then

         A5: n >= 1 by A1, FINSEQ_1: 1;

        

         A6: ( len |.(p ^ q).|) = ( len (p ^ q)) by Def2;

        then

         A7: n in ( dom (p ^ q)) by A1, A4, FINSEQ_1:def 3;

        per cases ;

          suppose

           A8: n in ( dom p);

          

           A9: ((p ^ q) . n) = (p . n) by A8, FINSEQ_1:def 7;

          

           A10: n in ( dom |.p.|) by A3, A8, FINSEQ_3: 29;

          

          thus ( |.(p ^ q).| . n) = |.((p ^ q) . n).| by A7, Def2

          .= ( |.p.| . n) by A8, A9, Def2

          .= (( |.p.| ^ |.q.|) . n) by A10, FINSEQ_1:def 7;

        end;

          suppose not n in ( dom p);

          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 Def2;

          then

           A17: (n -' ( len p)) in ( dom |.q.|) by A15, FINSEQ_1:def 3;

          

           A18: ((p ^ q) . n) = (q . (n -' ( len p))) by A13, A16, FINSEQ_1:def 7;

          

          thus ( |.(p ^ q).| . n) = |.((p ^ q) . n).| by A7, Def2

          .= ( |.q.| . (n -' ( len p))) by A16, A18, Def2

          .= (( |.p.| ^ |.q.|) . n) by A3, A13, A17, FINSEQ_1:def 7;

        end;

      end;

      ( len |.(p ^ q).|) = ( len (p ^ q)) by Def2

      .= (( len p) + ( len q)) by FINSEQ_1: 22

      .= (( len p) + ( len |.q.|)) by Def2

      .= (( len |.p.|) + ( len |.q.|)) by Def2

      .= ( len ( |.p.| ^ |.q.|)) by FINSEQ_1: 22;

      hence thesis by A2, FINSEQ_2: 9;

    end;

    theorem :: POLYNOM5:13

    for p be complex-valued FinSequence holds for x be Complex holds |.(p ^ <*x*>).| = ( |.p.| ^ <* |.x.|*>) & |.( <*x*> ^ p).| = ( <* |.x.|*> ^ |.p.|)

    proof

      let p be complex-valued FinSequence;

      let x be Complex;

      

      thus |.(p ^ <*x*>).| = ( |.p.| ^ |. <*x*>.|) by Th12

      .= ( |.p.| ^ <* |.x.|*>) by Th9;

      

      thus |.( <*x*> ^ p).| = ( |. <*x*>.| ^ |.p.|) by Th12

      .= ( <* |.x.|*> ^ |.p.|) by Th9;

    end;

    theorem :: POLYNOM5:14

    

     Th14: for p be FinSequence of the carrier of F_Complex holds |.( Sum p).| <= ( Sum |.p.|)

    proof

      set D = the carrier of F_Complex ;

      defpred P[ FinSequence of D] means |.( Sum $1).| <= ( Sum |.$1.|);

       A1:

      now

        let p be FinSequence of D;

        let x be Element of D;

        assume P[p];

        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;

        reconsider xx = |.x.| as Element of REAL by XREAL_0:def 1;

        (( Sum |.p.|) + |.x.|) = (( Sum |.p.|) + ( Sum <*xx*>)) by FINSOP_1: 11

        .= (( Sum |.p.|) + ( Sum |. <*x*>.|)) by Th9

        .= ( Sum ( |.p.| ^ |. <*x*>.|)) by RVSUM_1: 75

        .= ( Sum |.(p ^ <*x*>).|) by Th12;

        hence P[(p ^ <*x*>)] by A2, A3, XXREAL_0: 2;

      end;

      

       A4: P[( <*> D)] by Th8, COMPLFLD: 57, RLVECT_1: 43, RVSUM_1: 72;

      thus for p be FinSequence of D holds P[p] from FINSEQ_2:sch 2( A4, A1);

    end;

    begin

    definition

      let L be Abelian add-associative right_zeroed right_complementable right_unital commutative distributive non empty doubleLoopStr;

      let p be Polynomial of L;

      let n be Nat;

      :: POLYNOM5:def3

      func p `^ n -> sequence of L equals (( power ( Polynom-Ring L)) . (p,n));

      coherence

      proof

        reconsider n as Element of NAT by ORDINAL1:def 12;

        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 thesis by POLYNOM3:def 10;

      end;

    end

    registration

      let L be Abelian add-associative right_zeroed right_complementable right_unital commutative distributive non empty doubleLoopStr;

      let p be Polynomial of L;

      let n be Nat;

      cluster (p `^ n) -> finite-Support;

      coherence

      proof

        reconsider n as Element of NAT by ORDINAL1:def 12;

        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 thesis;

      end;

    end

    theorem :: POLYNOM5:15

    

     Th15: for L be Abelian add-associative right_zeroed right_complementable well-unital commutative distributive non empty doubleLoopStr holds for p be Polynomial of L holds (p `^ 0 ) = ( 1_. L)

    proof

      let L be Abelian add-associative right_zeroed right_complementable well-unital commutative distributive non empty doubleLoopStr;

      let p be Polynomial of 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: 37;

    end;

    theorem :: POLYNOM5:16

    for L be Abelian add-associative right_zeroed right_complementable well-unital commutative distributive non empty doubleLoopStr holds for p be Polynomial of L holds (p `^ 1) = p

    proof

      let L be Abelian add-associative right_zeroed right_complementable well-unital commutative distributive non empty doubleLoopStr;

      let p be Polynomial of L;

      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;

    end;

    theorem :: POLYNOM5:17

    for L be Abelian add-associative right_zeroed right_complementable well-unital commutative distributive non empty doubleLoopStr holds for p be Polynomial of L holds (p `^ 2) = (p *' p)

    proof

      let L be Abelian add-associative right_zeroed right_complementable well-unital commutative distributive non empty doubleLoopStr;

      let p be Polynomial of L;

      reconsider p1 = p as Element of ( Polynom-Ring L) by POLYNOM3:def 10;

      

      thus (p `^ 2) = (( power ( Polynom-Ring L)) . (p1,(1 + 1)))

      .= (( power (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)

      .= (p *' p) by POLYNOM3:def 10;

    end;

    theorem :: POLYNOM5:18

    for L be Abelian add-associative right_zeroed right_complementable well-unital commutative distributive non empty doubleLoopStr holds for p be Polynomial of L holds (p `^ 3) = ((p *' p) *' p)

    proof

      let L be Abelian add-associative right_zeroed right_complementable well-unital commutative distributive non empty doubleLoopStr;

      let p be Polynomial of L;

      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 (p1,(1 + 1))) * p1) by GROUP_1:def 7

      .= ((( power (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)

      .= (pp *' p) by POLYNOM3:def 10

      .= ((p *' p) *' p) by POLYNOM3:def 10;

    end;

    theorem :: POLYNOM5:19

    

     Th19: for L be Abelian add-associative right_zeroed right_complementable well-unital commutative distributive non empty doubleLoopStr holds for p be Polynomial of L holds for n be Nat holds (p `^ (n + 1)) = ((p `^ n) *' p)

    proof

      let L be Abelian add-associative right_zeroed right_complementable well-unital commutative distributive non empty doubleLoopStr;

      let p be Polynomial of L;

      let n be Nat;

      reconsider nn = n as Element of NAT by ORDINAL1:def 12;

      reconsider p1 = p as Element of ( Polynom-Ring L) by POLYNOM3:def 10;

      

      thus (p `^ (n + 1)) = ((( power ( Polynom-Ring L)) . (p1,nn)) * p1) by GROUP_1:def 7

      .= ((p `^ n) *' p) by POLYNOM3:def 10;

    end;

    theorem :: POLYNOM5:20

    

     Th20: for L be Abelian add-associative right_zeroed right_complementable well-unital commutative distributive non empty doubleLoopStr holds for n be Element of NAT holds (( 0_. L) `^ (n + 1)) = ( 0_. L)

    proof

      let L be Abelian add-associative right_zeroed right_complementable well-unital commutative distributive non empty doubleLoopStr;

      let n be Element of NAT ;

      

      thus (( 0_. L) `^ (n + 1)) = ((( 0_. L) `^ n) *' ( 0_. L)) by Th19

      .= ( 0_. L) by POLYNOM3: 34;

    end;

    theorem :: POLYNOM5:21

    for L be Abelian add-associative right_zeroed right_complementable well-unital commutative distributive non empty doubleLoopStr holds for n be Nat holds (( 1_. L) `^ n) = ( 1_. L)

    proof

      let L be Abelian add-associative right_zeroed right_complementable well-unital commutative distributive non empty doubleLoopStr;

      defpred P[ Nat] means (( 1_. L) `^ $1) = ( 1_. L);

       A1:

      now

        let n be Nat;

        assume P[n];

        

        then (( 1_. L) `^ (n + 1)) = (( 1_. L) *' ( 1_. L)) by Th19

        .= ( 1_. L) by POLYNOM3: 35;

        hence P[(n + 1)];

      end;

      

       A2: P[ 0 ] by Th15;

      thus for n be Nat holds P[n] from NAT_1:sch 2( A2, A1);

    end;

    theorem :: POLYNOM5:22

    

     Th22: for L be Field holds for p be Polynomial of L holds for x be Element of L holds for n be Nat holds ( eval ((p `^ n),x)) = (( power L) . (( eval (p,x)),n))

    proof

      let L be Field;

      let p be Polynomial of L;

      let x be Element of L;

      defpred P[ Nat] means ( eval ((p `^ $1),x)) = (( power L) . (( eval (p,x)),$1));

       A1:

      now

        let n be Nat;

        assume

         A2: P[n];

        ( 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 P[(n + 1)];

      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: P[ 0 ];

      thus for n be Nat holds P[n] from NAT_1:sch 2( A3, A1);

    end;

    

     Lm2: for L be non empty ZeroStr, p be AlgSequence of L st ( len p) > 0 holds (p . (( len p) -' 1)) <> ( 0. L)

    proof

      let L be non empty ZeroStr, p be AlgSequence of L;

      assume ( len p) > 0 ;

      then ex k be Nat st ( len p) = (k + 1) by NAT_1: 6;

      then ( len p) = ((( len p) -' 1) + 1) by NAT_D: 34;

      hence thesis by ALGSEQ_1: 10;

    end;

    theorem :: POLYNOM5:23

    

     Th23: for L be domRing holds for p be Polynomial of L st ( len p) <> 0 holds for n be Nat holds ( len (p `^ n)) = (((n * ( len p)) - n) + 1)

    proof

      let L be domRing;

      let p be Polynomial of L;

      defpred P[ Nat] means ( len (p `^ $1)) = ((($1 * ( len p)) - $1) + 1);

      assume

       A1: ( len p) <> 0 ;

       A2:

      now

        ( len p) >= ( 0 + 1) by A1, NAT_1: 13;

        then (( len p) - 1) >= (( 0 + 1) - 1);

        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 Nat;

        assume

         A5: P[n];

        ((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 P[(n + 1)];

      end;

      ( len (p `^ 0 )) = ( len ( 1_. L)) by Th15

      .= ((( 0 * ( len p)) - 0 ) + 1) by POLYNOM4: 4;

      then

       A7: P[ 0 ];

      thus for n be Nat holds P[n] from NAT_1:sch 2( A7, A2);

    end;

    definition

      let L be non empty multMagma;

      let p be sequence of L;

      let v be Element of L;

      :: POLYNOM5:def4

      func v * p -> sequence of L means

      : Def4: for n be Element of NAT holds (it . n) = (v * (p . n));

      existence

      proof

        deffunc F( Element of NAT ) = (v * (p . $1));

        consider r be sequence of L such that

         A1: for n be Element of NAT holds (r . n) = F(n) from FUNCT_2:sch 4;

        take r;

        thus thesis by A1;

      end;

      uniqueness

      proof

        let p1,p2 be sequence of L such that

         A2: for n be Element of NAT holds (p1 . n) = (v * (p . n)) and

         A3: for n be Element of NAT holds (p2 . n) = (v * (p . n));

        now

          let k be Element of NAT ;

          

          thus (p1 . k) = (v * (p . k)) by A2

          .= (p2 . k) by A3;

        end;

        hence p1 = p2 by FUNCT_2: 63;

      end;

    end

    registration

      let L be add-associative right_zeroed right_complementable right-distributive non empty doubleLoopStr;

      let p be Polynomial of L;

      let v be Element of L;

      cluster (v * p) -> finite-Support;

      coherence

      proof

        take s = ( len p);

        let i be Nat;

        assume

         A1: i >= s;

        reconsider ii = i as Element of NAT by ORDINAL1:def 12;

        

        thus ((v * p) . i) = (v * (p . ii)) by Def4

        .= (v * ( 0. L)) by A1, ALGSEQ_1: 8

        .= ( 0. L);

      end;

    end

    theorem :: POLYNOM5:24

    

     Th24: for L be add-associative right_zeroed right_complementable distributive non empty doubleLoopStr holds for p be Polynomial of L holds ( len (( 0. L) * p)) = 0

    proof

      let L be add-associative right_zeroed right_complementable distributive non empty doubleLoopStr;

      let p be Polynomial of L;

       0 is_at_least_length_of (( 0. L) * p)

      proof

        let i be Nat;

        assume i >= 0 ;

        reconsider ii = i as Element of NAT by ORDINAL1:def 12;

        

        thus ((( 0. L) * p) . i) = (( 0. L) * (p . ii)) by Def4

        .= ( 0. L);

      end;

      hence thesis by ALGSEQ_1:def 3;

    end;

    theorem :: POLYNOM5:25

    

     Th25: for L be add-associative right_zeroed right_complementable well-unital commutative associative distributive almost_left_invertible non empty doubleLoopStr holds for p be Polynomial of L holds for v be Element of L st v <> ( 0. L) holds ( len (v * p)) = ( len p)

    proof

      let L be add-associative right_zeroed right_complementable well-unital commutative associative distributive almost_left_invertible non empty doubleLoopStr;

      let p be Polynomial of L;

      let v be Element of L;

      assume

       A1: v <> ( 0. L);

       A2:

      now

        let n be Nat;

        assume

         A3: n is_at_least_length_of (v * p);

        n is_at_least_length_of p

        proof

          let i be Nat;

          reconsider i1 = i as Element of NAT by ORDINAL1:def 12;

          assume i >= n;

          then ((v * p) . i) = ( 0. L) by A3;

          then (v * (p . i1)) = ( 0. L) by Def4;

          hence thesis by A1, VECTSP_1: 12;

        end;

        hence ( len p) <= n by ALGSEQ_1:def 3;

      end;

      ( len p) is_at_least_length_of (v * p)

      proof

        let i be Nat;

        assume

         A4: i >= ( len p);

        reconsider ii = i as Element of NAT by ORDINAL1:def 12;

        

        thus ((v * p) . i) = (v * (p . ii)) by Def4

        .= (v * ( 0. L)) by A4, ALGSEQ_1: 8

        .= ( 0. L);

      end;

      hence thesis by A2, ALGSEQ_1:def 3;

    end;

    theorem :: POLYNOM5:26

    

     Th26: for L be add-associative right_zeroed right_complementable left-distributive non empty doubleLoopStr holds for p be sequence of L holds (( 0. L) * p) = ( 0_. L)

    proof

      let L be add-associative right_zeroed right_complementable left-distributive non empty doubleLoopStr;

      let p be sequence of L;

      for n be Element of NAT holds (( 0_. L) . n) = (( 0. L) * (p . n)) by FUNCOP_1: 7;

      hence thesis by Def4;

    end;

    theorem :: POLYNOM5:27

    

     Th27: for L be well-unital non empty multLoopStr holds for p be sequence of L holds (( 1. L) * p) = p

    proof

      let L be well-unital non empty multLoopStr;

      let p be sequence of L;

      for n be Element of NAT holds (p . n) = (( 1. L) * (p . n));

      hence thesis by Def4;

    end;

    theorem :: POLYNOM5:28

    

     Th28: for L be add-associative right_zeroed right_complementable right-distributive non empty doubleLoopStr holds for v be Element of L holds (v * ( 0_. L)) = ( 0_. L)

    proof

      let L be add-associative right_zeroed right_complementable right-distributive non empty doubleLoopStr;

      let v be Element of L;

      now

        let n be Element of NAT ;

        

        thus (( 0_. L) . n) = ( 0. L) by FUNCOP_1: 7

        .= (v * ( 0. L))

        .= (v * (( 0_. L) . n)) by FUNCOP_1: 7;

      end;

      hence thesis by Def4;

    end;

    theorem :: POLYNOM5:29

    

     Th29: for L be add-associative right_zeroed right_complementable well-unital right-distributive non empty doubleLoopStr holds for v be Element of L holds (v * ( 1_. L)) = <%v%>

    proof

      let L be add-associative right_zeroed right_complementable well-unital right-distributive non empty doubleLoopStr;

      let v be Element of L;

      now

        let n be Element of NAT ;

        per cases ;

          suppose

           A1: n = 0 ;

          

          hence ( <%v%> . n) = v by ALGSEQ_1:def 5

          .= (v * ( 1. L))

          .= (v * (( 1_. L) . n)) by A1, POLYNOM3: 30;

        end;

          suppose

           A2: n <> 0 ;

          

           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))

          .= (v * (( 1_. L) . n)) by A2, POLYNOM3: 30;

        end;

      end;

      hence thesis by Def4;

    end;

    theorem :: POLYNOM5:30

    

     Th30: for L be add-associative right_zeroed right_complementable well-unital distributive commutative associative almost_left_invertible non empty doubleLoopStr holds for p be Polynomial of L holds for v,x be Element of L holds ( eval ((v * p),x)) = (v * ( eval (p,x)))

    proof

      let L be add-associative right_zeroed right_complementable well-unital distributive commutative associative almost_left_invertible non empty doubleLoopStr;

      let p be Polynomial of L;

      let v,x be Element of L;

      consider F1 be FinSequence of the carrier of L such that

       A1: ( eval (p,x)) = ( Sum F1) and

       A2: ( len F1) = ( len p) and

       A3: for n be 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 be 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 be Element of NAT st n in ( dom F2) holds (F2 . n) = (((v * p) . (n -' 1)) * (( power L) . (x,(n -' 1)))) by POLYNOM4:def 2;

      per cases ;

        suppose v <> ( 0. L);

        then ( len F1) = ( len F2) by A2, A5, Th25;

        then

         A7: ( dom F1) = ( dom F2) by FINSEQ_3: 29;

        now

          let i be object;

          assume

           A8: i in ( dom F1);

          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 Def4

          .= (v * (F1 /. i)) by A9, GROUP_1:def 3;

        end;

        then F2 = (v * F1) by A7, POLYNOM1:def 1;

        hence thesis by A1, A4, POLYNOM1: 12;

      end;

        suppose

         A10: v = ( 0. L);

        

        hence ( eval ((v * p),x)) = ( eval (( 0_. L),x)) by Th26

        .= ( 0. L) by POLYNOM4: 17

        .= (v * ( eval (p,x))) by A10;

      end;

    end;

    theorem :: POLYNOM5:31

    

     Th31: for L be add-associative right_zeroed right_complementable right-distributive unital non empty doubleLoopStr holds for p be Polynomial of L holds ( eval (p,( 0. L))) = (p . 0 )

    proof

      let L be add-associative right_zeroed right_complementable right-distributive unital non empty doubleLoopStr;

      let p be Polynomial of L;

      consider F be 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 be Element of NAT st n in ( dom F) holds (F . n) = ((p . (n -' 1)) * (( power L) . (( 0. L),(n -' 1)))) by POLYNOM4:def 2;

      per cases ;

        suppose ( len F) > 0 ;

        then ( 0 + 1) <= ( len F) by NAT_1: 13;

        then

         A4: 1 in ( dom F) by FINSEQ_3: 25;

        now

          let i be Element of NAT ;

          assume that

           A5: i in ( dom F) and

           A6: i <> 1;

          ( 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);

        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;

      end;

        suppose ( len F) = 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;

      end;

    end;

    definition

      let L be non empty ZeroStr;

      let z0,z1 be Element of L;

      :: POLYNOM5:def5

      func <%z0,z1%> -> sequence of L equals ((( 0_. L) +* ( 0 ,z0)) +* (1,z1));

      coherence ;

    end

    theorem :: POLYNOM5:32

    

     Th32: for L be non empty ZeroStr holds for z0 be Element of L holds ( <%z0%> . 0 ) = z0 & for n be Element of NAT st n >= 1 holds ( <%z0%> . n) = ( 0. L)

    proof

      let L be non empty ZeroStr;

      let z0 be Element of L;

      thus ( <%z0%> . 0 ) = z0 by ALGSEQ_1:def 5;

      let n be Element of NAT ;

      

       A1: ( len <%z0%>) <= 1 by ALGSEQ_1:def 5;

      assume n >= 1;

      hence thesis by A1, ALGSEQ_1: 8, XXREAL_0: 2;

    end;

    theorem :: POLYNOM5:33

    

     Th33: for L be non empty ZeroStr holds for z0 be Element of L st z0 <> ( 0. L) holds ( len <%z0%>) = 1

    proof

      let L be non empty ZeroStr;

      let z0 be Element of L;

      assume z0 <> ( 0. L);

      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;

      then ( len <%z0%>) > 1 by A1, XXREAL_0: 1;

      hence contradiction by ALGSEQ_1:def 5;

    end;

    theorem :: POLYNOM5:34

    

     Th34: for L be non empty ZeroStr holds <%( 0. L)%> = ( 0_. L)

    proof

      let L be non empty ZeroStr;

      ( len <%( 0. L)%>) = 0 by ALGSEQ_1: 14;

      hence thesis by POLYNOM4: 5;

    end;

    theorem :: POLYNOM5:35

    

     Th35: for L be add-associative right_zeroed right_complementable distributive commutative associative well-unital domRing-like non empty doubleLoopStr holds for x,y be Element of L holds ( <%x%> *' <%y%>) = <%(x * y)%>

    proof

      let L be add-associative right_zeroed right_complementable distributive commutative associative well-unital domRing-like non empty doubleLoopStr;

      let x,y be Element of L;

      

       A1: ( len <%x%>) <= 1 by ALGSEQ_1:def 5;

      

       A2: ( len <%y%>) <= 1 by ALGSEQ_1:def 5;

      per cases ;

        suppose

         A3: ( len <%x%>) <> 0 & ( len <%y%>) <> 0 ;

        x <> ( 0. L) & y <> ( 0. L)

        proof

          assume x = ( 0. L) or y = ( 0. L);

          then <%x%> = ( 0_. L) or <%y%> = ( 0_. L) by Th34;

          hence contradiction by A3, POLYNOM4: 3;

        end;

        then (x * y) <> ( 0. L) by VECTSP_2:def 1;

        then

         A4: ( len <%(x * y)%>) = 1 by Th33;

        consider r be FinSequence of the carrier of L such that

         A5: ( len r) = ( 0 + 1) and

         A6: (( <%x%> *' <%y%>) . 0 ) = ( Sum r) and

         A7: for k be 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

          let n be Nat;

          assume n < 1;

          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;

        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 thesis by A9, A4, ALGSEQ_1: 12;

      end;

        suppose

         A13: ( len <%x%>) = 0 ;

        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;

      end;

        suppose

         A15: ( len <%y%>) = 0 ;

        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;

      end;

    end;

    theorem :: POLYNOM5:36

    

     Th36: for L be Abelian add-associative right_zeroed right_complementable well-unital associative commutative distributive almost_left_invertible non empty doubleLoopStr holds for x be Element of L holds for n be Nat holds ( <%x%> `^ n) = <%( power (x,n))%>

    proof

      let L be Abelian add-associative right_zeroed right_complementable well-unital associative commutative distributive almost_left_invertible non empty doubleLoopStr;

      let x be Element of L;

      defpred P[ Nat] means ( <%x%> `^ $1) = <%( power (x,$1))%>;

      

       A1: for n be Nat st P[n] holds P[(n + 1)]

      proof

        let n be Nat;

        assume ( <%x%> `^ n) = <%( power (x,n))%>;

        

        hence ( <%x%> `^ (n + 1)) = ( <%(( power L) . (x,n))%> *' <%x%>) by Th19

        .= <%((( power L) . (x,n)) * x)%> by Th35

        .= <%( power (x,(n + 1)))%> by GROUP_1:def 7;

      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: P[ 0 ];

      thus for n be Nat holds P[n] from NAT_1:sch 2( A2, A1);

    end;

    theorem :: POLYNOM5:37

    for L be add-associative right_zeroed right_complementable unital non empty doubleLoopStr holds for z0,x be Element of L holds ( eval ( <%z0%>,x)) = z0

    proof

      let L be add-associative right_zeroed right_complementable unital non empty doubleLoopStr;

      let z0,x be Element of L;

      consider F be FinSequence of the carrier of L such that

       A1: ( eval ( <%z0%>,x)) = ( Sum F) and

       A2: ( len F) = ( len <%z0%>) and

       A3: for n be 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;

      per cases by A4, NAT_1: 25;

        suppose ( len F) = 0 ;

        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;

      end;

        suppose

         A6: ( len F) = 1;

        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 thesis by A1, RLVECT_1: 44;

      end;

    end;

    theorem :: POLYNOM5:38

    

     Th38: for L be non empty ZeroStr holds for z0,z1 be Element of L holds ( <%z0, z1%> . 0 ) = z0 & ( <%z0, z1%> . 1) = z1 & for n be Nat st n >= 2 holds ( <%z0, z1%> . n) = ( 0. L)

    proof

      let L be non empty ZeroStr;

      let z0,z1 be Element of 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;

      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;

      let n be Nat;

      

       A2: n in NAT by ORDINAL1:def 12;

      assume

       A3: n >= 2;

      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;

    end;

    registration

      let L be non empty ZeroStr;

      let z0,z1 be Element of L;

      cluster <%z0, z1%> -> finite-Support;

      coherence

      proof

        take 2;

        let n be Nat;

        thus thesis by Th38;

      end;

    end

    theorem :: POLYNOM5:39

    

     Th39: for L be non empty ZeroStr holds for z0,z1 be Element of L holds ( len <%z0, z1%>) <= 2

    proof

      let L be non empty ZeroStr;

      let z0,z1 be Element of L;

      2 is_at_least_length_of <%z0, z1%> by Th38;

      hence thesis by ALGSEQ_1:def 3;

    end;

    theorem :: POLYNOM5:40

    

     Th40: for L be non empty ZeroStr holds for z0,z1 be Element of L st z1 <> ( 0. L) holds ( len <%z0, z1%>) = 2

    proof

      let L be non empty ZeroStr;

      let z0,z1 be Element of L;

      assume z1 <> ( 0. L);

      then ( <%z0, z1%> . 1) <> ( 0. L) by Th38;

      then

       A1: for n be Nat st n is_at_least_length_of <%z0, z1%> holds (1 + 1) <= n by NAT_1: 13;

      2 is_at_least_length_of <%z0, z1%> by Th38;

      hence thesis by A1, ALGSEQ_1:def 3;

    end;

    theorem :: POLYNOM5:41

    

     Th41: for L be non empty ZeroStr holds for z0 be Element of L st z0 <> ( 0. L) holds ( len <%z0, ( 0. L)%>) = 1

    proof

      let L be non empty ZeroStr;

      let z0 be Element of L;

      

       A1: 1 is_at_least_length_of <%z0, ( 0. L)%>

      proof

        let n be Nat;

        assume

         A2: n >= 1;

        per cases by A2, XXREAL_0: 1;

          suppose n = 1;

          hence thesis by Th38;

        end;

          suppose n > 1;

          then n >= (1 + 1) by NAT_1: 13;

          hence thesis by Th38;

        end;

      end;

      assume z0 <> ( 0. L);

      then ( <%z0, ( 0. L)%> . 0 ) <> ( 0. L) by Th38;

      then for n be Nat st n is_at_least_length_of <%z0, ( 0. L)%> holds ( 0 + 1) <= n by NAT_1: 13;

      hence thesis by A1, ALGSEQ_1:def 3;

    end;

    theorem :: POLYNOM5:42

    

     Th42: for L be non empty ZeroStr holds <%( 0. L), ( 0. L)%> = ( 0_. L)

    proof

      let L be non empty ZeroStr;

       0 is_at_least_length_of <%( 0. L), ( 0. L)%>

      proof

        let n be Nat;

        assume n >= 0 ;

        per cases ;

          suppose n = 0 ;

          hence thesis by Th38;

        end;

          suppose n > 0 ;

          then

           A1: n >= ( 0 + 1) by NAT_1: 13;

          now

            per cases by A1, XXREAL_0: 1;

              suppose n = 1;

              hence thesis by Th38;

            end;

              suppose n > 1;

              then n >= (1 + 1) by NAT_1: 13;

              hence thesis by Th38;

            end;

          end;

          hence thesis;

        end;

      end;

      then ( len <%( 0. L), ( 0. L)%>) = 0 by ALGSEQ_1:def 3;

      hence thesis by POLYNOM4: 5;

    end;

    theorem :: POLYNOM5:43

    for L be non empty ZeroStr holds for z0 be Element of L holds <%z0, ( 0. L)%> = <%z0%>

    proof

      let L be non empty ZeroStr;

      let z0 be Element of L;

      per cases ;

        suppose

         A1: z0 = ( 0. L);

        

        hence <%z0, ( 0. L)%> = ( 0_. L) by Th42

        .= <%z0%> by A1, Th34;

      end;

        suppose

         A2: z0 <> ( 0. L);

        then

         A3: ( len <%z0%>) = ( 0 + 1) by Th33;

         A4:

        now

          let n be Nat;

          assume n < ( len <%z0%>);

          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;

        end;

        ( len <%z0, ( 0. L)%>) = 1 by A2, Th41;

        hence thesis by A2, A4, Th33, ALGSEQ_1: 12;

      end;

    end;

    theorem :: POLYNOM5:44

    

     Th44: for L be add-associative right_zeroed right_complementable left-distributive unital non empty doubleLoopStr holds for z0,z1,x be Element of L holds ( eval ( <%z0, z1%>,x)) = (z0 + (z1 * x))

    proof

      let L be add-associative right_zeroed right_complementable left-distributive unital non empty doubleLoopStr;

      let z0,z1,x be Element of L;

      consider F be 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 be Element of NAT st n in ( dom F) holds (F . n) = (( <%z0, z1%> . (n -' 1)) * (( power L) . (x,(n -' 1)))) by POLYNOM4:def 2;

      ( len F) <= 2 by A2, Th39;

      then ( len F) = 0 or ... or ( len F) = 2;

      per cases ;

        suppose ( len F) = 0 ;

        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))

        .= (z0 + ((( 0_. L) . 1) * x)) by FUNCOP_1: 7

        .= (z0 + (z1 * x)) by A4, Th38;

      end;

        suppose

         A5: ( len F) = 1;

        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))

        .= (z0 + (( <%z0, z1%> . 1) * x)) by A2, A5, ALGSEQ_1: 8

        .= (z0 + (z1 * x)) by Th38;

      end;

        suppose

         A6: ( len F) = 2;

        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 thesis by A1, RLVECT_1: 45;

      end;

    end;

    theorem :: POLYNOM5:45

    for L be add-associative right_zeroed right_complementable left-distributive well-unital non empty doubleLoopStr holds for z0,z1,x be Element of L holds ( eval ( <%z0, ( 0. L)%>,x)) = z0

    proof

      let L be add-associative right_zeroed right_complementable left-distributive well-unital non empty doubleLoopStr;

      let z0,z1,x be Element of L;

      

      thus ( eval ( <%z0, ( 0. L)%>,x)) = (z0 + (( 0. L) * x)) by Th44

      .= (z0 + ( 0. L))

      .= z0 by RLVECT_1:def 4;

    end;

    theorem :: POLYNOM5:46

    for L be add-associative right_zeroed right_complementable left-distributive unital non empty doubleLoopStr holds for z0,z1,x be Element of L holds ( eval ( <%( 0. L), z1%>,x)) = (z1 * x)

    proof

      let L be add-associative right_zeroed right_complementable left-distributive unital non empty doubleLoopStr;

      let z0,z1,x be Element of L;

      

      thus ( eval ( <%( 0. L), z1%>,x)) = (( 0. L) + (z1 * x)) by Th44

      .= (z1 * x) by RLVECT_1: 4;

    end;

    theorem :: POLYNOM5:47

    

     Th47: for L be add-associative right_zeroed right_complementable left-distributive well-unital non empty doubleLoopStr holds for z0,z1,x be Element of L holds ( eval ( <%z0, ( 1. L)%>,x)) = (z0 + x)

    proof

      let L be add-associative right_zeroed right_complementable left-distributive well-unital non empty doubleLoopStr;

      let z0,z1,x be Element of L;

      

      thus ( eval ( <%z0, ( 1. L)%>,x)) = (z0 + (( 1. L) * x)) by Th44

      .= (z0 + x);

    end;

    theorem :: POLYNOM5:48

    for L be add-associative right_zeroed right_complementable left-distributive well-unital non empty doubleLoopStr holds for z0,z1,x be Element of L holds ( eval ( <%( 0. L), ( 1. L)%>,x)) = x

    proof

      let L be add-associative right_zeroed right_complementable left-distributive well-unital non empty doubleLoopStr;

      let z0,z1,x be Element of L;

      

      thus ( eval ( <%( 0. L), ( 1. L)%>,x)) = (( 0. L) + (( 1. L) * x)) by Th44

      .= (( 0. L) + x)

      .= x by RLVECT_1: 4;

    end;

    begin

    definition

      let L be Abelian add-associative right_zeroed right_complementable well-unital commutative distributive non empty doubleLoopStr;

      let p,q be Polynomial of L;

      :: POLYNOM5:def6

      func Subst (p,q) -> Polynomial of L means

      : Def6: ex F be FinSequence of the carrier of ( Polynom-Ring L) st it = ( Sum F) & ( len F) = ( len p) & for n be Element of NAT st n in ( dom F) holds (F . n) = ((p . (n -' 1)) * (q `^ (n -' 1)));

      existence

      proof

        defpred P[ Nat, set] means $2 = ((p . ($1 -' 1)) * (q `^ ($1 -' 1)));

        set k = ( len p);

         A1:

        now

          let n be Nat;

          assume n in ( Seg k);

          reconsider x = ((p . (n -' 1)) * (q `^ (n -' 1))) as Element of ( Polynom-Ring L) by POLYNOM3:def 10;

          take x;

          thus P[n, x];

        end;

        consider F be FinSequence of the carrier of ( Polynom-Ring L) such that

         A2: ( dom F) = ( Seg k) & for n be Nat st n in ( Seg k) holds P[n, (F . n)] from FINSEQ_1:sch 5( A1);

        reconsider r = ( Sum F) as Polynomial of L by POLYNOM3:def 10;

        take r, F;

        thus thesis by A2, FINSEQ_1:def 3;

      end;

      uniqueness

      proof

        let y1,y2 be Polynomial of L;

        given F1 be FinSequence of the carrier of ( Polynom-Ring L) such that

         A3: y1 = ( Sum F1) and

         A4: ( len F1) = ( len p) and

         A5: for n be Element of NAT st n in ( dom F1) holds (F1 . n) = ((p . (n -' 1)) * (q `^ (n -' 1)));

        given F2 be FinSequence of the carrier of ( Polynom-Ring L) such that

         A6: y2 = ( Sum F2) and

         A7: ( len F2) = ( len p) and

         A8: for n be Element of NAT st n in ( dom F2) holds (F2 . n) = ((p . (n -' 1)) * (q `^ (n -' 1)));

        

         A9: ( dom F1) = ( Seg ( len F1)) by FINSEQ_1:def 3;

        now

          let n be Nat;

          assume

           A10: n in ( dom F1);

          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;

        end;

        hence y1 = y2 by A3, A4, A6, A7, FINSEQ_2: 9;

      end;

    end

    theorem :: POLYNOM5:49

    

     Th49: for L be Abelian add-associative right_zeroed right_complementable well-unital commutative distributive non empty doubleLoopStr holds for p be Polynomial of L holds ( Subst (( 0_. L),p)) = ( 0_. L)

    proof

      let L be Abelian add-associative right_zeroed right_complementable well-unital commutative distributive non empty doubleLoopStr;

      let p be Polynomial of L;

      consider F be 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 be Element of NAT st n in ( dom F) holds (F . n) = ((( 0_. L) . (n -' 1)) * (p `^ (n -' 1))) by Def6;

      now

        let n be Element of NAT ;

        assume n in ( dom F);

        

        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;

      end;

      

      hence ( Subst (( 0_. L),p)) = ( 0. ( Polynom-Ring L)) by A1, POLYNOM3: 1

      .= ( 0_. L) by POLYNOM3:def 10;

    end;

    theorem :: POLYNOM5:50

    for L be Abelian add-associative right_zeroed right_complementable well-unital commutative distributive non empty doubleLoopStr holds for p be Polynomial of L holds ( Subst (p,( 0_. L))) = <%(p . 0 )%>

    proof

      let L be Abelian add-associative right_zeroed right_complementable well-unital commutative distributive non empty doubleLoopStr;

      let p be Polynomial of L;

      consider F be 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 be Element of NAT st n in ( dom F) holds (F . n) = ((p . (n -' 1)) * (( 0_. L) `^ (n -' 1))) by Def6;

      per cases ;

        suppose ( len F) <> 0 ;

        then ( 0 + 1) <= ( len F) by NAT_1: 13;

        then

         A4: 1 in ( dom F) by FINSEQ_3: 25;

        now

          let n be Element of NAT ;

          assume that

           A5: n in ( dom F) and

           A6: n <> 1;

          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;

          

          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;

        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;

      end;

        suppose ( len F) = 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;

      end;

    end;

    theorem :: POLYNOM5:51

    for L be Abelian add-associative right_zeroed right_complementable well-unital associative commutative distributive almost_left_invertible non empty doubleLoopStr holds for p be Polynomial of L holds for x be Element of L holds ( len ( Subst (p, <%x%>))) <= 1

    proof

      let L be Abelian add-associative right_zeroed right_complementable well-unital associative commutative distributive almost_left_invertible non empty doubleLoopStr;

      let p be Polynomial of L;

      let x be Element of L;

      now

        now

          consider F be 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 be Element of NAT st n in ( dom F) holds (F . n) = ((p . (n -' 1)) * ( <%x%> `^ (n -' 1))) by Def6;

          defpred P[ Nat] means for p be Polynomial of L st p = ( Sum (F | $1)) holds ( len p) <= 1;

          

           A3: for n be Nat st P[n] holds P[(n + 1)]

          proof

            let n be Nat;

            reconsider nn = n as Element of NAT by ORDINAL1:def 12;

            reconsider F1 = ( Sum (F | n)) as Polynomial of L by POLYNOM3:def 10;

            reconsider maxFq = ( max (( len F1),( len ((p . nn) * ( <%x%> `^ n))))) as Element of NAT by ORDINAL1:def 12;

            

             A4: ( len ((p . nn) * ( <%x%> `^ n))) <= 1

            proof

              per cases ;

                suppose (p . n) <> ( 0. L);

                

                then ( len ((p . nn) * ( <%x%> `^ n))) = ( len ( <%x%> `^ n)) by Th25

                .= ( len <%( power (x,n))%>) by Th36;

                hence thesis by ALGSEQ_1:def 5;

              end;

                suppose (p . n) = ( 0. L);

                hence thesis by Th24;

              end;

            end;

            assume

             A5: for q be Polynomial of L st q = ( Sum (F | n)) holds ( len q) <= 1;

            then ( len F1) <= 1;

            then

             A6: maxFq <= 1 by A4, XXREAL_0: 28;

            let q be Polynomial of L;

            assume

             A7: q = ( Sum (F | (n + 1)));

            

             A8: maxFq >= ( len F1) & maxFq >= ( len ((p . nn) * ( <%x%> `^ n))) by XXREAL_0: 25;

            now

              per cases ;

                suppose

                 A9: (n + 1) <= ( len F);

                (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 . nn) * ( <%x%> `^ ((n + 1) -' 1))) by NAT_D: 34

                .= ((p . nn) * ( <%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 . nn) * ( <%x%> `^ n))) by A11, POLYNOM3:def 10;

                then ( len q) <= maxFq by A8, POLYNOM4: 6;

                hence thesis by A6, XXREAL_0: 2;

              end;

                suppose

                 A12: (n + 1) > ( len F);

                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 thesis by A5, A7, A13;

              end;

            end;

            hence thesis;

          end;

          

           A14: (F | ( len F)) = F by FINSEQ_1: 58;

          

           A15: P[ 0 ]

          proof

            let p be Polynomial of L;

            

             A16: (F | 0 ) = ( <*> the carrier of ( Polynom-Ring L));

            assume p = ( Sum (F | 0 ));

            

            then p = ( 0. ( Polynom-Ring L)) by A16, RLVECT_1: 43

            .= ( 0_. L) by POLYNOM3:def 10;

            hence thesis by POLYNOM4: 3;

          end;

          for n be Nat holds P[n] from NAT_1:sch 2( A15, A3);

          hence thesis by A1, A14;

        end;

        hence thesis;

      end;

      hence thesis;

    end;

    theorem :: POLYNOM5:52

    

     Th52: for L be Field holds for p,q be 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;

      let p,q be Polynomial of L;

      assume that

       A1: ( len p) <> 0 and

       A2: ( len q) > 1;

      consider F be 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 be Element of NAT st n in ( dom F) holds (F . n) = ((p . (n -' 1)) * (q `^ (n -' 1))) by Def6;

      

       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 ;

      

       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 | lF1);

        reconsider sF1 = ( Sum F1) as Polynomial of L by POLYNOM3:def 10;

        

         A11: ( len F) = (lF1 + 1) by A6, XREAL_1: 235;

        then

         A12: F = (F1 ^ <*(F /. ( len F))*>) by FINSEQ_5: 21;

        then

         A13: ( Sum F) = (( Sum F1) + (F /. ( len F))) by FVSUM_1: 71;

        

         A14: ( len F) = (( len F1) + 1) by A12, FINSEQ_2: 16;

        assume

         A15: ( len ( Subst (p,q))) < ((((( len p) * ( len q)) - ( len p)) - ( len q)) + (1 + 1));

        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

          per cases ;

            suppose

             A17: ( len F1) <> {} ;

            defpred P[ Nat] means for F2 be Polynomial of L st F2 = ( Sum (F1 | $1)) holds ( len F2) <= (((($1 * ( len q)) - ( len q)) - $1) + 2);

            

             A18: (F1 | ( len F1)) = F1 by FINSEQ_1: 58;

            

             A19: for n be non zero Nat st P[n] holds P[(n + 1)]

            proof

              let n be non zero Nat;

              assume

               A20: for F2 be Polynomial of L st F2 = ( Sum (F1 | n)) holds ( len F2) <= ((((n * ( len q)) - ( len q)) - n) + 2);

              ( 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 (F1 | n)) as Polynomial of L by POLYNOM3:def 10;

              let F2 be Polynomial of L;

              assume

               A22: F2 = ( Sum (F1 | (n + 1)));

              ( 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

                per cases ;

                  suppose

                   A24: (n + 1) <= ( len F1);

                  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 ORDINAL1:def 12;

                  

                   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

                    per cases ;

                      suppose (p . n) <> ( 0. L);

                      then ( len ((p . nn) * (q `^ nn))) = ( len (q `^ nn)) by Th25;

                      hence thesis by A2, Th23;

                    end;

                      suppose

                       A27: (p . n) = ( 0. L);

                      ( len q) >= ( 0 + 1) by A2;

                      then (( len q) - 1) >= 0 ;

                      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 thesis by A27, A28, Th24;

                    end;

                  end;

                  then

                   A29: maxFq <= (((n * ( len q)) - n) + 1) by A23, XXREAL_0: 28;

                  ( len F1) <= ( 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 F1) by A24, A25, FINSEQ_3: 25;

                  

                  then

                   A32: (F1 /. (n + 1)) = (F1 . (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;

                  (F1 | (nn + 1)) = ((F1 | nn) ^ <*(F1 /. (nn + 1))*>) by A24, FINSEQ_5: 82;

                  

                  then F2 = (( Sum (F1 | n)) + (F1 /. (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;

                end;

                  suppose

                   A33: (n + 1) > ( len F1);

                  ( - ( 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 F1) by A33, NAT_1: 13;

                  then

                   A35: (F1 | n) = F1 by FINSEQ_1: 58;

                  (F1 | (n + 1)) = F1 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;

                end;

              end;

              hence ( len F2) <= (((((n + 1) * ( len q)) - ( len q)) - (n + 1)) + 2);

            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 F1) by A17, NAT_1: 13;

            then

             A37: 1 in ( dom F1) by FINSEQ_3: 25;

            

             A38: P[1]

            proof

              let F2 be Polynomial of L;

              

               Z: (F1 . 1) = (F1 /. 1) by A37, PARTFUN1:def 6;

              (F1 | 1) = <*(F1 . 1)*> by A17, CARD_1: 27, FINSEQ_5: 20;

              

              then

               A39: ( Sum (F1 | 1)) = (F1 . 1) by Z, RLVECT_1: 44

              .= (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 (F1 | 1));

              hence ( len F2) <= ((((1 * ( len q)) - ( len q)) - 1) + 2) by A39, ALGSEQ_1:def 5;

            end;

            for n be non zero Nat holds P[n] from NAT_1:sch 10( A38, A19);

            then ( len sF1) <= ((((( len F1) * ( len q)) - ( len q)) - ( len F1)) + 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 . lF1) * (q `^ lF1)) by A5, A41;

            then ( Subst (p,q)) = (sF1 + ((p . lF1) * (q `^ lF1))) by A3, A13, POLYNOM3:def 10;

            

            then

             A42: (( Subst (p,q)) . k) = ((sF1 . k) + (((p . lF1) * (q `^ lF1)) . k)) by NORMSP_1:def 2

            .= (((p . lF1) * (q `^ lF1)) . k) by A40, RLVECT_1:def 4

            .= ((p . lF1) * ((q `^ lF1) . k)) by Def4;

            ( len (q `^ lF1)) = (k + 1) by A9;

            then

             A43: ((q `^ lF1) . k) <> ( 0. L) by ALGSEQ_1: 10;

            (p . lF1) <> ( 0. L) by A4, A11, ALGSEQ_1: 10;

            hence contradiction by A16, A42, A43, VECTSP_1: 12;

          end;

            suppose

             A44: ( len F1) = {} ;

            

             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;

            F1 = ( <*> 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;

          end;

        end;

        hence contradiction;

      end;

      defpred P[ Nat] means for F1 be Polynomial of L st F1 = ( Sum (F | $1)) holds ( len F1) <= ( len (q `^ ($1 -' 1)));

      

       A49: for n be non zero Nat st P[n] holds P[(n + 1)]

      proof

        let n be non zero Nat;

        assume

         A50: for F1 be Polynomial of L st F1 = ( Sum (F | n)) holds ( len F1) <= ( len (q `^ (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;

        assume

         A51: F1 = ( Sum (F | (n + 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 ;

        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;

        ( len (q `^ (n -' 1))) = ((((n -' 1) * ( len q)) - (n -' 1)) + 1) by A2, Th23

        .= ((((n - 1) * ( len q)) - (n -' 1)) + 1) by XREAL_0:def 2

        .= ((((n * ( len q)) - (1 * ( len q))) - (n - 1)) + 1) by XREAL_0:def 2

        .= (((((n * ( len q)) - ( len q)) - n) + 1) + 1);

        then

         A54: ( len (q `^ (n -' 1))) <= ( len (q `^ nn)) by A2, A53, Th23;

        per cases ;

          suppose

           A55: (n + 1) <= ( len F);

          reconsider maxFq = ( max (( len F2),( len ((p . nn) * (q `^ nn))))) as Element of NAT by ORDINAL1:def 12;

          (p . n) <> ( 0. L) or (p . n) = ( 0. L);

          then

           A56: ( len ((p . nn) * (q `^ nn))) <= ( len (q `^ nn)) by Th24, Th25;

          ( len F2) <= ( len (q `^ (n -' 1))) by A50;

          then ( len F2) <= ( len (q `^ nn)) by A54, XXREAL_0: 2;

          then

           A57: maxFq <= ( len (q `^ nn)) by A56, XXREAL_0: 28;

          (F | (n + 1)) = ((F | n) ^ <*(F /. (nn + 1))*>) by A55, FINSEQ_5: 82;

          then

           A58: F1 = (( Sum (F | n)) + (F /. (n + 1))) by A51, FVSUM_1: 71;

          (n + 1) >= 1 by NAT_1: 11;

          then

           A59: (n + 1) in ( dom F) by A55, FINSEQ_3: 25;

          

          then (F /. (n + 1)) = (F . (n + 1)) by PARTFUN1:def 6

          .= ((p . ((n + 1) -' 1)) * (q `^ ((n + 1) -' 1))) by A5, A59

          .= ((p . nn) * (q `^ ((n + 1) -' 1))) by NAT_D: 34

          .= ((p . nn) * (q `^ nn)) by NAT_D: 34;

          then

           A60: F1 = (F2 + ((p . nn) * (q `^ nn))) by A58, POLYNOM3:def 10;

          maxFq >= ( len F2) & maxFq >= ( len ((p . nn) * (q `^ nn))) by XXREAL_0: 25;

          then ( len F1) <= maxFq by A60, POLYNOM4: 6;

          then ( len F1) <= ( len (q `^ nn)) by A57, XXREAL_0: 2;

          hence thesis by NAT_D: 34;

        end;

          suppose

           A61: (n + 1) > ( len F);

          then n >= ( len F) by NAT_1: 13;

          then

           A62: (F | n) = F by FINSEQ_1: 58;

          (F | (n + 1)) = F by A61, FINSEQ_1: 58;

          then ( len F1) <= ( len (q `^ (n -' 1))) by A50, A51, A62;

          then ( len F1) <= ( len (q `^ nn)) by A54, XXREAL_0: 2;

          hence thesis by NAT_D: 34;

        end;

      end;

      

       A63: (F | ( len F)) = F by FINSEQ_1: 58;

      

       A64: P[1]

      proof

        let F1 be Polynomial of L;

        

         Z: (F . 1) = (F /. 1) by A7, PARTFUN1:def 6;

        (F | 1) = <*(F . 1)*> by A1, A4, CARD_1: 27, FINSEQ_5: 20;

        

        then

         A65: ( Sum (F | 1)) = (F . 1) by Z, RLVECT_1: 44

        .= ((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));

        then ( len F1) <= 1 by A65, ALGSEQ_1:def 5;

        then ( len F1) <= ( len ( 1_. L)) by POLYNOM4: 4;

        then ( len F1) <= ( len (q `^ 0 )) by Th15;

        hence thesis by XREAL_1: 232;

      end;

      for n be non zero Nat holds P[n] from NAT_1:sch 10( A64, A49);

      then ( len ( Subst (p,q))) <= ( len (q `^ (( len F) -' 1))) by A1, A3, A4, A63;

      hence thesis by A9, A10, XXREAL_0: 1;

    end;

    theorem :: POLYNOM5:53

    

     Th53: for L be Field holds for p,q be Polynomial of L holds for x be Element of L holds ( eval (( Subst (p,q)),x)) = ( eval (p,( eval (q,x))))

    proof

      let L be Field;

      let p,q be Polynomial of L;

      let x be Element of L;

      consider F1 be 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 be 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 be 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 be Element of NAT st n in ( dom F) holds (F . n) = ((p . (n -' 1)) * (q `^ (n -' 1))) by Def6;

      defpred P[ Nat] means for r be Polynomial of L st r = ( Sum (F | $1)) holds ( eval (r,x)) = ( Sum (F1 | $1));

      

       A7: for n be Nat st P[n] holds P[(n + 1)]

      proof

        let n be Nat;

        reconsider nn = n as Element of NAT by ORDINAL1:def 12;

        assume

         A8: for r be Polynomial of L st r = ( Sum (F | n)) holds ( eval (r,x)) = ( Sum (F1 | n));

        let r be Polynomial of L;

        assume

         A9: r = ( Sum (F | (n + 1)));

        per cases ;

          suppose

           A10: (n + 1) <= ( len F);

          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 . nn) * (q `^ ((n + 1) -' 1))) by NAT_D: 34

          .= ((p . nn) * (q `^ n)) by NAT_D: 34;

          then r = (r1 + ((p . nn) * (q `^ n))) by A12, POLYNOM3:def 10;

          

          hence ( eval (r,x)) = (( eval (r1,x)) + ( eval (((p . nn) * (q `^ n)),x))) by POLYNOM4: 19

          .= (( Sum (F1 | n)) + ( eval (((p . nn) * (q `^ n)),x))) by A8

          .= (( Sum (F1 | n)) + ((p . nn) * ( eval ((q `^ n),x)))) by Th30

          .= (( Sum (F1 | n)) + ((p . nn) * (( 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;

        end;

          suppose

           A16: (n + 1) > ( len F);

          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 thesis by A8, A9, A17;

        end;

      end;

      

       A18: (F | ( len F)) = F & (F1 | ( len F1)) = F1 by FINSEQ_1: 58;

      

       A19: P[ 0 ]

      proof

        let r be Polynomial of L;

        

         A20: (F | 0 ) = ( <*> the carrier of ( Polynom-Ring L));

        

         A21: (F1 | 0 ) = ( <*> the carrier of L);

        assume r = ( Sum (F | 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;

      end;

      for n be Nat holds P[n] from NAT_1:sch 2( A19, A7);

      hence thesis by A4, A5, A1, A2, A18;

    end;

    begin

    definition

      let L be unital non empty doubleLoopStr;

      let p be Polynomial of L;

      let x be Element of L;

      :: POLYNOM5:def7

      pred x is_a_root_of p means ( eval (p,x)) = ( 0. L);

    end

    definition

      let L be unital non empty doubleLoopStr;

      let p be Polynomial of L;

      :: POLYNOM5:def8

      attr p is with_roots means ex x be Element of L st x is_a_root_of p;

    end

    theorem :: POLYNOM5:54

    

     Th54: for L be unital non empty doubleLoopStr holds ( 0_. L) is with_roots

    proof

      let L be unital non empty doubleLoopStr;

      set x = the Element of L;

      take x;

      thus ( eval (( 0_. L),x)) = ( 0. L) by POLYNOM4: 17;

    end;

    registration

      let L be unital non empty doubleLoopStr;

      cluster ( 0_. L) -> with_roots;

      coherence by Th54;

    end

    theorem :: POLYNOM5:55

    for L be unital non empty doubleLoopStr holds for x be Element of L holds x is_a_root_of ( 0_. L) by POLYNOM4: 17;

    registration

      let L be unital non empty doubleLoopStr;

      cluster with_roots for Polynomial of L;

      existence

      proof

        take ( 0_. L);

        thus thesis;

      end;

    end

    definition

      let L be unital non empty doubleLoopStr;

      :: POLYNOM5:def9

      attr L is algebraic-closed means for p be Polynomial of L st ( len p) > 1 holds p is with_roots;

    end

    definition

      let L be unital non empty doubleLoopStr;

      let p be Polynomial of L;

      :: POLYNOM5:def10

      func Roots (p) -> Subset of L means

      : Def10: for x be Element of L holds x in it iff x is_a_root_of p;

      existence

      proof

        { x where x be Element of L : x is_a_root_of p } c= the carrier of L

        proof

          let y be object;

          assume y in { x where x be Element of L : x is_a_root_of p };

          then ex x be Element of L st x = y & x is_a_root_of p;

          hence thesis;

        end;

        then

        reconsider X = { x where x be Element of L : x is_a_root_of p } as Subset of L;

        take X;

        let x be Element of L;

        thus x in X implies x is_a_root_of p

        proof

          assume x in X;

          then ex y be Element of L st x = y & y is_a_root_of p;

          hence thesis;

        end;

        assume x is_a_root_of p;

        hence thesis;

      end;

      uniqueness

      proof

        let X1,X2 be Subset of L such that

         A1: for x be Element of L holds x in X1 iff x is_a_root_of p and

         A2: for x be Element of L holds x in X2 iff x is_a_root_of p;

        thus X1 c= X2 by A1, A2;

        let x be object;

        assume

         A3: x in X2;

        then

        reconsider y = x as Element of L;

        y is_a_root_of p by A2, A3;

        hence thesis by A1;

      end;

    end

    definition

      let L be commutative associative well-unital distributive almost_left_invertible non empty doubleLoopStr;

      let p be Polynomial of L;

      :: POLYNOM5:def11

      func NormPolynomial (p) -> sequence of L means

      : Def11: for n be Element of NAT holds (it . n) = ((p . n) / (p . (( len p) -' 1)));

      existence

      proof

        deffunc F( Element of NAT ) = ((p . $1) / (p . (( len p) -' 1)));

        consider q be sequence of L such that

         A1: for n be Element of NAT holds (q . n) = F(n) from FUNCT_2:sch 4;

        take q;

        thus thesis by A1;

      end;

      uniqueness

      proof

        let p1,p2 be sequence of L such that

         A2: for n be Element of NAT holds (p1 . n) = ((p . n) / (p . (( len p) -' 1))) and

         A3: for n be Element of NAT holds (p2 . n) = ((p . n) / (p . (( len p) -' 1)));

        now

          let n be Element of NAT ;

          

          thus (p1 . n) = ((p . n) / (p . (( len p) -' 1))) by A2

          .= (p2 . n) by A3;

        end;

        hence p1 = p2 by FUNCT_2: 63;

      end;

    end

    registration

      let L be add-associative right_zeroed right_complementable commutative associative well-unital distributive almost_left_invertible non empty doubleLoopStr;

      let p be Polynomial of L;

      cluster ( NormPolynomial p) -> finite-Support;

      coherence

      proof

        now

          let n be Nat;

          assume

           A1: n >= ( len p);

          reconsider nn = n as Element of NAT by ORDINAL1:def 12;

          

          thus (( NormPolynomial p) . n) = ((p . nn) / (p . (( len p) -' 1))) by Def11

          .= (( 0. L) / (p . (( len p) -' 1))) by A1, ALGSEQ_1: 8

          .= (( 0. L) * ((p . (( len p) -' 1)) " ))

          .= ( 0. L);

        end;

        hence thesis;

      end;

    end

    theorem :: POLYNOM5:56

    

     Th56: for L be commutative associative well-unital distributive almost_left_invertible non empty doubleLoopStr holds for p be Polynomial of L st ( len p) <> 0 holds (( NormPolynomial p) . (( len p) -' 1)) = ( 1. L)

    proof

      let L be commutative associative well-unital distributive almost_left_invertible non empty doubleLoopStr;

      let p be Polynomial of L;

      assume ( len p) <> 0 ;

      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 Def11

      .= ((p . (( len p) -' 1)) * ((p . (( len p) -' 1)) " ))

      .= ( 1. L) by A1, VECTSP_1:def 10;

    end;

    theorem :: POLYNOM5:57

    

     Th57: for L be Field holds for p be Polynomial of L st ( len p) <> 0 holds ( len ( NormPolynomial p)) = ( len p)

    proof

      let L be Field;

      let p be Polynomial of L;

      assume ( len p) <> 0 ;

      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

        let n be Nat;

        assume

         A3: n is_at_least_length_of ( NormPolynomial p);

        n is_at_least_length_of p

        proof

          let i be Nat;

          reconsider ii = i as Element of NAT by ORDINAL1:def 12;

          assume i >= n;

          then (( NormPolynomial p) . i) = ( 0. L) by A3;

          then ((p . ii) / (p . (( len p) -' 1))) = ( 0. L) by Def11;

          then ((p . ii) * ((p . (( len p) -' 1)) " )) = ( 0. L);

          hence thesis by A1, VECTSP_1: 12;

        end;

        hence ( len p) <= n by ALGSEQ_1:def 3;

      end;

      ( len p) is_at_least_length_of ( NormPolynomial p)

      proof

        let n be Nat;

        assume

         A4: n >= ( len p);

        reconsider nn = n as Element of NAT by ORDINAL1:def 12;

        

        thus (( NormPolynomial p) . n) = ((p . nn) / (p . (( len p) -' 1))) by Def11

        .= (( 0. L) / (p . (( len p) -' 1))) by A4, ALGSEQ_1: 8

        .= (( 0. L) * ((p . (( len p) -' 1)) " ))

        .= ( 0. L);

      end;

      hence thesis by A2, ALGSEQ_1:def 3;

    end;

    theorem :: POLYNOM5:58

    

     Th58: for L be Field holds for p be Polynomial of L st ( len p) <> 0 holds for x be Element of L holds ( eval (( NormPolynomial p),x)) = (( eval (p,x)) / (p . (( len p) -' 1)))

    proof

      let L be Field;

      let p be Polynomial of L;

      assume

       A1: ( len p) <> 0 ;

      set NPp = ( NormPolynomial p);

      let x be Element of L;

      consider F1 be FinSequence of the carrier of L such that

       A2: ( eval (p,x)) = ( Sum F1) and

       A3: ( len F1) = ( len p) and

       A4: for n be 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 be FinSequence of the carrier of L such that

       A5: ( eval (NPp,x)) = ( Sum F2) and

       A6: ( len F2) = ( len NPp) and

       A7: for n be Element of NAT st n in ( dom F2) holds (F2 . n) = ((NPp . (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

        let i be object;

        assume

         A9: i in ( dom F1);

        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

        .= ((NPp . (i1 -' 1)) * (( power L) . (x,(i1 -' 1)))) by A7, A8, A9

        .= (((p . (i1 -' 1)) / (p . (( len p) -' 1))) * (( power L) . (x,(i1 -' 1)))) by Def11

        .= (((p . (i1 -' 1)) * ((p . (( len p) -' 1)) " )) * (( power L) . (x,(i1 -' 1))))

        .= ((F1 /. i) * ((p . (( len p) -' 1)) " )) by A10, GROUP_1:def 3;

      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 thesis;

    end;

    theorem :: POLYNOM5:59

    

     Th59: for L be Field holds for p be Polynomial of L st ( len p) <> 0 holds for x be Element of L holds x is_a_root_of p iff x is_a_root_of ( NormPolynomial p)

    proof

      let L be Field;

      let p be Polynomial of L;

      assume

       A1: ( len p) <> 0 ;

      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;

      thus x is_a_root_of p implies x is_a_root_of ( NormPolynomial p)

      proof

        assume x is_a_root_of p;

        then ( eval (p,x)) = ( 0. L);

        

        then ( eval (( NormPolynomial p),x)) = (( 0. L) / (p . (( len p) -' 1))) by A1, Th58

        .= (( 0. L) * ((p . (( len p) -' 1)) " ))

        .= ( 0. L);

        hence thesis;

      end;

      assume x is_a_root_of ( NormPolynomial p);

      

      then ( 0. L) = ( eval (( NormPolynomial p),x))

      .= (( eval (p,x)) / (p . (( len p) -' 1))) by A1, Th58

      .= (( eval (p,x)) * ((p . (( len p) -' 1)) " ));

      then ( eval (p,x)) = ( 0. L) by A2, VECTSP_1: 12;

      hence thesis;

    end;

    theorem :: POLYNOM5:60

    

     Th60: for L be Field holds for p be Polynomial of L st ( len p) <> 0 holds p is with_roots iff ( NormPolynomial p) is with_roots

    proof

      let L be Field;

      let p be Polynomial of L;

      assume

       A1: ( len p) <> 0 ;

      thus p is with_roots implies ( NormPolynomial p) is with_roots

      proof

        assume p is with_roots;

        then

        consider x be Element of L such that

         A2: x is_a_root_of p;

        x is_a_root_of ( NormPolynomial p) by A1, A2, Th59;

        hence thesis;

      end;

      assume ( NormPolynomial p) is with_roots;

      then

      consider x be Element of L such that

       A3: x is_a_root_of ( NormPolynomial p);

      x is_a_root_of p by A1, A3, Th59;

      hence thesis;

    end;

    theorem :: POLYNOM5:61

    for L be Field holds for p be Polynomial of L st ( len p) <> 0 holds ( Roots p) = ( Roots ( NormPolynomial p))

    proof

      let L be Field;

      let p be Polynomial of L;

      assume

       A1: ( len p) <> 0 ;

      thus ( Roots p) c= ( Roots ( NormPolynomial p))

      proof

        let x be object;

        assume

         A2: x in ( Roots p);

        then

        reconsider x1 = x as Element of L;

        x1 is_a_root_of p by A2, Def10;

        then x1 is_a_root_of ( NormPolynomial p) by A1, Th59;

        hence thesis by Def10;

      end;

      thus ( Roots ( NormPolynomial p)) c= ( Roots p)

      proof

        let x be object;

        assume

         A3: x in ( Roots ( NormPolynomial p));

        then

        reconsider x1 = x as Element of L;

        x1 is_a_root_of ( NormPolynomial p) by A3, Def10;

        then x1 is_a_root_of p by A1, Th59;

        hence thesis by Def10;

      end;

    end;

    theorem :: POLYNOM5:62

    

     Th62: ( id COMPLEX ) is_continuous_on COMPLEX

    proof

       A1:

      now

        let x be Complex;

        let r be Real;

        assume that x in COMPLEX and

         A2: 0 < r;

        take s = r;

        thus 0 < s by A2;

        let y be Complex;

        assume that y in COMPLEX and

         A3: |.(y - x).| < s;

        reconsider xx = x, yy = y as Element of COMPLEX by XCMPLX_0:def 2;

         |.((( id COMPLEX ) /. yy) - (( id COMPLEX ) /. xx)).| < r by A3;

        hence |.((( id COMPLEX ) /. y) - (( id COMPLEX ) /. x)).| < r;

      end;

      ( dom ( id COMPLEX )) = COMPLEX by FUNCT_2:def 1;

      hence thesis by A1, CFCONT_1: 39;

    end;

    theorem :: POLYNOM5:63

    

     Th63: for x be Element of COMPLEX holds ( COMPLEX --> x) is_continuous_on COMPLEX

    proof

      let x be Element of COMPLEX ;

       A1:

      now

        let x1 be Complex;

        let r be Real;

        assume that

         A2: x1 in COMPLEX and

         A3: 0 < r;

        take s = r;

        thus 0 < s by A3;

        let x2 be Complex;

        assume that

         A4: x2 in COMPLEX and |.(x2 - x1).| < s;

        reconsider xx1 = x1, xx2 = x2 as Element of COMPLEX by A2, A4;

        (( COMPLEX --> x) /. xx1) = x & (( COMPLEX --> x) /. xx2) = x by FUNCOP_1: 7;

        hence |.((( COMPLEX --> x) /. x2) - (( COMPLEX --> x) /. x1)).| < r by A3, COMPLEX1: 44;

      end;

      ( dom ( COMPLEX --> x)) = COMPLEX by FUNCOP_1: 13;

      hence thesis by A1, CFCONT_1: 39;

    end;

    definition

      let L be unital non empty multMagma;

      let x be Element of L;

      let n be Nat;

      :: POLYNOM5:def12

      func FPower (x,n) -> Function of L, L means

      : Def12: for y be Element of L holds (it . y) = (x * ( power (y,n)));

      existence

      proof

        deffunc F( Element of L) = (x * ( power ($1,n)));

        consider f be Function of the carrier of L, the carrier of L such that

         A1: for y be Element of L holds (f . y) = F(y) from FUNCT_2:sch 4;

        reconsider f as Function of L, L;

        take f;

        thus thesis by A1;

      end;

      uniqueness

      proof

        let f1,f2 be Function of L, L such that

         A2: for y be Element of L holds (f1 . y) = (x * ( power (y,n))) and

         A3: for y be Element of L holds (f2 . y) = (x * ( power (y,n)));

        now

          let y be Element of L;

          

          thus (f1 . y) = (x * ( power (y,n))) by A2

          .= (f2 . y) by A3;

        end;

        hence f1 = f2 by FUNCT_2: 63;

      end;

    end

    theorem :: POLYNOM5:64

    for L be unital non empty multMagma holds ( FPower (( 1_ L),1)) = ( id the carrier of L)

    proof

      let L be unital non empty multMagma;

       A1:

      now

        let x be object;

        assume x in the carrier of L;

        then

        reconsider x1 = x as Element of L;

        (( FPower (( 1_ L),1)) . x1) = (( 1_ L) * ( power (x1,1))) by Def12

        .= (( power L) . (x1,1)) by GROUP_1:def 4;

        hence (( FPower (( 1_ L),1)) . x) = x by GROUP_1: 50;

      end;

      ( dom ( FPower (( 1_ L),1))) = the carrier of L by FUNCT_2:def 1;

      hence thesis by A1, FUNCT_1: 17;

    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

        let x be Element of F_Complex ;

        reconsider x1 = x as Element of COMPLEX by COMPLFLD:def 1;

        (( id COMPLEX ) /. x1) = x1 & ( dom (( id COMPLEX ) (#) ( id COMPLEX ))) = COMPLEX by 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 (x,2)));

      end;

      hence thesis by Def12;

    end;

    theorem :: POLYNOM5:66

    

     Th66: for L be unital non empty multMagma holds for x be Element of L holds ( FPower (x, 0 )) = (the carrier of L --> x)

    proof

      let L be unital non empty multMagma;

      let x be Element of L;

      reconsider f = (the carrier of L --> x) as Function of L, L;

      now

        let y be Element of L;

        

        thus (f . y) = x by FUNCOP_1: 7

        .= (x * ( 1_ L)) by GROUP_1:def 4

        .= (x * ( power (y, 0 ))) by GROUP_1:def 7;

      end;

      hence thesis by Def12;

    end;

    theorem :: POLYNOM5:67

    for x be Element of F_Complex holds ex x1 be Element of COMPLEX st x = x1 & ( FPower (x,1)) = (x1 (#) ( id COMPLEX ))

    proof

      let x be Element of F_Complex ;

      reconsider x1 = x as Element of COMPLEX by COMPLFLD:def 1;

      take x1;

      thus x = x1;

      the carrier of F_Complex = COMPLEX by COMPLFLD:def 1;

      then

      reconsider f = (x1 (#) ( id COMPLEX )) as Function of F_Complex , F_Complex ;

      now

        let y be Element of F_Complex ;

        reconsider y1 = y as Element of COMPLEX by COMPLFLD:def 1;

        

        thus (f . y) = (x1 * (( id COMPLEX ) . y1)) by VALUED_1: 6

        .= (x * y)

        .= (x * ( power (y,1))) by GROUP_1: 50;

      end;

      hence thesis by Def12;

    end;

    theorem :: POLYNOM5:68

    for x be Element of F_Complex holds ex x1 be Element of COMPLEX st x = x1 & ( FPower (x,2)) = (x1 (#) (( id COMPLEX ) (#) ( id COMPLEX )))

    proof

      let x be Element of F_Complex ;

      reconsider x1 = x as Element of COMPLEX by COMPLFLD:def 1;

      take x1;

      thus x = x1;

      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

        let y be Element of F_Complex ;

        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)))

        .= (x * (y * y))

        .= (x * ( power (y,2))) by GROUP_1: 51;

      end;

      hence thesis by Def12;

    end;

    theorem :: POLYNOM5:69

    

     Th69: for x be Element of F_Complex holds for n be Nat holds ex f be Function of COMPLEX , COMPLEX st f = ( FPower (x,n)) & ( FPower (x,(n + 1))) = (f (#) ( id COMPLEX ))

    proof

      let x be Element of F_Complex ;

      let n be Nat;

      

       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;

      thus f = ( FPower (x,n));

      now

        let y be Element of F_Complex ;

        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)

        .= ((x * ( power (y,n))) * y) by Def12

        .= (x * ((( power F_Complex ) . (y,n)) * y))

        .= (x * ( power (y,(n + 1)))) by GROUP_1:def 7;

      end;

      hence thesis by Def12;

    end;

    theorem :: POLYNOM5:70

    

     Th70: for x be Element of F_Complex holds for n be Nat holds ex f be Function of COMPLEX , COMPLEX st f = ( FPower (x,n)) & f is_continuous_on COMPLEX

    proof

      let x be Element of F_Complex ;

      defpred P[ Nat] means ex f be 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 be Nat st P[n] holds P[(n + 1)]

      proof

        let n be Nat;

        reconsider g = ( FPower (x,(n + 1))) as Function of COMPLEX , COMPLEX by A1;

        given f be Function of COMPLEX , COMPLEX such that

         A3: f = ( FPower (x,n)) & f is_continuous_on COMPLEX ;

        take g;

        thus g = ( FPower (x,(n + 1)));

        ex f1 be Function of COMPLEX , COMPLEX st f1 = ( FPower (x,n)) & ( FPower (x,(n + 1))) = (f1 (#) ( id COMPLEX )) by Th69;

        hence thesis by A3, Th62, CFCONT_1: 43;

      end;

      

       A4: P[ 0 ]

      proof

        reconsider f = ( FPower (x, 0 )) as Function of COMPLEX , COMPLEX by A1;

        take f;

        thus f = ( FPower (x, 0 ));

        f = (the carrier of F_Complex --> x) by Th66;

        hence thesis by A1, Th63;

      end;

      thus for n be Nat holds P[n] from NAT_1:sch 2( A4, A2);

    end;

    definition

      let L be well-unital non empty doubleLoopStr;

      let p be Polynomial of L;

      :: POLYNOM5:def13

      func Polynomial-Function (L,p) -> Function of L, L means

      : Def13: for x be Element of L holds (it . x) = ( eval (p,x));

      existence

      proof

        deffunc F( Element of L) = ( eval (p,$1));

        consider f be Function of the carrier of L, the carrier of L such that

         A1: for x be Element of L holds (f . x) = F(x) from FUNCT_2:sch 4;

        reconsider f as Function of L, L;

        take f;

        thus thesis by A1;

      end;

      uniqueness

      proof

        let f1,f2 be Function of L, L such that

         A2: for x be Element of L holds (f1 . x) = ( eval (p,x)) and

         A3: for x be Element of L holds (f2 . x) = ( eval (p,x));

        now

          let x be Element of L;

          

          thus (f1 . x) = ( eval (p,x)) by A2

          .= (f2 . x) by A3;

        end;

        hence f1 = f2 by FUNCT_2: 63;

      end;

    end

    theorem :: POLYNOM5:71

    

     Th71: for p be Polynomial of F_Complex holds ex f be 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 ;

      reconsider fzero = ( COMPLEX --> 0c ) as Element of FuFF by FUNCT_2: 9;

      defpred P[ 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 F( Element of FuFF, Element of FuFF) = ($1 + $2);

      take f;

      thus f = ( Polynomial-Function ( F_Complex ,p));

      

       A2: for x,y be Element of FuFF holds F(x,y) in FuFF by FUNCT_2: 8;

      consider fadd be BinOp of FuFF such that

       A3: for x,y be Element of FuFF holds (fadd . (x,y)) = F(x,y) from FUNCT_7:sch 1( A2);

      reconsider L = addLoopStr (# FuFF, fadd, fzero #) as non empty addLoopStr;

       A4:

      now

        let u,v,w be Element of L;

        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;

      end;

       A7:

      now

        let v be Element of L;

        reconsider v1 = v as Function of COMPLEX , COMPLEX by FUNCT_2: 66;

         A8:

        now

          let x be Element of COMPLEX ;

          

          thus ((v1 + fzero) . x) = ((v1 . x) + (fzero . x)) by VALUED_1: 1

          .= ((v1 . x) + 0c ) by FUNCOP_1: 7

          .= (v1 . x);

        end;

        

        thus (v + ( 0. L)) = (v1 + fzero) by A3

        .= v by A8, FUNCT_2: 63;

      end;

      L is right_complementable

      proof

        let v be Element of L;

        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;

         A9:

        now

          let x be Element of COMPLEX ;

          

          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;

        end;

        

        thus (v + w) = (v1 + ( - v1)) by A3

        .= ( 0. L) by A9, FUNCT_2: 63;

      end;

      then

      reconsider L as add-associative right_zeroed right_complementable non empty addLoopStr by A4, A7, RLVECT_1:def 3, RLVECT_1:def 4;

       A10:

      now

        let n be Nat;

        reconsider x = ( FPower ((p . (n -' 1)),(n -' 1))) as Element of L by A1, FUNCT_2: 9;

        assume n in ( Seg ( len p));

        take x;

        thus P[n, x];

      end;

      consider F be FinSequence of the carrier of L such that

       A11: ( dom F) = ( Seg ( len p)) and

       A12: for n be Nat st n in ( Seg ( len p)) holds P[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

        let x be Element of COMPLEX ;

        reconsider x1 = x as Element of F_Complex by COMPLFLD:def 1;

        consider H be 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 be 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 P[ Nat] means for SFk be 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 be Nat st P[k] holds P[(k + 1)]

        proof

          let k be Nat;

          reconsider kk = k as Element of NAT by ORDINAL1:def 12;

          assume

           A20: for SFk be Function of COMPLEX , COMPLEX st SFk = ( Sum (F | k)) holds ( Sum (H | k)) = (SFk . x);

          reconsider SFk1 = ( Sum (F | k)) as Function of COMPLEX , COMPLEX by FUNCT_2: 66;

          let SFk be Function of COMPLEX , COMPLEX ;

          assume

           A21: SFk = ( Sum (F | (k + 1)));

          per cases ;

            suppose

             A22: ( len F) > k;

            reconsider g2 = ( FPower ((p . kk),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 . kk),((k + 1) -' 1))) by NAT_D: 34

            .= ( FPower ((p . kk),k)) by NAT_D: 34;

            (F | (k + 1)) = ((F | k) ^ <*(F . (k + 1))*>) by A22, FINSEQ_5: 83

            .= ((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 . kk) * (( power F_Complex ) . (x1,((k + 1) -' 1)))) by NAT_D: 34

            .= ((p . kk) * ( power (x1,k))) by NAT_D: 34

            .= (( FPower ((p . kk),k)) . x) by Def12;

            (H | (k + 1)) = ((H | k) ^ <*(H . (k + 1))*>) by A16, A18, A22, FINSEQ_5: 83

            .= ((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;

          end;

            suppose

             A30: ( len F) <= k;

            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 thesis by A20, A21, A31;

          end;

        end;

        

         A32: P[ 0 ]

        proof

          let SFk be Function of COMPLEX , COMPLEX ;

          

           A33: (F | 0 ) = ( <*> the carrier of L);

          assume SFk = ( Sum (F | 0 ));

          

          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;

        end;

        

         A35: for k be Nat holds P[k] from NAT_1:sch 2( A32, A19);

        

         A36: ( Sum (F | ( len F))) = SF by FINSEQ_1: 58;

        

        thus (f . x) = ( Sum H) by A15, Def13

        .= ( Sum (H | ( len H))) by FINSEQ_1: 58

        .= (SF . x) by A16, A18, A35, A36;

      end;

      defpred P[ Nat] means for g be PartFunc of COMPLEX , COMPLEX st g = ( Sum (F | $1)) holds g is_continuous_on COMPLEX ;

      

       A37: for k be Nat st P[k] holds P[(k + 1)]

      proof

        let k be Nat;

        reconsider kk = k as Element of NAT by ORDINAL1:def 12;

        reconsider g1 = ( Sum (F | k)) as Function of COMPLEX , COMPLEX by FUNCT_2: 66;

        assume

         A38: for g be PartFunc of COMPLEX , COMPLEX st g = ( Sum (F | k)) holds g is_continuous_on COMPLEX ;

        then

         A39: g1 is_continuous_on COMPLEX ;

        let g be PartFunc of COMPLEX , COMPLEX ;

        assume

         A40: g = ( Sum (F | (k + 1)));

        per cases ;

          suppose

           A41: ( len F) > k;

          

           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 . kk),((k + 1) -' 1))) by NAT_D: 34

          .= ( FPower ((p . kk),k)) by NAT_D: 34;

          consider g2 be Function of COMPLEX , COMPLEX such that

           A45: g2 = ( FPower ((p . kk),k)) and

           A46: g2 is_continuous_on COMPLEX by Th70;

          (F | (k + 1)) = ((F | k) ^ <*(F . (k + 1))*>) by A41, FINSEQ_5: 83

          .= ((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 thesis by A39, A46, CFCONT_1: 43;

        end;

          suppose

           A47: ( len F) <= k;

          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 thesis by A38, A40;

        end;

      end;

      

       A48: P[ 0 ]

      proof

        let g be PartFunc of COMPLEX , COMPLEX ;

        

         A49: (F | 0 ) = ( <*> the carrier of L);

        assume g = ( Sum (F | 0 ));

        

        then g = ( 0. L) by A49, RLVECT_1: 43

        .= ( COMPLEX --> 0c );

        hence thesis by Th63;

      end;

      for k be Nat holds P[k] from NAT_1:sch 2( A48, A37);

      hence thesis by A13, A14, FUNCT_2: 63;

    end;

    theorem :: POLYNOM5:72

    

     Th72: for p be Polynomial of F_Complex st ( len p) > 2 & |.(p . (( len p) -' 1)).| = 1 holds for F be FinSequence of REAL st ( len F) = ( len p) & for n be Element of NAT st n in ( dom F) holds (F . n) = |.(p . (n -' 1)).| holds for z be Element of F_Complex st |.z.| > ( Sum F) holds |.( eval (p,z)).| > ( |.(p . 0 ).| + 1)

    proof

      let p be Polynomial of F_Complex ;

      assume that

       A1: ( len p) > 2 and

       A2: |.(p . (( len p) -' 1)).| = 1;

      let F be FinSequence of REAL ;

      assume that

       A3: ( len F) = ( len p) and

       A4: for n be Element of NAT st n in ( dom F) holds (F . n) = |.(p . (n -' 1)).|;

      set lF1 = (( len F) -' 1);

      

       A5: (lF1 + 1) = ( len F) by A1, A3, XREAL_1: 235, XXREAL_0: 2;

      

      then

       A6: F = (F | (lF1 + 1)) by FINSEQ_1: 58

      .= ((F | lF1) ^ <*(F /. (lF1 + 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

        let n be Element of NAT ;

        

         A10: ( dom (F | lF1)) c= ( dom F) by FINSEQ_5: 18;

        assume

         A11: n in ( dom (F | lF1));

        

        then ((F | lF1) . n) = ((F | lF1) /. 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 | lF1) . n) >= 0 by COMPLEX1: 46;

      end;

      

       A12: ( len (F | lF1)) = lF1 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 ;

      consider G be 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 be 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);

      

       A18: ( len F) in ( dom F) by A7, A3, FINSEQ_3: 25;

      

      then (F /. (lF1 + 1)) = (F . (lF1 + 1)) by A5, PARTFUN1:def 6

      .= 1 by A2, A3, A4, A5, A18;

      then

       A19: ( Sum F) = (( Sum (F | lF1)) + 1) by A6, RVSUM_1: 74;

      

       A20: ( len F) >= ((1 + 1) + 0 ) by A1, A3;

      then lF1 >= 1 by A5, XREAL_1: 6;

      then

       A21: 1 in ( dom (F | lF1)) by A12, FINSEQ_3: 25;

      

      then ((F | lF1) . 1) = ((F | lF1) /. 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 | lF1)) >= |.(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 | (lF1 + 1)) by A3, A15, A5, FINSEQ_1: 58

      .= ((G | lF1) ^ <*(G /. (lF1 + 1))*>) by A3, A15, A5, FINSEQ_5: 82;

      then

       A24: ( Sum G) = (( Sum (G | lF1)) + (G /. (lF1 + 1))) by FVSUM_1: 71;

      

       A25: ( dom F) = ( dom G) by A3, A15, FINSEQ_3: 29;

      

      then (G /. (lF1 + 1)) = (G . (lF1 + 1)) by A5, A18, PARTFUN1:def 6

      .= ((p . lF1) * (( power F_Complex ) . (z,lF1))) by A16, A5, A18, A25;

      then |.(G /. (lF1 + 1)).| = (1 * |.(( power F_Complex ) . (z,lF1)).|) by A2, A3, COMPLFLD: 71;

      then

       A26: |.( eval (p,z)).| >= ( |.(( power F_Complex ) . (z,lF1)).| - |.( Sum (G | lF1)).|) by A14, A24, COMPLFLD: 64;

      

       A27: (( len F) - 1) >= 0 by A7, A3;

      

       A28: ( len (F | lF1)) = lF1 by A5, FINSEQ_1: 59, NAT_1: 11

      .= ( len (G | lF1)) by A3, A15, A5, FINSEQ_1: 59, NAT_1: 11;

      then

       A29: ((F | lF1) | ( len (F | lF1))) = (F | lF1) & ((G | lF1) | ( len (F | lF1))) = (G | lF1) by FINSEQ_1: 58;

      defpred P[ Nat] means |.( Sum ((G | lF1) | $1)).| <= (( Sum ((F | lF1) | $1)) * |.(( power F_Complex ) . (z,lF2)).|);

      (( len F) - 2) >= 0 by A20, XREAL_1: 19;

      

      then

       A30: (lF2 + 1) = ((( len F) - 2) + 1) by XREAL_0:def 2

      .= lF1 by A27, XREAL_0:def 2;

      then (( power F_Complex ) . (z,lF1)) = ((( power F_Complex ) . (z,lF2)) * z) by GROUP_1:def 7;

      

      then

       A31: ( |.(( power F_Complex ) . (z,lF1)).| - ( |.(( power F_Complex ) . (z,lF2)).| * ( Sum (F | lF1)))) = (( |.(( power F_Complex ) . (z,lF2)).| * |.z.|) - ( |.(( power F_Complex ) . (z,lF2)).| * ( Sum (F | lF1)))) by COMPLFLD: 71

      .= ( |.(( power F_Complex ) . (z,lF2)).| * ( |.z.| - ( Sum (F | lF1))));

      

       A32: |.z.| > ( |.(p . 0 ).| + 1) by A17, A22, XXREAL_0: 2;

      then

       A33: |.z.| > 1 by A13, XXREAL_0: 2;

      

       A34: ( dom (F | lF1)) = ( dom (G | lF1)) by A28, FINSEQ_3: 29;

      

       A35: for n be Nat st P[n] holds P[(n + 1)]

      proof

        let n be Nat;

        reconsider nn = n as Element of NAT by ORDINAL1:def 12;

        assume

         A36: |.( Sum ((G | lF1) | n)).| <= (( Sum ((F | lF1) | n)) * |.(( power F_Complex ) . (z,lF2)).|);

        then

         A37: ( |.( Sum ((G | lF1) | n)).| + |.((G | lF1) /. (n + 1)).|) <= ((( Sum ((F | lF1) | n)) * |.(( power F_Complex ) . (z,lF2)).|) + |.((G | lF1) /. (n + 1)).|) by XREAL_1: 6;

        per cases ;

          suppose

           A38: (n + 1) <= ( len (G | lF1));

          then (n + 1) <= (lF2 + 1) by A3, A15, A5, A30, FINSEQ_1: 59, NAT_1: 11;

          then n <= lF2 by XREAL_1: 6;

          then ( |.z.| to_power n) <= ( |.z.| to_power lF2) by A33, PRE_FF: 8;

          then ( |.z.| to_power n) <= |.( power (z,lF2)).| by A23, Th7;

          then

           A39: |.(p . nn).| >= 0 & |.( power (z,n)).| <= |.( power (z,lF2)).| by A23, Th7, COMPLEX1: 46;

          ((G | lF1) | (n + 1)) = (((G | lF1) | n) ^ <*((G | lF1) /. (n + 1))*>) by A38, FINSEQ_5: 82;

          then ( Sum ((G | lF1) | (n + 1))) = (( Sum ((G | lF1) | n)) + ((G | lF1) /. (n + 1))) by FVSUM_1: 71;

          then |.( Sum ((G | lF1) | (n + 1))).| <= ( |.( Sum ((G | lF1) | n)).| + |.((G | lF1) /. (n + 1)).|) by COMPLFLD: 62;

          then

           A40: |.( Sum ((G | lF1) | (n + 1))).| <= ((( Sum ((F | lF1) | n)) * |.(( power F_Complex ) . (z,lF2)).|) + |.((G | lF1) /. (n + 1)).|) by A37, XXREAL_0: 2;

          

           A41: ( dom (G | lF1)) c= ( dom G) by FINSEQ_5: 18;

          (n + 1) >= 1 by NAT_1: 11;

          then

           A42: (n + 1) in ( dom (G | lF1)) by A38, FINSEQ_3: 25;

          

          then

           A43: ((F | lF1) /. (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 . nn).| by NAT_D: 34;

          ((G | lF1) /. (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 . nn) * (( power F_Complex ) . (z,((n + 1) -' 1)))) by NAT_D: 34

          .= ((p . nn) * (( power F_Complex ) . (z,n))) by NAT_D: 34;

          then |.((G | lF1) /. (n + 1)).| = (((F | lF1) /. (n + 1)) * |.(( power F_Complex ) . (z,n)).|) by A43, COMPLFLD: 71;

          then |.((G | lF1) /. (n + 1)).| <= (((F | lF1) /. (n + 1)) * |.(( power F_Complex ) . (z,lF2)).|) by A43, A39, XREAL_1: 64;

          then

           A44: ((( Sum ((F | lF1) | n)) * |.(( power F_Complex ) . (z,lF2)).|) + |.((G | lF1) /. (n + 1)).|) <= ((( Sum ((F | lF1) | n)) * |.(( power F_Complex ) . (z,lF2)).|) + (((F | lF1) /. (n + 1)) * |.(( power F_Complex ) . (z,lF2)).|)) by XREAL_1: 6;

          ((F | lF1) | (n + 1)) = (((F | lF1) | n) ^ <*((F | lF1) /. (n + 1))*>) by A28, A38, FINSEQ_5: 82;

          then ( Sum ((F | lF1) | (n + 1))) = (( Sum ((F | lF1) | n)) + ((F | lF1) /. (n + 1))) by RVSUM_1: 74;

          hence thesis by A40, A44, XXREAL_0: 2;

        end;

          suppose

           A45: (n + 1) > ( len (G | lF1));

          then n >= ( len (G | lF1)) by NAT_1: 13;

          then

           A46: ((G | lF1) | n) = (G | lF1) & ((F | lF1) | n) = (F | lF1) by A28, FINSEQ_1: 58;

          ((G | lF1) | (n + 1)) = (G | lF1) by A45, FINSEQ_1: 58;

          hence thesis by A28, A36, A45, A46, FINSEQ_1: 58;

        end;

      end;

      ((G | lF1) | 0 ) = ( <*> the carrier of F_Complex );

      then

       A47: P[ 0 ] by COMPLFLD: 57, RLVECT_1: 43, RVSUM_1: 72;

      for n be Nat holds P[n] from NAT_1:sch 2( A47, A35);

      then |.( Sum (G | lF1)).| <= (( Sum (F | lF1)) * |.(( power F_Complex ) . (z,lF2)).|) by A29;

      then ( |.(( power F_Complex ) . (z,lF1)).| - |.( Sum (G | lF1)).|) >= ( |.(( power F_Complex ) . (z,lF1)).| - (( Sum (F | lF1)) * |.(( power F_Complex ) . (z,lF2)).|)) by XREAL_1: 13;

      then

       A48: |.( eval (p,z)).| >= ( |.(( power F_Complex ) . (z,lF1)).| - ( |.(( power F_Complex ) . (z,lF2)).| * ( Sum (F | lF1)))) 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 lF2 >= 1 by XREAL_0:def 2;

      then ( |.z.| to_power lF2) >= ( |.z.| to_power 1) by A33, PRE_FF: 8;

      then |.( power (z,lF2)).| >= ( |.z.| to_power 1) by A23, Th7;

      then |.(( power F_Complex ) . (z,lF2)).| >= |.( power (z,1)).| by A23, Th7;

      then

       A49: |.(( power F_Complex ) . (z,lF2)).| >= |.z.| by GROUP_1: 50;

       |.(( power F_Complex ) . (z,lF2)).| >= 0 & ( |.z.| - ( Sum (F | lF1))) > 1 by A17, A19, COMPLEX1: 46, XREAL_1: 20;

      then ( |.(( power F_Complex ) . (z,lF2)).| * ( |.z.| - ( Sum (F | lF1)))) >= ( |.(( power F_Complex ) . (z,lF2)).| * 1) by XREAL_1: 64;

      then |.( eval (p,z)).| >= |.(( power F_Complex ) . (z,lF2)).| by A48, A31, XXREAL_0: 2;

      then |.( eval (p,z)).| >= |.z.| by A49, XXREAL_0: 2;

      hence thesis by A32, XXREAL_0: 2;

    end;

    theorem :: POLYNOM5:73

    

     Th73: for p be Polynomial of F_Complex st ( len p) > 2 holds ex z0 be Element of F_Complex st for z be Element of F_Complex holds |.( eval (p,z)).| >= |.( eval (p,z0)).|

    proof

      defpred P[ set] means not contradiction;

      let p be Polynomial of F_Complex ;

      set np = ( NormPolynomial p);

      deffunc F( Element of F_Complex ) = ( In ( |.( eval (np,$1)).|, REAL ));

      reconsider D = { F(z) where z be Element of F_Complex : P[z] } as Subset of REAL from DOMAIN_1:sch 8;

      set q = ( lower_bound D);

      

       A1: D is bounded_below

      proof

        take 0 ;

        let b be ExtReal;

        assume b in D;

        then

        consider z be Element of F_Complex such that

         A2: b = ( In ( |.( eval (np,z)).|, REAL ));

        b = |.( eval (np,z)).| by A2;

        hence thesis by COMPLEX1: 46;

      end;

      defpred P[ Nat, object] means ex g1 be Element of F_Complex st g1 = $2 & |.( eval (np,g1)).| < (q + (1 / ($1 + 1)));

      ( In ( |.( eval (np,( 0. F_Complex ))).|, REAL )) = |.( eval (np,( 0. F_Complex ))).|;

      then

       A3: |.( eval (np,( 0. F_Complex ))).| in D;

      

       A4: for n be Nat holds ex g be Complex st P[n, g]

      proof

        let n be Nat;

        consider r be Real such that

         A5: r in D and

         A6: r < (q + (1 / (n + 1))) by A3, A1, SEQ_4:def 2;

        consider g1 be Element of F_Complex such that

         A7: r = ( In ( |.( eval (np,g1)).|, REAL )) by A5;

        reconsider g = g1 as Element of COMPLEX by COMPLFLD:def 1;

        take g, g1;

        thus g1 = g;

        thus thesis by A6, A7;

      end;

      consider G be Complex_Sequence such that

       A8: for n be Nat holds P[n, (G . n)] from CFCONT_1:sch 1( A4);

      deffunc G( Nat) = ( In ( |.(np . ($1 -' 1)).|, REAL ));

      consider F be FinSequence of REAL such that

       A9: ( len F) = ( len np) and

       A10: for n be Nat st n in ( dom F) holds (F . n) = G(n) from FINSEQ_2:sch 1;

      assume

       A11: ( len p) > 2;

      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;

      G is bounded

      proof

        take r = (( Sum F) + 1);

        let n be Nat;

        consider Gn be Element of F_Complex such that

         A14: Gn = (G . n) and

         A15: |.( eval (np,Gn)).| < (q + (1 / (n + 1))) by A8;

        (n + 1) >= ( 0 + 1) by XREAL_1: 6;

        then

         A16: (1 / (n + 1)) <= 1 by XREAL_1: 211;

        

         A17: ( len np) = ( len p) by A11, Th57;

        then

         A18: (np . (( len np) -' 1)) = ( 1_ F_Complex ) by A11, Th56;

         |.(G . n).| <= ( Sum F)

        proof

          

           A19: ( eval (np,( 0. F_Complex ))) = (np . 0 ) by Th31;

          ( In ( |.(np . 0 ).|, REAL )) = |.(np . 0 ).|;

          then |.(np . 0 ).| in D by A19;

          then |.(np . 0 ).| >= q by A1, SEQ_4:def 2;

          then

           A20: ( |.(np . 0 ).| + 1) >= (q + (1 / (n + 1))) by A16, XREAL_1: 7;

          

           A21: for n be Element of NAT st n in ( dom F) holds (F . n) = |.(np . (n -' 1)).|

          proof

            let n be Element of NAT ;

            assume n in ( dom F);

            then (F . n) = G(n) by A10;

            hence (F . n) = |.(np . (n -' 1)).|;

          end;

          assume |.(G . n).| > ( Sum F);

          then |.( eval (np,Gn)).| > ( |.(np . 0 ).| + 1) by A11, A9, A14, A17, A18, A21, COMPLFLD: 60, Th72;

          hence contradiction by A15, A20, XXREAL_0: 2;

        end;

        then ( |.(G . n).| + 0 ) < r by XREAL_1: 8;

        hence thesis;

      end;

      then

      consider G1 be Complex_Sequence such that

       A22: G1 is subsequence of G and

       A23: G1 is convergent by COMSEQ_3: 50;

      defpred P[ Nat, object] means ex G1n be Element of F_Complex st G1n = (G1 . $1) & $2 = ( eval (np,G1n));

      ( lim G1) in COMPLEX by XCMPLX_0:def 2;

      then

      reconsider z0 = ( lim G1) as Element of F_Complex by COMPLFLD:def 1;

      

       A24: for n be Nat holds ex g be Complex st P[n, g]

      proof

        let n be Nat;

        reconsider nn = n as Element of NAT by ORDINAL1:def 12;

        reconsider G1n = (G1 . nn) as Element of F_Complex by COMPLFLD:def 1;

        reconsider g = ( eval (np,G1n)) as Element of COMPLEX by COMPLFLD:def 1;

        take g, G1n;

        thus G1n = (G1 . n);

        thus thesis;

      end;

      consider H be Complex_Sequence such that

       A25: for n be Nat holds P[n, (H . n)] from CFCONT_1:sch 1( A24);

      reconsider enp0 = ( eval (np,z0)) as Element of COMPLEX by COMPLFLD:def 1;

      consider g be Complex such that

       A26: for p be Real st 0 < p holds ex n be Nat st for m be Nat st n <= m holds |.((G1 . m) - g).| < p by A23;

      

       A27: g in COMPLEX by XCMPLX_0:def 2;

      then

      reconsider g1 = g as Element of F_Complex by COMPLFLD:def 1;

      reconsider eg = ( eval (np,g1)) as Element of COMPLEX by COMPLFLD:def 1;

      now

        let p be Real;

        consider fPF be Function of COMPLEX , COMPLEX such that

         A28: fPF = ( Polynomial-Function ( F_Complex ,np)) and

         A29: fPF is_continuous_on COMPLEX by Th71;

        assume 0 < p;

        then

        consider p1 be Real such that

         A30: 0 < p1 and

         A31: for x1 be Complex st x1 in COMPLEX & |.(x1 - g).| < p1 holds |.((fPF /. x1) - (fPF /. g)).| < p by A29, CFCONT_1: 39, A27;

        consider n be Nat such that

         A32: for m be Nat st n <= m holds |.((G1 . m) - g).| < p1 by A26, A30;

        take n;

        let m be Nat;

        reconsider mm = m as Element of NAT by ORDINAL1:def 12;

        assume n <= m;

        then

         A33: |.((G1 . m) - g).| < p1 by A32;

        ex G1m be Element of F_Complex st G1m = (G1 . m) & (H . m) = ( eval (np,G1m)) by A25;

        then

         A34: (H . m) = (fPF /. (G1 . mm)) by A28, Def13;

        eg = (fPF /. g) by A28, Def13;

        hence |.((H . m) - eg).| < p by A31, A33, A34;

      end;

      then

       A35: H is convergent;

      consider PF be Function of COMPLEX , COMPLEX such that

       A36: PF = ( Polynomial-Function ( F_Complex ,np)) and

       A37: PF is_continuous_on COMPLEX by Th71;

      now

        let a be Real;

        

         A38: ( lim G1) in COMPLEX by XCMPLX_0:def 2;

        assume 0 < a;

        then

        consider s be Real such that

         A39: 0 < s and

         A40: for x1 be Complex st x1 in COMPLEX & |.(x1 - ( lim G1)).| < s holds |.((PF /. x1) - (PF /. ( lim G1))).| < a by A37, CFCONT_1: 39, A38;

        consider n be Nat such that

         A41: for m be Nat st n <= m holds |.((G1 . m) - ( lim G1)).| < s by A23, A39, COMSEQ_2:def 6;

        take n;

        let m be Nat;

        reconsider mm = m as Element of NAT by ORDINAL1:def 12;

        assume n <= m;

        then

         A42: |.((G1 . m) - ( lim G1)).| < s by A41;

        ex G1m be Element of F_Complex st G1m = (G1 . m) & (H . m) = ( eval (np,G1m)) by A25;

        then

         A43: (PF /. (G1 . mm)) = (H . m) by A36, Def13;

        (PF /. ( lim G1)) = ( eval (np,z0)) by A36, Def13;

        hence |.((H . m) - enp0).| < a by A40, A42, A43;

      end;

      then

       A44: enp0 = ( lim H) by A35, COMSEQ_2:def 6;

      deffunc F( Nat) = (1 / ($1 + 1));

      consider R be Real_Sequence such that

       A45: for n be Nat holds (R . n) = F(n) from SEQ_1:sch 1;

      take z0;

      let z be Element of F_Complex ;

      reconsider v = |.( eval (np,z)).| as Element of REAL by XREAL_0:def 1;

      set Rcons = ( seq_const |.( eval (np,z)).|);

      consider Nseq be increasing sequence of NAT such that

       A46: G1 = (G * Nseq) by A22, VALUED_0:def 17;

      ( In ( |.( eval (np,z)).|, REAL )) = |.( eval (np,z)).|;

      then |.( eval (np,z)).| in D;

      then

       A47: |.( eval (np,z)).| >= q by A1, SEQ_4:def 2;

       A48:

      now

        let n be Nat;

        

         A49: n in NAT by ORDINAL1:def 12;

        consider G1n be Element of F_Complex such that

         A50: G1n = (G1 . n) and

         A51: (H . n) = ( eval (np,G1n)) by A25;

        consider gNn be Element of F_Complex such that

         A52: gNn = (G . (Nseq . n)) and

         A53: |.( eval (np,gNn)).| < (q + (1 / ((Nseq . n) + 1))) by A8;

        (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 (q + (1 / ((Nseq . n) + 1))) <= (q + (1 / (n + 1))) by XREAL_1: 6;

        then |.( eval (np,gNn)).| < (q + (1 / (n + 1))) by A53, XXREAL_0: 2;

        then q > ( |.( eval (np,gNn)).| - (1 / (n + 1))) by XREAL_1: 19;

        then

         A54: (Rcons . n) = |.( eval (np,z)).| & |.( eval (np,z)).| > ( |.( eval (np,gNn)).| - (1 / (n + 1))) by A47, SEQ_1: 57, XXREAL_0: 2;

        ( dom ( |.H.| - R)) = NAT by FUNCT_2:def 1;

        

        then (( |.H.| - R) . n) = (( |.H.| . n) - (R . n)) by VALUED_1: 13, A49

        .= (( |.H.| . n) - (1 / (n + 1))) by A45

        .= ( |.( eval (np,G1n)).| - (1 / (n + 1))) by A51, VALUED_1: 18;

        hence (Rcons . n) >= (( |.H.| - R) . n) by A46, A50, A52, A54, FUNCT_2: 15, A49;

      end;

      

       A55: R is convergent by A45, SEQ_4: 31;

      then ( |.H.| - R) is convergent by A35;

      then (Rcons . 0 ) = |.( eval (np,z)).| & ( lim ( |.H.| - R)) <= ( lim Rcons) by A48, SEQ_1: 57, SEQ_2: 18;

      then

       A56: ( lim ( |.H.| - R)) <= |.( eval (np,z)).| by SEQ_4: 25;

      ( lim ( |.H.| - R)) = (( lim |.H.|) - ( lim R)) by A35, A55, SEQ_2: 12

      .= ( |.( lim H).| - ( lim R)) by A35, SEQ_2: 27

      .= ( |.( lim H).| - 0 ) by A45, SEQ_4: 31;

      then |.(( eval (p,z)) / (p . (( len p) -' 1))).| >= |.( eval (np,z0)).| by A11, A56, A44, 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 thesis by A13, XREAL_1: 74;

    end;

    ::$Notion-Name

    theorem :: POLYNOM5:74

    

     Th74: for p be Polynomial of F_Complex st ( len p) > 1 holds p is with_roots

    proof

      let p be Polynomial of F_Complex ;

      assume

       A1: ( len p) > 1;

      then

       A2: ( len p) >= (1 + 1) by NAT_1: 13;

      per cases by A2, XXREAL_0: 1;

        suppose ( len p) > 2;

        then

        consider z0 be Element of F_Complex such that

         A3: for z be Element of F_Complex holds |.( eval (p,z)).| >= |.( eval (p,z0)).| by Th73;

        set q = ( Subst (p, <%z0, ( 1_ F_Complex )%>));

        defpred P[ Nat] means $1 >= 1 & (q . $1) <> ( 0. F_Complex );

        ( len <%z0, ( 1_ F_Complex )%>) = 2 by Th40;

        

        then

         A4: ( len q) = ((((2 * ( len p)) - ( len p)) - 2) + 2) by A1, Th52

        .= ( len p);

        

         A5: ex k be Nat st P[k]

        proof

          (( len q) - 1) = (( len q) -' 1) by A1, A4, XREAL_0:def 2;

          then

          reconsider k = (( len q) - 1) as Element of NAT ;

          take k;

          ( len q) >= (1 + 1) by A1, A4, NAT_1: 13;

          hence k >= 1 by XREAL_1: 19;

          ( len q) = (k + 1);

          hence (q . k) <> ( 0. F_Complex ) by ALGSEQ_1: 10;

        end;

        consider k be Nat such that

         A6: P[k] and

         A7: for n be Nat st P[n] holds k <= n from NAT_1:sch 5( A5);

        

         A8: (k + 1) > 1 by A6, NAT_1: 13;

        reconsider k1 = k as non zero Element of NAT by A6, ORDINAL1:def 12;

        set sq = the CRoot of k1, ( - ((q . 0 ) / (q . k1)));

        deffunc O( Nat) = ((q . ( In ((k1 + $1), NAT ))) * (( power F_Complex ) . (sq,( In ((k1 + $1), NAT )))));

        consider F2 be FinSequence of the carrier of F_Complex such that

         A9: ( len F2) = (( len q) -' (k1 + 1)) and

         A10: for n be Nat st n in ( dom F2) holds (F2 . n) = O(n) from FINSEQ_2:sch 1;

        k1 < ( len q) by A6, ALGSEQ_1: 8;

        then

         A11: ((k + 1) + 0 ) <= ( len q) by NAT_1: 13;

        then (( len q) - (k + 1)) >= 0 by XREAL_1: 19;

        then

         A12: ( len F2) = (( len q) - (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 (q,( 0. F_Complex ))) by Th53;

         A14:

        now

          let z be Element of F_Complex ;

          ( eval (q,z)) = ( eval (p,( eval ( <%z0, ( 1_ F_Complex )%>,z)))) by Th53

          .= ( eval (p,(z0 + z))) by Th47;

          then |.( eval (q,z)).| >= |.( eval (p,z0)).| by A3;

          hence |.( eval (q,z)).| >= |.(q . 0 ).| by A13, Th31;

        end;

        now

          let c be Real;

          assume that

           A15: 0 < c and

           A16: c < 1;

          set z1 = ( [**c, 0 **] * sq);

          consider F1 be FinSequence of the carrier of F_Complex such that

           A17: ( eval (q,z1)) = ( Sum F1) and

           A18: ( len F1) = ( len q) and

           A19: for n be Element of NAT st n in ( dom F1) holds (F1 . n) = ((q . (n -' 1)) * (( power F_Complex ) . (z1,(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

            let i be Element of NAT ;

            assume that

             A24: i in ( dom (F1 | k)) and

             A25: i <> 1;

            

             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;

            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

            .= ((q . (i -' 1)) * (( power F_Complex ) . (z1,(i -' 1)))) by A19, A23, A24

            .= (( 0. F_Complex ) * (( power F_Complex ) . (z1,(i -' 1)))) by A7, A27, A29

            .= ( 0. F_Complex );

          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

          .= ((q . (1 -' 1)) * (( power F_Complex ) . (z1,(1 -' 1)))) by A19, A22, A23

          .= ((q . 0 ) * (( power F_Complex ) . (z1,(1 -' 1)))) by XREAL_1: 232

          .= ((q . 0 ) * (( power F_Complex ) . (z1, 0 ))) by XREAL_1: 232

          .= ((q . 0 ) * ( 1_ F_Complex )) by GROUP_1:def 7

          .= (q . 0 );

          (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 **] * gc);

          

           A35: (F1 /. (k + 1)) = (F1 . (k + 1)) by A31, PARTFUN1:def 6

          .= ((q . ((k + 1) -' 1)) * (( power F_Complex ) . (z1,((k + 1) -' 1)))) by A19, A31

          .= ((q . k1) * (( power F_Complex ) . (z1,((k + 1) -' 1)))) by NAT_D: 34

          .= ((q . k1) * (( power F_Complex ) . (z1,k1))) by NAT_D: 34

          .= ((q . k1) * ((( power F_Complex ) . ( [**c, 0 **],k1)) * (( power F_Complex ) . (sq,k1)))) by GROUP_1: 52

          .= ((q . k1) * ((( power F_Complex ) . ( [**c, 0 **],k1)) * ( - ((q . 0 ) / (q . k1))))) by COMPLFLD:def 2

          .= (((q . k1) * ( - ((q . 0 ) / (q . k1)))) * (( power F_Complex ) . ( [**c, 0 **],k1)))

          .= (((q . k1) * (( - (q . 0 )) / (q . k1))) * (( power F_Complex ) . ( [**c, 0 **],k1))) by A6, COMPLFLD: 42

          .= ((((q . k1) * ( - (q . 0 ))) / (q . k1)) * (( power F_Complex ) . ( [**c, 0 **],k1)))

          .= (( - (q . 0 )) * (( power F_Complex ) . ( [**c, 0 **],k1))) by A6, COMPLFLD: 30

          .= (( - (q . 0 )) * [**(c to_power k), 0 **]) by A15, HAHNBAN1: 29;

          

           A36: |.(((q . 0 ) * (( 1_ F_Complex ) - [**(c to_power k), 0 **])) + ( [**(c to_power (k + 1)), 0 **] * gc)).| <= ( |.((q . 0 ) * (( 1_ F_Complex ) - [**(c to_power k), 0 **])).| + |.( [**(c to_power (k + 1)), 0 **] * gc).|) 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

          .= (((q . 0 ) + (( - (q . 0 )) * [**(c to_power k), 0 **])) + ( Sum (F1 /^ (k + 1)))) by A30, A35, RLVECT_1: 44

          .= (((q . 0 ) + ( - ((q . 0 ) * [**(c to_power k), 0 **]))) + ( Sum (F1 /^ (k + 1)))) by VECTSP_1: 9

          .= ((((q . 0 ) * ( 1_ F_Complex )) - ((q . 0 ) * [**(c to_power k), 0 **])) + ( Sum (F1 /^ (k + 1))))

          .= (((q . 0 ) * (( 1_ F_Complex ) - [**(c to_power k), 0 **])) + ( [**(c to_power (k + 1)), 0 **] * gc)) by A34, VECTSP_1: 11;

          then |.(((q . 0 ) * (( 1_ F_Complex ) - [**(c to_power k), 0 **])) + ( [**(c to_power (k + 1)), 0 **] * gc)).| >= |.(q . 0 ).| by A14, A17;

          then ( |.((q . 0 ) * (( 1_ F_Complex ) - [**(c to_power k), 0 **])).| + |.( [**(c to_power (k + 1)), 0 **] * gc).|) >= |.(q . 0 ).| by A36, XXREAL_0: 2;

          then (( |.(q . 0 ).| * |.(( 1_ F_Complex ) - [**(c to_power k), 0 **]).|) + |.( [**(c to_power (k + 1)), 0 **] * gc).|) >= |.(q . 0 ).| by COMPLFLD: 71;

          then

           A37: (( |.(q . 0 ).| * |.(( 1_ F_Complex ) - [**(c to_power k), 0 **]).|) + ( |. [**(c to_power (k + 1)), 0 **].| * |.gc.|)) >= |.(q . 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 Def2

          .= ( len (F1 /^ (k + 1))) by A20, FINSEQ_3: 29

          .= (( len F1) - (k + 1)) by A11, A18, RFINSEQ:def 1

          .= ( len |.F2.|) by A12, A18, Def2;

          now

            let i be Element of NAT ;

            

             A41: (((k + 1) + i) -' 1) = (((k + i) + 1) - 1) by XREAL_0:def 2

            .= (k + i);

            assume i in ( dom |.((F1 /^ (k + 1)) * ( [**(c to_power (k + 1)), 0 **] " )).|);

            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, Def2;

            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 ;

            (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, Def2;

            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

            .= ((q . ( In ((((k + 1) + i) -' 1), NAT ))) * (( power F_Complex ) . (( [**c, 0 **] * sq),(((k + 1) + i) -' 1)))) by A19, A44

            .= ((q . ( In ((k + i), NAT ))) * (( power (sq,(k + i))) * ( power ( [**c, 0 **],(k + i))))) by A41, GROUP_1: 52

            .= (((q . ( In ((k + i), NAT ))) * ( power (sq,(k + i)))) * ( power ( [**c, 0 **],(k + i))));

            

             A51: ( len F2) = ( len |.F2.|) by Def2;

            

             A53: ( |.((F1 /^ (k + 1)) * ( [**(c to_power (k + 1)), 0 **] " )).| . i) = |.(((F1 /^ (k + 1)) * ( [**(c to_power (k + 1)), 0 **] " )) . i).| by A49, Def2

            .= |.(((F1 /^ (k + 1)) * ( [**(c to_power (k + 1)), 0 **] " )) /. i).| by A49, PARTFUN1:def 6

            .= |.(((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

            .= ( |.(((q . ( In ((k + i), NAT ))) * ( power (sq,(k + i)))) * ( power ( [**c, 0 **],(k + i)))).| * ( |.(c to_power (k + 1)).| " )) by A33, A50, COMPLFLD: 7, COMPLFLD: 72

            .= (( |.((q . ( In ((k + i), NAT ))) * ( power (sq,(k + i)))).| * |.( power ( [**c, 0 **],(k + i))).|) * ( |.(c to_power (k + 1)).| " )) by COMPLFLD: 71

            .= (( |.((q . ( In ((k + i), NAT ))) * ( power (sq,(k + i)))).| * |. [**(c to_power (k + i)), 0 **].|) * ( |.(c to_power (k + 1)).| " )) by A15, HAHNBAN1: 29

            .= (( |.((q . ( In ((k + i), NAT ))) * ( power (sq,(k + i)))).| * (c to_power (k + i))) * ( |.(c to_power (k + 1)).| " )) by A47, ABSVALUE:def 1

            .= (( |.((q . ( In ((k + i), NAT ))) * ( power (sq,(k + i)))).| * (c to_power (k + i))) * ((c to_power ( In ((k + 1), NAT ))) " )) by A33, ABSVALUE:def 1

            .= ( |.((q . ( In ((k + i), NAT ))) * ( power (sq,(k + i)))).| * ((c to_power (k + i)) * ((c to_power (k + 1)) " )))

            .= ( |.((q . ( In ((k + i), NAT ))) * ( power (sq,(k + i)))).| * ((c to_power (k + i)) / (c to_power (k + 1))))

            .= ( |.((q . ( In ((k + i), NAT ))) * ( power (sq,(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;

            ((q . ( In ((k + i), NAT ))) * ( power (sq,(k + i)))) = ((q . ( In ((k + i), NAT ))) * (( power F_Complex ) . (sq,( In ((k + i), NAT )))))

            .= O(i)

            .= (F2 . i) by A54, A10;

            then ( |.((F1 /^ (k + 1)) * ( [**(c to_power (k + 1)), 0 **] " )).| . i) <= |.(F2 . i).| by A46, A53, COMPLEX1: 46, XREAL_1: 153;

            hence ( |.((F1 /^ (k + 1)) * ( [**(c to_power (k + 1)), 0 **] " )).| . i) <= ( |.F2.| . i) by A54, Def2;

          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 **].| * |.gc.|) >= (( |.(q . 0 ).| * 1) - ( |.(q . 0 ).| * (1 - (c to_power k)))) by A37, XREAL_1: 20;

          then ((c to_power (k + 1)) * |.gc.|) >= ( |.(q . 0 ).| * (c to_power k)) by A33, ABSVALUE:def 1;

          then (((c to_power (k + 1)) * |.gc.|) / (c to_power k)) >= (( |.(q . 0 ).| * (c to_power k)) / (c to_power k)) by A39, XREAL_1: 72;

          then (((c to_power (k + 1)) / (c to_power k)) * |.gc.|) >= |.(q . 0 ).| by A39, XCMPLX_1: 89;

          then ((c to_power ((k + 1) - k)) * |.gc.|) >= |.(q . 0 ).| by A15, POWER: 29;

          then

           A56: (c * |.gc.|) >= |.(q . 0 ).| by POWER: 25;

          gc = (( Sum (F1 /^ (k + 1))) * ( [**(c to_power (k + 1)), 0 **] " ))

          .= ( Sum ((F1 /^ (k + 1)) * ( [**(c to_power (k + 1)), 0 **] " ))) by POLYNOM1: 13;

          then |.gc.| <= ( Sum |.((F1 /^ (k + 1)) * ( [**(c to_power (k + 1)), 0 **] " )).|) by Th14;

          then |.gc.| <= ( Sum |.F2.|) by A55, XXREAL_0: 2;

          then (c * |.gc.|) <= (c * ( Sum |.F2.|)) by A15, XREAL_1: 64;

          hence (c * ( Sum |.F2.|)) >= |.(q . 0 ).| by A56, XXREAL_0: 2;

        end;

        then |.(q . 0 ).| <= 0 by Lm1;

        then

         A57: (q . 0 ) = ( 0. F_Complex ) by COMPLFLD: 59;

        ex x be Element of F_Complex st x is_a_root_of p

        proof

          take z0;

          ( eval (p,z0)) = ( 0. F_Complex ) by A13, A57, Th31;

          hence thesis;

        end;

        hence thesis;

      end;

        suppose

         A58: ( len p) = 2;

        set np = ( NormPolynomial p);

        

         A59: (( len p) -' 1) = (2 - 1) by A58, XREAL_0:def 2;

        

         A60: ( len np) = ( len p) by A58, Th57;

         A61:

        now

          let k be Nat;

          assume

           A62: k < ( len np);

          per cases by A58, A60, A62, NAT_1: 23;

            suppose k = 0 ;

            hence (np . k) = ( <%(np . 0 ), ( 1_ F_Complex )%> . k) by Th38;

          end;

            suppose

             A63: k = 1;

            

            hence (np . k) = ( 1_ F_Complex ) by A58, A59, Th56

            .= ( <%(np . 0 ), ( 1_ F_Complex )%> . k) by A63, Th38;

          end;

        end;

        ( len <%(np . 0 ), ( 1_ F_Complex )%>) = 2 by Th40;

        then

         A64: np = <%(np . 0 ), ( 1_ F_Complex )%> by A58, A61, Th57, ALGSEQ_1: 12;

        ex x be Element of F_Complex st x is_a_root_of np

        proof

          take z0 = ( - (np . 0 ));

          ( eval (np,z0)) = ((np . 0 ) + z0) by A64, Th47

          .= ( 0. F_Complex ) by RLVECT_1: 5;

          hence thesis;

        end;

        then np is with_roots;

        hence thesis by A58, Th60;

      end;

    end;

    registration

      cluster F_Complex -> algebraic-closed;

      coherence by Th74;

    end

    registration

      cluster algebraic-closed add-associative right_zeroed right_complementable Abelian commutative associative distributive almost_left_invertible non degenerated for well-unital non empty doubleLoopStr;

      existence

      proof

        take F_Complex ;

        thus thesis;

      end;

    end