polynom4.miz



    begin

    theorem :: POLYNOM4:1

    for D be non empty set holds for p be FinSequence of D holds for n be Element of NAT st 1 <= n & n <= ( len p) holds p = (((p | (n -' 1)) ^ <*(p . n)*>) ^ (p /^ n)) by FINSEQ_5: 84;

    

     Lm1: for R be left_zeroed right_add-cancelable right-distributive non empty doubleLoopStr, a be Element of R holds (a * ( 0. R)) = ( 0. R)

    proof

      let R be left_zeroed right_add-cancelable right-distributive non empty doubleLoopStr, a be Element of R;

      (a * ( 0. R)) = (a * (( 0. R) + ( 0. R))) by ALGSTR_1:def 2

      .= ((a * ( 0. R)) + (a * ( 0. R))) by VECTSP_1:def 2;

      then ((a * ( 0. R)) + (a * ( 0. R))) = (( 0. R) + (a * ( 0. R))) by ALGSTR_1:def 2;

      hence thesis by ALGSTR_0:def 4;

    end;

    registration

      cluster almost_left_invertible -> domRing-like for left_zeroed right_add-cancelable right-distributive well-unital associative non empty doubleLoopStr;

      coherence

      proof

        let L be left_zeroed right_add-cancelable right-distributive well-unital associative non empty doubleLoopStr;

        assume

         A1: L is almost_left_invertible;

        now

          let x,y be Element of L;

          assume

           A2: (x * y) = ( 0. L);

          thus x = ( 0. L) or y = ( 0. L)

          proof

            assume x <> ( 0. L);

            then

            consider z be Element of L such that

             A3: (z * x) = ( 1. L) by A1;

            (z * ( 0. L)) = (( 1. L) * y) by A2, A3, GROUP_1:def 3

            .= y;

            hence thesis by Lm1;

          end;

        end;

        hence thesis by VECTSP_2:def 1;

      end;

    end

    registration

      cluster strict Abelian add-associative right_zeroed right_complementable associative commutative distributive unital domRing-like almost_left_invertible non degenerated for non empty doubleLoopStr;

      existence

      proof

        set F = the non degenerated strict Field;

        take F;

        thus thesis;

      end;

    end

    begin

    theorem :: POLYNOM4:2

    

     Th2: 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;

      now

        let i be Element of NAT ;

        consider r be FinSequence of the carrier of L such that ( len r) = (i + 1) and

         A1: ((( 0_. L) *' p) . i) = ( Sum r) and

         A2: for k be Element of NAT st k in ( dom r) holds (r . k) = ((( 0_. L) . (k -' 1)) * (p . ((i + 1) -' k))) by POLYNOM3:def 9;

        now

          let k be Element of NAT ;

          assume k in ( dom r);

          

          hence (r . k) = ((( 0_. L) . (k -' 1)) * (p . ((i + 1) -' k))) by A2

          .= (( 0. L) * (p . ((i + 1) -' k))) by FUNCOP_1: 7

          .= ( 0. L);

        end;

        

        hence ((( 0_. L) *' p) . i) = ( 0. L) by A1, POLYNOM3: 1

        .= (( 0_. L) . i) by FUNCOP_1: 7;

      end;

      hence thesis by FUNCT_2: 63;

    end;

    theorem :: POLYNOM4:3

    

     Th3: for L be non empty ZeroStr holds ( len ( 0_. L)) = 0

    proof

      let L be non empty ZeroStr;

      for i be Nat holds i >= 0 implies (( 0_. L) . i) = ( 0. L) by FUNCOP_1: 7, ORDINAL1:def 12;

      then 0 is_at_least_length_of ( 0_. L);

      hence thesis by ALGSEQ_1:def 3;

    end;

    theorem :: POLYNOM4:4

    

     Th4: for L be non degenerated non empty multLoopStr_0 holds ( len ( 1_. L)) = 1

    proof

      let L be non degenerated non empty multLoopStr_0;

       A1:

      now

        let i be Nat;

        assume that

         A2: i is_at_least_length_of ( 1_. L) and

         A3: ( 0 + 1) > i;

         0 >= i by A3, NAT_1: 13;

        then (( 1_. L) . 0 ) = ( 0. L) by A2;

        hence contradiction by POLYNOM3: 30;

      end;

      for i be Nat st i >= 1 holds (( 1_. L) . i) = ( 0. L) by POLYNOM3: 30;

      then 1 is_at_least_length_of ( 1_. L);

      hence thesis by A1, ALGSEQ_1:def 3;

    end;

    theorem :: POLYNOM4:5

    

     Th5: for L be non empty ZeroStr holds for p be Polynomial of L st ( len p) = 0 holds p = ( 0_. L)

    proof

      let L be non empty ZeroStr;

      let p be Polynomial of L;

      assume ( len p) = 0 ;

      then

       A1: 0 is_at_least_length_of p by ALGSEQ_1:def 3;

       A2:

      now

        let x be object;

        assume x in ( dom p);

        then

        reconsider i = x as Element of NAT by NORMSP_1: 12;

        i >= 0 ;

        hence (p . x) = ( 0. L) by A1;

      end;

      ( dom p) = NAT by NORMSP_1: 12;

      hence thesis by A2, FUNCOP_1: 11;

    end;

    theorem :: POLYNOM4:6

    

     Th6: for L be right_zeroed non empty addLoopStr holds for p,q be Polynomial of L holds for n be Element of NAT st n >= ( len p) & n >= ( len q) holds n >= ( len (p + q))

    proof

      let L be right_zeroed non empty addLoopStr;

      let p,q be Polynomial of L;

      let n be Element of NAT ;

      assume n >= ( len p) & n >= ( len q);

      then n is_at_least_length_of p & n is_at_least_length_of q by POLYNOM3: 23;

      then n is_at_least_length_of (p + q) by POLYNOM3: 24;

      hence thesis by POLYNOM3: 23;

    end;

    theorem :: POLYNOM4:7

    

     Th7: for L be add-associative right_zeroed right_complementable non empty addLoopStr holds for p,q be Polynomial of L st ( len p) <> ( len q) holds ( len (p + q)) = ( max (( len p),( len q)))

    proof

      let L be add-associative right_zeroed right_complementable non empty addLoopStr;

      let p,q be Polynomial of L;

      assume

       A1: ( len p) <> ( len q);

      per cases by A1, XXREAL_0: 1;

        suppose

         A2: ( len p) < ( len q);

        then ( len q) >= (( len p) + 1) by NAT_1: 13;

        then (( len q) - 1) >= ( len p) by XREAL_1: 19;

        then

         A3: (( len q) -' 1) >= ( len p) by XREAL_0:def 2;

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

        then

         A4: ( len q) = ((( len q) -' 1) + 1) by XREAL_1: 235;

        

         A5: ((p + q) . (( len q) -' 1)) = ((p . (( len q) -' 1)) + (q . (( len q) -' 1))) by NORMSP_1:def 2

        .= (( 0. L) + (q . (( len q) -' 1))) by A3, ALGSEQ_1: 8

        .= (q . (( len q) -' 1)) by RLVECT_1: 4;

        

         A6: ( len (p + q)) >= ( len q)

        proof

          assume ( len (p + q)) < ( len q);

          then (( len (p + q)) + 1) <= ( len q) by NAT_1: 13;

          then ( len (p + q)) <= (( len q) - 1) by XREAL_1: 19;

          then ( len (p + q)) <= (( len q) -' 1) by XREAL_0:def 2;

          then ((p + q) . (( len q) -' 1)) = ( 0. L) by ALGSEQ_1: 8;

          hence contradiction by A5, A4, ALGSEQ_1: 10;

        end;

        ( max (( len p),( len q))) = ( len q) & ( len (p + q)) <= ( len q) by A2, Th6, XXREAL_0:def 10;

        hence thesis by A6, XXREAL_0: 1;

      end;

        suppose

         A7: ( len p) > ( len q);

        then ( len p) >= (( len q) + 1) by NAT_1: 13;

        then (( len p) - 1) >= ( len q) by XREAL_1: 19;

        then

         A8: (( len p) -' 1) >= ( len q) by XREAL_0:def 2;

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

        then

         A9: ( len p) = ((( len p) -' 1) + 1) by XREAL_1: 235;

        

         A10: ((p + q) . (( len p) -' 1)) = ((p . (( len p) -' 1)) + (q . (( len p) -' 1))) by NORMSP_1:def 2

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

        .= (p . (( len p) -' 1)) by RLVECT_1: 4;

        

         A11: ( len (p + q)) >= ( len p)

        proof

          assume ( len (p + q)) < ( len p);

          then (( len (p + q)) + 1) <= ( len p) by NAT_1: 13;

          then ( len (p + q)) <= (( len p) - 1) by XREAL_1: 19;

          then ( len (p + q)) <= (( len p) -' 1) by XREAL_0:def 2;

          then ((p + q) . (( len p) -' 1)) = ( 0. L) by ALGSEQ_1: 8;

          hence contradiction by A10, A9, ALGSEQ_1: 10;

        end;

        ( max (( len p),( len q))) = ( len p) & ( len (p + q)) <= ( len p) by A7, Th6, XXREAL_0:def 10;

        hence thesis by A11, XXREAL_0: 1;

      end;

    end;

    theorem :: POLYNOM4:8

    

     Th8: for L be add-associative right_zeroed right_complementable non empty addLoopStr holds for p be Polynomial of L holds ( len ( - p)) = ( len p)

    proof

      let L be add-associative right_zeroed right_complementable non empty addLoopStr;

      let p be Polynomial of L;

       A1:

      now

        let n be Nat;

        assume

         A2: n is_at_least_length_of ( - p);

        n is_at_least_length_of p

        proof

          let i be Nat;

          assume i >= n;

          then i in NAT & (( - p) . i) = ( 0. L) by A2, ORDINAL1:def 12;

          then ( - (p . i)) = ( 0. L) by BHSP_1: 44;

          hence (p . i) = ( 0. L) by VECTSP_2: 3;

        end;

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

      end;

      ( len p) is_at_least_length_of ( - p)

      proof

        let i be Nat;

        assume

         A3: i >= ( len p);

        

        thus (( - p) . i) = ( - (p . i)) by BHSP_1: 44

        .= ( - ( 0. L)) by A3, ALGSEQ_1: 8

        .= ( 0. L) by RLVECT_1: 12;

      end;

      hence thesis by A1, ALGSEQ_1:def 3;

    end;

    theorem :: POLYNOM4:9

    for L be add-associative right_zeroed right_complementable non empty addLoopStr holds for p,q be Polynomial of L holds for n be Element of NAT st n >= ( len p) & n >= ( len q) holds n >= ( len (p - q))

    proof

      let L be add-associative right_zeroed right_complementable non empty addLoopStr;

      let p,q be Polynomial of L;

      ( len q) = ( len ( - q)) by Th8;

      hence thesis by Th6;

    end;

    theorem :: POLYNOM4:10

    for L be add-associative right_zeroed right_complementable distributive associative left_unital non empty doubleLoopStr, p,q be Polynomial of L st ((p . (( len p) -' 1)) * (q . (( len q) -' 1))) <> ( 0. L) holds ( len (p *' q)) = ((( len p) + ( len q)) - 1)

    proof

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

      let p,q be Polynomial of L;

      

       A1: ((( len p) + ( len q)) -' 1) is_at_least_length_of (p *' q)

      proof

        let i be Nat;

        i in NAT by ORDINAL1:def 12;

        then

        consider r be FinSequence of the carrier of L such that

         A2: ( len r) = (i + 1) and

         A3: ((p *' q) . i) = ( Sum r) and

         A4: for k be Element of NAT st k in ( dom r) holds (r . k) = ((p . (k -' 1)) * (q . ((i + 1) -' k))) by POLYNOM3:def 9;

        assume i >= ((( len p) + ( len q)) -' 1);

        then i >= ((( len p) + ( len q)) - 1) by XREAL_0:def 2;

        then (i + 1) >= (( len p) + ( len q)) by XREAL_1: 20;

        then ( len p) <= ((i + 1) - ( len q)) by XREAL_1: 19;

        then

         A5: ( - ( len p)) >= ( - ((i + 1) - ( len q))) by XREAL_1: 24;

        now

          let k be Element of NAT ;

          assume

           A6: k in ( dom r);

          then

           A7: (r . k) = ((p . (k -' 1)) * (q . ((i + 1) -' k))) by A4;

          k in ( Seg ( len r)) by A6, FINSEQ_1:def 3;

          then k <= (i + 1) by A2, FINSEQ_1: 1;

          then

           A8: ((i + 1) - k) >= 0 by XREAL_1: 48;

          per cases ;

            suppose (k -' 1) < ( len p);

            then (k - 1) < ( len p) by XREAL_0:def 2;

            then ( - (k - 1)) > ( - ( len p)) by XREAL_1: 24;

            then (1 - k) > (( len q) - (i + 1)) by A5, XXREAL_0: 2;

            then ((i + 1) + (1 - k)) > ( len q) by XREAL_1: 19;

            then (((i + 1) - k) + 1) > ( len q);

            then (((i + 1) -' k) + 1) > ( len q) by A8, XREAL_0:def 2;

            then ((i + 1) -' k) >= ( len q) by NAT_1: 13;

            then (q . ((i + 1) -' k)) = ( 0. L) by ALGSEQ_1: 8;

            hence (r . k) = ( 0. L) by A7;

          end;

            suppose (k -' 1) >= ( len p);

            then (p . (k -' 1)) = ( 0. L) by ALGSEQ_1: 8;

            hence (r . k) = ( 0. L) by A7;

          end;

        end;

        hence ((p *' q) . i) = ( 0. L) by A3, POLYNOM3: 1;

      end;

      assume

       A9: ((p . (( len p) -' 1)) * (q . (( len q) -' 1))) <> ( 0. L);

       A10:

      now

        assume ( len p) <= 0 ;

        then ( len p) = 0 ;

        then p = ( 0_. L) by Th5;

        then (p . (( len p) -' 1)) = ( 0. L) by FUNCOP_1: 7;

        hence contradiction by A9;

      end;

       A11:

      now

        assume ( len q) <= 0 ;

        then ( len q) = 0 ;

        then q = ( 0_. L) by Th5;

        then (q . (( len q) -' 1)) = ( 0. L) by FUNCOP_1: 7;

        hence contradiction by A9;

      end;

      then (( len p) + ( len q)) >= ( 0 + 1) by NAT_1: 13;

      then

       A12: ((( len p) + ( len q)) - 1) >= (1 - 1) by XREAL_1: 9;

      now

        let n be Nat;

        assume that

         A13: n is_at_least_length_of (p *' q) and

         A14: ((( len p) + ( len q)) -' 1) > n;

        ((( len p) + ( len q)) -' 1) >= (n + 1) by A14, NAT_1: 13;

        then

         A15: (((( len p) + ( len q)) -' 1) - 1) >= n by XREAL_1: 19;

        

         A16: (((( len p) + ( len q)) -' 1) - 1) = (((( len p) + ( len q)) - 1) - 1) by A12, XREAL_0:def 2;

        

         A17: ( len q) >= ( 0 + 1) by A11, NAT_1: 13;

        then

         A18: (( len q) - 1) >= 0 by XREAL_1: 19;

        (( len p) + ( len q)) > ( 0 + 1) by A10, A17, XREAL_1: 8;

        then (( len p) + ( len q)) >= (1 + 1) by NAT_1: 13;

        then

         A19: ((( len p) + ( len q)) - 2) >= (2 - 2) by XREAL_1: 9;

        then

         A20: ((( len p) + ( len q)) -' 2) = ((( len p) + ( len q)) - (1 + 1)) by XREAL_0:def 2;

        consider r be FinSequence of the carrier of L such that

         A21: ( len r) = (((( len p) + ( len q)) -' 2) + 1) and

         A22: ((p *' q) . ((( len p) + ( len q)) -' 2)) = ( Sum r) and

         A23: for k be Element of NAT st k in ( dom r) holds (r . k) = ((p . (k -' 1)) * (q . ((((( len p) + ( len q)) -' 2) + 1) -' k))) by POLYNOM3:def 9;

        

         A24: ( len r) = ((((( len p) + ( len q)) - 1) + ( - 1)) + 1) by A21, A19, XREAL_0:def 2

        .= (( len p) + (( len q) - 1));

        

        then

         A25: ((((( len p) + ( len q)) -' 2) + 1) -' ( len p)) = ((((( len p) + ( len q)) -' 2) + 1) - ( len p)) by A21, A18, XREAL_0:def 2

        .= (( len q) -' 1) by A21, A18, A24, XREAL_0:def 2;

        (( len r) - ( len p)) = (( len q) - 1) by A24;

        then

         A26: (( len p) + 0 ) <= ( len r) by A18, XREAL_1: 19;

        now

          let i be Element of NAT ;

          assume

           A27: i in ( dom (r /^ ( len p)));

          then

           A28: i in ( Seg ( len (r /^ ( len p)))) by FINSEQ_1:def 3;

          then

           A29: 1 <= i by FINSEQ_1: 1;

          (i + ( len p)) >= i by NAT_1: 11;

          then (i + ( len p)) >= ( 0 + 1) by A29, XXREAL_0: 2;

          then ((i + ( len p)) - 1) >= 0 by XREAL_1: 19;

          then

           A30: ((i + ( len p)) -' 1) = (( len p) + (i - 1)) by XREAL_0:def 2;

          ( 0 + 1) <= i by A28, FINSEQ_1: 1;

          then (i - 1) >= 0 by XREAL_1: 19;

          then

           A31: ((i + ( len p)) -' 1) >= (( len p) + 0 ) by A30, XREAL_1: 6;

          i <= ( len (r /^ ( len p))) by A28, FINSEQ_1: 1;

          then i <= (( len r) - ( len p)) by A26, RFINSEQ:def 1;

          then

           A32: (i + ( len p)) <= ( len r) by XREAL_1: 19;

          (i + ( len p)) >= i by NAT_1: 11;

          then (i + ( len p)) >= 1 by A29, XXREAL_0: 2;

          then (i + ( len p)) in ( Seg ( len r)) by A32, FINSEQ_1: 1;

          then

           A33: (i + ( len p)) in ( dom r) by FINSEQ_1:def 3;

          

          thus ((r /^ ( len p)) . i) = (r . (i + ( len p))) by A26, A27, RFINSEQ:def 1

          .= ((p . ((i + ( len p)) -' 1)) * (q . ((((( len p) + ( len q)) -' 2) + 1) -' (i + ( len p))))) by A23, A33

          .= (( 0. L) * (q . ((((( len p) + ( len q)) -' 2) + 1) -' (i + ( len p))))) by A31, ALGSEQ_1: 8

          .= ( 0. L);

        end;

        then

         A34: ( Sum (r /^ ( len p))) = ( 0. L) by POLYNOM3: 1;

        

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

        then ( len p) in ( Seg ( len r)) by A26, FINSEQ_1: 1;

        then

         A36: ( len p) in ( dom r) by FINSEQ_1:def 3;

        now

          

           A37: (( len p) - 1) >= (1 - 1) by A35, XREAL_1: 9;

          

           A38: (((( len p) + ( len q)) -' 2) + 1) = ((( len p) - 1) + ( len q)) by A21, A24

          .= ((( len p) -' 1) + ( len q)) by A37, XREAL_0:def 2;

          

           A39: ( dom (r | (( len p) -' 1))) c= ( dom r) by FINSEQ_5: 18;

          let i be Element of NAT ;

          assume

           A40: i in ( dom (r | (( len p) -' 1)));

          ( len p) < (( len r) + 1) by A26, NAT_1: 13;

          then (( len p) - 1) < ((( len r) + 1) - 1) by XREAL_1: 9;

          then (( len p) -' 1) < ( len r) by A37, XREAL_0:def 2;

          then ( len (r | (( len p) -' 1))) = (( len p) -' 1) by FINSEQ_1: 59;

          then i in ( Seg (( len p) -' 1)) by A40, FINSEQ_1:def 3;

          then i <= (( len p) -' 1) by FINSEQ_1: 1;

          then (i + ( len q)) <= ((( len p) -' 1) + ( len q)) by XREAL_1: 6;

          then ( len q) <= ((((( len p) + ( len q)) -' 2) + 1) - i) by A38, XREAL_1: 19;

          then

           A41: ( len q) <= ((((( len p) + ( len q)) -' 2) + 1) -' i) by XREAL_0:def 2;

          

          thus ((r | (( len p) -' 1)) . i) = ((r | (( len p) -' 1)) /. i) by A40, PARTFUN1:def 6

          .= (r /. i) by A40, FINSEQ_4: 70

          .= (r . i) by A40, A39, PARTFUN1:def 6

          .= ((p . (i -' 1)) * (q . ((((( len p) + ( len q)) -' 2) + 1) -' i))) by A23, A40, A39

          .= ((p . (i -' 1)) * ( 0. L)) by A41, ALGSEQ_1: 8

          .= ( 0. L);

        end;

        then

         A42: ( Sum (r | (( len p) -' 1))) = ( 0. L) by POLYNOM3: 1;

        r = (((r | (( len p) -' 1)) ^ <*(r . ( len p))*>) ^ (r /^ ( len p))) by A26, A35, FINSEQ_5: 84;

        then r = (((r | (( len p) -' 1)) ^ <*(r /. ( len p))*>) ^ (r /^ ( len p))) by A26, A35, FINSEQ_4: 15;

        

        then ( Sum r) = (( Sum ((r | (( len p) -' 1)) ^ <*(r /. ( len p))*>)) + ( Sum (r /^ ( len p)))) by RLVECT_1: 41

        .= ((( Sum (r | (( len p) -' 1))) + ( Sum <*(r /. ( len p))*>)) + ( Sum (r /^ ( len p)))) by RLVECT_1: 41;

        

        then ( Sum r) = (( Sum <*(r /. ( len p))*>) + ( 0. L)) by A42, A34, RLVECT_1: 4

        .= ( Sum <*(r /. ( len p))*>) by RLVECT_1: 4

        .= (r /. ( len p)) by RLVECT_1: 44

        .= (r . ( len p)) by A36, PARTFUN1:def 6

        .= ((p . (( len p) -' 1)) * (q . (( len q) -' 1))) by A23, A36, A25;

        hence contradiction by A9, A13, A22, A16, A20, A15;

      end;

      then ( len (p *' q)) = ((( len p) + ( len q)) -' 1) by A1, ALGSEQ_1:def 3;

      hence thesis by A12, XREAL_0:def 2;

    end;

    begin

    definition

      let L be non empty ZeroStr;

      let p be Polynomial of L;

      :: POLYNOM4:def1

      func Leading-Monomial (p) -> sequence of L means

      : Def1: (it . (( len p) -' 1)) = (p . (( len p) -' 1)) & for n be Element of NAT st n <> (( len p) -' 1) holds (it . n) = ( 0. L);

      existence

      proof

        reconsider P = (( 0_. L) +* ((( len p) -' 1),(p . (( len p) -' 1)))) as sequence of L;

        take P;

        (( len p) -' 1) in NAT ;

        then (( len p) -' 1) in ( dom ( 0_. L)) by NORMSP_1: 12;

        hence (P . (( len p) -' 1)) = (p . (( len p) -' 1)) by FUNCT_7: 31;

        let n be Element of NAT ;

        assume n <> (( len p) -' 1);

        

        hence (P . n) = (( 0_. L) . n) by FUNCT_7: 32

        .= ( 0. L) by FUNCOP_1: 7;

      end;

      uniqueness

      proof

        let P1,P2 be sequence of L such that

         A1: (P1 . (( len p) -' 1)) = (p . (( len p) -' 1)) and

         A2: for n be Element of NAT st n <> (( len p) -' 1) holds (P1 . n) = ( 0. L) and

         A3: (P2 . (( len p) -' 1)) = (p . (( len p) -' 1)) and

         A4: for n be Element of NAT st n <> (( len p) -' 1) holds (P2 . n) = ( 0. L);

        now

          let i be Element of NAT ;

          per cases ;

            suppose i = (( len p) -' 1);

            hence (P1 . i) = (P2 . i) by A1, A3;

          end;

            suppose

             A5: i <> (( len p) -' 1);

            

            hence (P1 . i) = ( 0. L) by A2

            .= (P2 . i) by A4, A5;

          end;

        end;

        hence P1 = P2 by FUNCT_2: 63;

      end;

    end

    theorem :: POLYNOM4:11

    

     Th11: for L be non empty ZeroStr holds for p be Polynomial of L holds ( Leading-Monomial p) = (( 0_. L) +* ((( len p) -' 1),(p . (( len p) -' 1))))

    proof

      let L be non empty ZeroStr;

      let p be Polynomial of L;

      reconsider P = (( 0_. L) +* ((( len p) -' 1),(p . (( len p) -' 1)))) as sequence of L;

       A1:

      now

        let n be Element of NAT ;

        assume n <> (( len p) -' 1);

        

        hence (P . n) = (( 0_. L) . n) by FUNCT_7: 32

        .= ( 0. L) by FUNCOP_1: 7;

      end;

      (( len p) -' 1) in NAT ;

      then (( len p) -' 1) in ( dom ( 0_. L)) by NORMSP_1: 12;

      then (P . (( len p) -' 1)) = (p . (( len p) -' 1)) by FUNCT_7: 31;

      hence thesis by A1, Def1;

    end;

    registration

      let L be non empty ZeroStr;

      let p be Polynomial of L;

      cluster ( Leading-Monomial p) -> finite-Support;

      coherence

      proof

        take ( len p);

        let i be Nat;

        

         A1: i in NAT by ORDINAL1:def 12;

        assume i >= ( len p);

        then (i + 1) > ( len p) by NAT_1: 13;

        then

         A2: ((i + 1) - 1) > (( len p) - 1) by XREAL_1: 9;

        

         A3: ( Leading-Monomial p) = (( 0_. L) +* ((( len p) -' 1),(p . (( len p) -' 1)))) by Th11;

        per cases ;

          suppose ( len p) > 0 ;

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

          then (( len p) - 1) >= (( 0 + 1) - 1) by XREAL_1: 9;

          then i <> (( len p) -' 1) by A2, XREAL_0:def 2;

          

          hence (( Leading-Monomial p) . i) = (( 0_. L) . i) by A3, FUNCT_7: 32

          .= ( 0. L) by A1, FUNCOP_1: 7;

        end;

          suppose

           A4: ( len p) = 0 ;

          then

           A5: (( len p) -' 1) = 0 by NAT_2: 8;

           0 in NAT ;

          then

           A6: 0 in ( dom ( 0_. L)) by NORMSP_1: 12;

          now

            per cases ;

              suppose i > 0 ;

              

              hence (( Leading-Monomial p) . i) = (( 0_. L) . i) by A3, A5, FUNCT_7: 32

              .= ( 0. L) by A1, FUNCOP_1: 7;

            end;

              suppose i = 0 ;

              

              hence (( Leading-Monomial p) . i) = (p . 0 ) by A3, A5, A6, FUNCT_7: 31

              .= (( 0_. L) . 0 ) by A4, Th5

              .= ( 0. L) by FUNCOP_1: 7;

            end;

          end;

          hence thesis;

        end;

      end;

    end

    theorem :: POLYNOM4:12

    

     Th12: for L be non empty ZeroStr holds for p be Polynomial of L st ( len p) = 0 holds ( Leading-Monomial p) = ( 0_. L)

    proof

      let L be non empty ZeroStr;

      let p be Polynomial of L;

      assume ( len p) = 0 ;

      then

       A1: (( 0_. L) . (( len p) -' 1)) = (p . (( len p) -' 1)) by Th5;

      for n be Element of NAT st n <> (( len p) -' 1) holds (( 0_. L) . n) = ( 0. L) by FUNCOP_1: 7;

      hence thesis by A1, Def1;

    end;

    theorem :: POLYNOM4:13

    for L be non empty ZeroStr holds ( Leading-Monomial ( 0_. L)) = ( 0_. L)

    proof

      let L be non empty ZeroStr;

      ( len ( 0_. L)) = 0 by Th3;

      hence thesis by Th12;

    end;

    theorem :: POLYNOM4:14

    for L be non degenerated non empty multLoopStr_0 holds ( Leading-Monomial ( 1_. L)) = ( 1_. L)

    proof

      let L be non degenerated non empty multLoopStr_0;

       A1:

      now

        let n be Element of NAT ;

        assume n <> (( len ( 1_. L)) -' 1);

        then n <> (1 -' 1) by Th4;

        then n <> 0 by XREAL_1: 232;

        hence (( 1_. L) . n) = ( 0. L) by POLYNOM3: 30;

      end;

      (( 1_. L) . (( len ( 1_. L)) -' 1)) = (( 1_. L) . (( len ( 1_. L)) -' 1));

      hence thesis by A1, Def1;

    end;

    theorem :: POLYNOM4:15

    

     Th15: for L be non empty ZeroStr holds for p be Polynomial of L holds ( len ( Leading-Monomial p)) = ( len p)

    proof

      let L be non empty ZeroStr;

      let p be Polynomial of L;

      set r = ( Leading-Monomial p);

      

       A1: ( Leading-Monomial p) = (( 0_. L) +* ((( len p) -' 1),(p . (( len p) -' 1)))) by Th11;

      per cases ;

        suppose ( len p) > 0 ;

        then

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

        (( len p) -' 1) in NAT ;

        then

         A3: (( len p) -' 1) in ( dom ( 0_. L)) by NORMSP_1: 12;

         A4:

        now

          let m be Nat;

          assume

           A5: m is_at_least_length_of r;

          assume ( len p) > m;

          then ( len p) >= (m + 1) by NAT_1: 13;

          then (( len p) - 1) >= ((m + 1) - 1) by XREAL_1: 9;

          then (( len p) -' 1) >= m by XREAL_0:def 2;

          then (r . (( len p) -' 1)) = ( 0. L) by A5;

          then

           A6: (p . (( len p) -' 1)) = ( 0. L) by A1, A3, FUNCT_7: 31;

          ( len p) = ((( len p) -' 1) + 1) by A2, XREAL_1: 235;

          hence contradiction by A6, ALGSEQ_1: 10;

        end;

        

         A7: (( len p) - 1) >= 0 by A2, XREAL_1: 19;

        ( len p) is_at_least_length_of r

        proof

          let i be Nat;

          

           A8: i in NAT by ORDINAL1:def 12;

          assume i >= ( len p);

          then (i + 1) > ( len p) by NAT_1: 13;

          then ((i + 1) - 1) > (( len p) - 1) by XREAL_1: 9;

          then i <> (( len p) -' 1) by A7, XREAL_0:def 2;

          

          hence (r . i) = (( 0_. L) . i) by A1, FUNCT_7: 32

          .= ( 0. L) by A8, FUNCOP_1: 7;

        end;

        hence thesis by A4, ALGSEQ_1:def 3;

      end;

        suppose

         A9: ( len p) = 0 ;

        

        hence ( len ( Leading-Monomial p)) = ( len ( 0_. L)) by Th12

        .= ( len p) by A9, Th5;

      end;

    end;

    theorem :: POLYNOM4:16

    

     Th16: for L be add-associative right_zeroed right_complementable non empty addLoopStr holds for p be Polynomial of L st ( len p) <> 0 holds ex q be Polynomial of L st ( len q) < ( len p) & p = (q + ( Leading-Monomial p)) & for n be Element of NAT st n < (( len p) - 1) holds (q . n) = (p . n)

    proof

      let L be add-associative right_zeroed right_complementable non empty addLoopStr;

      let p be Polynomial of L;

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

      consider q be Polynomial of L such that

       A1: ( len q) <= (( len p) -' 1) and

       A2: for n be Element of NAT st n < (( len p) -' 1) holds (q . n) = F(n) from POLYNOM3:sch 2;

      assume ( len p) <> 0 ;

      then

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

      take q;

      ( len q) < ((( len p) -' 1) + 1) by A1, NAT_1: 13;

      hence

       A4: ( len q) < ( len p) by A3, XREAL_1: 235;

       A5:

      now

        let k be Nat;

        

         A6: k in NAT by ORDINAL1:def 12;

        assume k < ( len p);

        then (k + 1) <= ( len p) by NAT_1: 13;

        then

         A7: ((k + 1) - 1) <= (( len p) - 1) by XREAL_1: 9;

        per cases by A7, XXREAL_0: 1;

          suppose k < (( len p) - 1);

          then

           A8: k < (( len p) -' 1) by XREAL_0:def 2;

          

          thus ((q + ( Leading-Monomial p)) . k) = ((q . k) + (( Leading-Monomial p) . k)) by NORMSP_1:def 2

          .= ((p . k) + (( Leading-Monomial p) . k)) by A2, A6, A8

          .= ((p . k) + ( 0. L)) by A6, A8, Def1

          .= (p . k) by RLVECT_1:def 4;

        end;

          suppose k = (( len p) - 1);

          then

           A9: k = (( len p) -' 1) by XREAL_0:def 2;

          

          thus ((q + ( Leading-Monomial p)) . k) = ((q . k) + (( Leading-Monomial p) . k)) by NORMSP_1:def 2

          .= (( 0. L) + (( Leading-Monomial p) . k)) by A1, A9, ALGSEQ_1: 8

          .= (( Leading-Monomial p) . k) by RLVECT_1: 4

          .= (p . k) by A9, Def1;

        end;

      end;

      

       A10: ( len ( Leading-Monomial p)) = ( len p) by Th15;

      

      then ( len (q + ( Leading-Monomial p))) = ( max (( len q),( len ( Leading-Monomial p)))) by A4, Th7

      .= ( len p) by A4, A10, XXREAL_0:def 10;

      hence p = (q + ( Leading-Monomial p)) by A5, ALGSEQ_1: 12;

      let n be Element of NAT ;

      assume n < (( len p) - 1);

      then n < (( len p) -' 1) by XREAL_0:def 2;

      hence thesis by A2;

    end;

    begin

    definition

      let L be unital non empty doubleLoopStr;

      let p be Polynomial of L;

      let x be Element of L;

      :: POLYNOM4:def2

      func eval (p,x) -> Element of L means

      : Def2: ex F be FinSequence of the carrier of 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)) * (( power L) . (x,(n -' 1))));

      existence

      proof

        deffunc G( Nat) = ((p . ($1 -' 1)) * (( power L) . (x,($1 -' 1))));

        consider F be FinSequence of the carrier of L such that

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

         A2: for n be Nat st n in ( dom F) holds (F . n) = G(n) from FINSEQ_2:sch 1;

        take y = ( Sum F);

        take F;

        thus y = ( Sum F) & ( len F) = ( len p) by A1;

        let n be Element of NAT ;

        assume n in ( dom F);

        hence thesis by A2;

      end;

      uniqueness

      proof

        let y1,y2 be Element of L;

        given F1 be FinSequence of the carrier of 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)) * (( power L) . (x,(n -' 1))));

        given F2 be FinSequence of the carrier of 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)) * (( power L) . (x,(n -' 1))));

        

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

        now

          let n be Nat;

          assume

           A10: n in ( dom F1);

          then

           A11: n in ( dom F2) by A7, A9, FINSEQ_1:def 3;

          

          thus (F1 . n) = ((p . (n -' 1)) * (( power L) . (x,(n -' 1)))) by A5, A10

          .= (F2 . n) by A8, A11;

        end;

        hence thesis by A3, A4, A6, A7, FINSEQ_2: 9;

      end;

    end

    theorem :: POLYNOM4:17

    

     Th17: for L be unital non empty doubleLoopStr holds for x be Element of L holds ( eval (( 0_. L),x)) = ( 0. L)

    proof

      let L be unital non empty doubleLoopStr;

      let x be Element of L;

      consider F be FinSequence of the carrier of L such that

       A1: ( eval (( 0_. L),x)) = ( Sum F) and

       A2: ( len F) = ( len ( 0_. L)) and for n be Element of NAT st n in ( dom F) holds (F . n) = ((( 0_. L) . (n -' 1)) * (( power L) . (x,(n -' 1)))) by Def2;

      ( len F) = 0 by A2, Th3;

      then F = ( <*> the carrier of L);

      hence thesis by A1, RLVECT_1: 43;

    end;

    theorem :: POLYNOM4:18

    

     Th18: for L be well-unital add-associative right_zeroed right_complementable associative non degenerated non empty doubleLoopStr holds for x be Element of L holds ( eval (( 1_. L),x)) = ( 1. L)

    proof

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

      let x be Element of L;

      consider F be FinSequence of the carrier of L such that

       A1: ( eval (( 1_. L),x)) = ( Sum F) and

       A2: ( len F) = ( len ( 1_. L)) and

       A3: for n be Element of NAT st n in ( dom F) holds (F . n) = ((( 1_. L) . (n -' 1)) * (( power L) . (x,(n -' 1)))) by Def2;

      

       A4: ( len F) = 1 by A2, Th4;

      then 1 in ( Seg ( len F)) by FINSEQ_1: 1;

      then 1 in ( dom F) by FINSEQ_1:def 3;

      

      then (F . 1) = ((( 1_. L) . (1 -' 1)) * (( power L) . (x,(1 -' 1)))) by A3

      .= ((( 1_. L) . 0 ) * (( power L) . (x,(1 -' 1)))) by XREAL_1: 232

      .= (( 1. L) * (( power L) . (x,(1 -' 1)))) by POLYNOM3: 30

      .= (( power L) . (x,(1 -' 1)))

      .= (( power L) . (x, 0 )) by XREAL_1: 232

      .= ( 1_ L) by GROUP_1:def 7

      .= ( 1. L);

      then F = <*( 1. L)*> by A4, FINSEQ_1: 40;

      hence thesis by A1, RLVECT_1: 44;

    end;

    theorem :: POLYNOM4:19

    

     Th19: for L be Abelian add-associative right_zeroed right_complementable unital left-distributive non empty doubleLoopStr holds for p,q be Polynomial of L holds for x be Element of L holds ( eval ((p + q),x)) = (( eval (p,x)) + ( eval (q,x)))

    proof

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

      let p,q be Polynomial of L;

      let x be Element of L;

      reconsider k = ( max (( len p),( len q))) as Element of NAT by ORDINAL1:def 12;

      

       A1: (k - ( len p)) >= 0 by XREAL_1: 48, XXREAL_0: 25;

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

      

       A5: ( len (F1 ^ ((k -' ( len F1)) |-> ( 0. L)))) = (( len p) + ( len ((k -' ( len p)) |-> ( 0. L)))) by A3, FINSEQ_1: 22

      .= (( len p) + (k -' ( len p))) by CARD_1:def 7

      .= (( len p) + (k - ( len p))) by A1, XREAL_0:def 2

      .= k;

      

       A6: (k - ( len q)) >= 0 by XREAL_1: 48, XXREAL_0: 25;

      k >= ( len p) & k >= ( len q) by XXREAL_0: 25;

      then

       A7: (k - ( len (p + q))) >= 0 by Th6, XREAL_1: 48;

      consider F3 be FinSequence of the carrier of L such that

       A8: ( eval ((p + q),x)) = ( Sum F3) and

       A9: ( len F3) = ( len (p + q)) and

       A10: for n be Element of NAT st n in ( dom F3) holds (F3 . n) = (((p + q) . (n -' 1)) * (( power L) . (x,(n -' 1)))) by Def2;

      

       A11: ( len (F3 ^ ((k -' ( len F3)) |-> ( 0. L)))) = (( len (p + q)) + ( len ((k -' ( len (p + q))) |-> ( 0. L)))) by A9, FINSEQ_1: 22

      .= (( len (p + q)) + (k -' ( len (p + q)))) by CARD_1:def 7

      .= (( len (p + q)) + (k - ( len (p + q)))) by A7, XREAL_0:def 2

      .= k;

      consider F2 be FinSequence of the carrier of L such that

       A12: ( eval (q,x)) = ( Sum F2) and

       A13: ( len F2) = ( len q) and

       A14: for n be Element of NAT st n in ( dom F2) holds (F2 . n) = ((q . (n -' 1)) * (( power L) . (x,(n -' 1)))) by Def2;

      ( len (F2 ^ ((k -' ( len F2)) |-> ( 0. L)))) = (( len q) + ( len ((k -' ( len q)) |-> ( 0. L)))) by A13, FINSEQ_1: 22

      .= (( len q) + (k -' ( len q))) by CARD_1:def 7

      .= (( len q) + (k - ( len q))) by A6, XREAL_0:def 2

      .= k;

      then

      reconsider G1 = (F1 ^ ((k -' ( len F1)) |-> ( 0. L))), G2 = (F2 ^ ((k -' ( len F2)) |-> ( 0. L))), G3 = (F3 ^ ((k -' ( len F3)) |-> ( 0. L))) as Element of (k -tuples_on the carrier of L) by A5, A11, FINSEQ_2: 92;

      now

        let n be Nat;

        assume

         A15: n in ( Seg k);

        then

         A16: ( 0 + 1) <= n by FINSEQ_1: 1;

        

         A17: n <= k by A15, FINSEQ_1: 1;

        per cases by XXREAL_0: 1;

          suppose

           A18: ( len p) > ( len q);

          then

           A19: k = ( len p) by XXREAL_0:def 10;

          then ( len (p + q)) = ( len p) by A18, Th7;

          then

           A20: n in ( dom F3) by A9, A15, A19, FINSEQ_1:def 3;

          

           A21: ( len G2) = k by CARD_1:def 7;

          then

           A22: n in ( dom G2) by A15, FINSEQ_1:def 3;

          then

           A23: (G2 /. n) = (G2 . n) by PARTFUN1:def 6;

          ( len G1) = k by CARD_1:def 7;

          then

           A24: n in ( dom G1) by A15, FINSEQ_1:def 3;

          then

           A25: (G1 /. n) = (G1 . n) by PARTFUN1:def 6;

          

           A26: n in ( dom F1) by A3, A15, A19, FINSEQ_1:def 3;

          

           A27: (G1 /. n) = (G1 . n) by A24, PARTFUN1:def 6

          .= (F1 . n) by A26, FINSEQ_1:def 7

          .= (F1 /. n) by A26, PARTFUN1:def 6;

          

           A28: (F1 . n) = ((p . (n -' 1)) * (( power L) . (x,(n -' 1)))) by A4, A26;

          now

            per cases ;

              suppose n <= ( len q);

              then n in ( Seg ( len q)) by A16, FINSEQ_1: 1;

              then

               A29: n in ( dom F2) by A13, FINSEQ_1:def 3;

              then

               A30: (F2 . n) = ((q . (n -' 1)) * (( power L) . (x,(n -' 1)))) by A14;

              

               A31: (G2 /. n) = (G2 . n) by A22, PARTFUN1:def 6

              .= (F2 . n) by A29, FINSEQ_1:def 7

              .= (F2 /. n) by A29, PARTFUN1:def 6;

              

              thus (G3 . n) = (F3 . n) by A20, FINSEQ_1:def 7

              .= (((p + q) . (n -' 1)) * (( power L) . (x,(n -' 1)))) by A10, A20

              .= (((p . (n -' 1)) + (q . (n -' 1))) * (( power L) . (x,(n -' 1)))) by NORMSP_1:def 2

              .= (((p . (n -' 1)) * (( power L) . (x,(n -' 1)))) + ((q . (n -' 1)) * (( power L) . (x,(n -' 1))))) by VECTSP_1:def 3

              .= (((p . (n -' 1)) * (( power L) . (x,(n -' 1)))) + (F2 /. n)) by A29, A30, PARTFUN1:def 6

              .= ((F1 /. n) + (F2 /. n)) by A26, A28, PARTFUN1:def 6

              .= ((G1 + G2) . n) by A15, A25, A23, A27, A31, FVSUM_1: 18;

            end;

              suppose

               A32: n > ( len q);

              then

               A33: n >= (( len q) + 1) by NAT_1: 13;

              then (n - 1) >= ( len q) by XREAL_1: 19;

              then

               A34: (n -' 1) >= ( len q) by XREAL_0:def 2;

              (n - ( len F2)) <= (k - ( len F2)) by A17, XREAL_1: 9;

              then

               A35: (n - ( len F2)) <= (k -' ( len F2)) by XREAL_0:def 2;

              

               A36: (n - ( len F2)) >= 1 by A13, A33, XREAL_1: 19;

              then (n - ( len F2)) = (n -' ( len F2)) by XREAL_0:def 2;

              then

               A37: (n - ( len F2)) in ( Seg (k -' ( len F2))) by A36, A35, FINSEQ_1: 1;

              n <= ( len G2) by A15, A21, FINSEQ_1: 1;

              

              then

               A38: (G2 /. n) = (((k -' ( len F2)) |-> ( 0. L)) . (n - ( len F2))) by A13, A23, A32, FINSEQ_1: 24

              .= ( 0. L) by A37, FUNCOP_1: 7;

              

              thus (G3 . n) = (F3 . n) by A20, FINSEQ_1:def 7

              .= (((p + q) . (n -' 1)) * (( power L) . (x,(n -' 1)))) by A10, A20

              .= (((p . (n -' 1)) + (q . (n -' 1))) * (( power L) . (x,(n -' 1)))) by NORMSP_1:def 2

              .= (((p . (n -' 1)) + ( 0. L)) * (( power L) . (x,(n -' 1)))) by A34, ALGSEQ_1: 8

              .= ((p . (n -' 1)) * (( power L) . (x,(n -' 1)))) by RLVECT_1: 4

              .= (F1 . n) by A4, A26

              .= (G1 /. n) by A26, A27, PARTFUN1:def 6

              .= ((G1 /. n) + ( 0. L)) by RLVECT_1: 4

              .= ((G1 + G2) . n) by A15, A25, A23, A38, FVSUM_1: 18;

            end;

          end;

          hence (G3 . n) = ((G1 + G2) . n);

        end;

          suppose

           A39: ( len p) < ( len q);

          then

           A40: k = ( len q) by XXREAL_0:def 10;

          then ( len (p + q)) = ( len q) by A39, Th7;

          then

           A41: n in ( dom F3) by A9, A15, A40, FINSEQ_1:def 3;

          

           A42: ( len G1) = k by CARD_1:def 7;

          then

           A43: n in ( dom G1) by A15, FINSEQ_1:def 3;

          then

           A44: (G1 /. n) = (G1 . n) by PARTFUN1:def 6;

          ( len G2) = k by CARD_1:def 7;

          then

           A45: n in ( dom G2) by A15, FINSEQ_1:def 3;

          then

           A46: (G2 /. n) = (G2 . n) by PARTFUN1:def 6;

          

           A47: n in ( dom F2) by A13, A15, A40, FINSEQ_1:def 3;

          

           A48: (G2 /. n) = (G2 . n) by A45, PARTFUN1:def 6

          .= (F2 . n) by A47, FINSEQ_1:def 7

          .= (F2 /. n) by A47, PARTFUN1:def 6;

          

           A49: (F2 . n) = ((q . (n -' 1)) * (( power L) . (x,(n -' 1)))) by A14, A47;

          now

            per cases ;

              suppose n <= ( len p);

              then n in ( Seg ( len p)) by A16, FINSEQ_1: 1;

              then

               A50: n in ( dom F1) by A3, FINSEQ_1:def 3;

              then

               A51: (F1 . n) = ((p . (n -' 1)) * (( power L) . (x,(n -' 1)))) by A4;

              

               A52: (G1 /. n) = (G1 . n) by A43, PARTFUN1:def 6

              .= (F1 . n) by A50, FINSEQ_1:def 7

              .= (F1 /. n) by A50, PARTFUN1:def 6;

              

              thus (G3 . n) = (F3 . n) by A41, FINSEQ_1:def 7

              .= (((p + q) . (n -' 1)) * (( power L) . (x,(n -' 1)))) by A10, A41

              .= (((p . (n -' 1)) + (q . (n -' 1))) * (( power L) . (x,(n -' 1)))) by NORMSP_1:def 2

              .= (((p . (n -' 1)) * (( power L) . (x,(n -' 1)))) + ((q . (n -' 1)) * (( power L) . (x,(n -' 1))))) by VECTSP_1:def 3

              .= ((F1 /. n) + ((q . (n -' 1)) * (( power L) . (x,(n -' 1))))) by A50, A51, PARTFUN1:def 6

              .= ((F1 /. n) + (F2 /. n)) by A47, A49, PARTFUN1:def 6

              .= ((G1 + G2) . n) by A15, A44, A46, A48, A52, FVSUM_1: 18;

            end;

              suppose

               A53: n > ( len p);

              then

               A54: n >= (( len p) + 1) by NAT_1: 13;

              then (n - 1) >= ( len p) by XREAL_1: 19;

              then

               A55: (n -' 1) >= ( len p) by XREAL_0:def 2;

              (n - ( len F1)) <= (k - ( len F1)) by A17, XREAL_1: 9;

              then

               A56: (n - ( len F1)) <= (k -' ( len F1)) by XREAL_0:def 2;

              

               A57: (n - ( len F1)) >= 1 by A3, A54, XREAL_1: 19;

              then (n - ( len F1)) = (n -' ( len F1)) by XREAL_0:def 2;

              then

               A58: (n - ( len F1)) in ( Seg (k -' ( len F1))) by A57, A56, FINSEQ_1: 1;

              n <= ( len G1) by A15, A42, FINSEQ_1: 1;

              

              then

               A59: (G1 /. n) = (((k -' ( len F1)) |-> ( 0. L)) . (n - ( len F1))) by A3, A44, A53, FINSEQ_1: 24

              .= ( 0. L) by A58, FUNCOP_1: 7;

              

              thus (G3 . n) = (F3 . n) by A41, FINSEQ_1:def 7

              .= (((p + q) . (n -' 1)) * (( power L) . (x,(n -' 1)))) by A10, A41

              .= (((p . (n -' 1)) + (q . (n -' 1))) * (( power L) . (x,(n -' 1)))) by NORMSP_1:def 2

              .= ((( 0. L) + (q . (n -' 1))) * (( power L) . (x,(n -' 1)))) by A55, ALGSEQ_1: 8

              .= ((q . (n -' 1)) * (( power L) . (x,(n -' 1)))) by RLVECT_1: 4

              .= (F2 . n) by A14, A47

              .= (G2 /. n) by A47, A48, PARTFUN1:def 6

              .= (( 0. L) + (G2 /. n)) by RLVECT_1: 4

              .= ((G1 + G2) . n) by A15, A44, A46, A59, FVSUM_1: 18;

            end;

          end;

          hence (G3 . n) = ((G1 + G2) . n);

        end;

          suppose

           A60: ( len p) = ( len q);

          ( len G2) = k by CARD_1:def 7;

          then

           A61: n in ( dom G2) by A15, FINSEQ_1:def 3;

          then

           A62: (G2 /. n) = (G2 . n) by PARTFUN1:def 6;

          ( len G1) = k by CARD_1:def 7;

          then

           A63: n in ( dom G1) by A15, FINSEQ_1:def 3;

          then

           A64: (G1 /. n) = (G1 . n) by PARTFUN1:def 6;

          

           A65: ( len G3) = k by CARD_1:def 7;

          

           A66: n in ( dom F2) by A13, A15, A60, FINSEQ_1:def 3;

          

           A67: n in ( dom F1) by A3, A15, A60, FINSEQ_1:def 3;

          then

           A68: (F1 . n) = ((p . (n -' 1)) * (( power L) . (x,(n -' 1)))) by A4;

          

           A69: (G1 /. n) = (G1 . n) by A63, PARTFUN1:def 6

          .= (F1 . n) by A67, FINSEQ_1:def 7

          .= (F1 /. n) by A67, PARTFUN1:def 6;

          now

            per cases ;

              suppose

               A70: n <= ( len (p + q));

              

               A71: n in ( dom F2) by A13, A15, A60, FINSEQ_1:def 3;

              then

               A72: (F2 . n) = ((q . (n -' 1)) * (( power L) . (x,(n -' 1)))) by A14;

              

               A73: (G2 /. n) = (G2 . n) by A61, PARTFUN1:def 6

              .= (F2 . n) by A71, FINSEQ_1:def 7

              .= (F2 /. n) by A71, PARTFUN1:def 6;

              n in ( Seg ( len (p + q))) by A16, A70, FINSEQ_1: 1;

              then

               A74: n in ( dom F3) by A9, FINSEQ_1:def 3;

              

              hence (G3 . n) = (F3 . n) by FINSEQ_1:def 7

              .= (((p + q) . (n -' 1)) * (( power L) . (x,(n -' 1)))) by A10, A74

              .= (((p . (n -' 1)) + (q . (n -' 1))) * (( power L) . (x,(n -' 1)))) by NORMSP_1:def 2

              .= (((p . (n -' 1)) * (( power L) . (x,(n -' 1)))) + ((q . (n -' 1)) * (( power L) . (x,(n -' 1))))) by VECTSP_1:def 3

              .= (((p . (n -' 1)) * (( power L) . (x,(n -' 1)))) + (F2 /. n)) by A71, A72, PARTFUN1:def 6

              .= ((F1 /. n) + (F2 /. n)) by A67, A68, PARTFUN1:def 6

              .= ((G1 + G2) . n) by A15, A64, A62, A69, A73, FVSUM_1: 18;

            end;

              suppose

               A75: n > ( len (p + q));

              then

               A76: n >= (( len (p + q)) + 1) by NAT_1: 13;

              then (n - 1) >= ((( len (p + q)) + 1) - 1) by XREAL_1: 9;

              then

               A77: (n -' 1) >= ( len (p + q)) by XREAL_0:def 2;

              (n - ( len F3)) <= (k - ( len F3)) by A17, XREAL_1: 9;

              then

               A78: (n - ( len F3)) <= (k -' ( len F3)) by XREAL_0:def 2;

              

               A79: (G2 . n) = (F2 . n) by A66, FINSEQ_1:def 7

              .= ((q . (n -' 1)) * (( power L) . (x,(n -' 1)))) by A14, A66;

              

               A80: (G1 . n) = (F1 . n) by A67, FINSEQ_1:def 7

              .= ((p . (n -' 1)) * (( power L) . (x,(n -' 1)))) by A4, A67;

              

               A81: (n - ( len F3)) >= 1 by A9, A76, XREAL_1: 19;

              then (n - ( len F3)) = (n -' ( len F3)) by XREAL_0:def 2;

              then

               A82: (n - ( len F3)) in ( Seg (k -' ( len F3))) by A81, A78, FINSEQ_1: 1;

              n <= ( len G3) by A15, A65, FINSEQ_1: 1;

              

              hence (G3 . n) = (((k -' ( len F3)) |-> ( 0. L)) . (n - ( len F3))) by A9, A75, FINSEQ_1: 24

              .= ( 0. L) by A82, FUNCOP_1: 7

              .= (( 0. L) * (( power L) . (x,(n -' 1))))

              .= (((p + q) . (n -' 1)) * (( power L) . (x,(n -' 1)))) by A77, ALGSEQ_1: 8

              .= (((p . (n -' 1)) + (q . (n -' 1))) * (( power L) . (x,(n -' 1)))) by NORMSP_1:def 2

              .= (((p . (n -' 1)) * (( power L) . (x,(n -' 1)))) + ((q . (n -' 1)) * (( power L) . (x,(n -' 1))))) by VECTSP_1:def 3

              .= ((G1 + G2) . n) by A15, A80, A79, FVSUM_1: 18;

            end;

          end;

          hence (G3 . n) = ((G1 + G2) . n);

        end;

      end;

      then

       A83: G3 = (G1 + G2) by FINSEQ_2: 119;

      

       A84: ( Sum G3) = (( Sum F3) + ( Sum ((k -' ( len F3)) |-> ( 0. L)))) by RLVECT_1: 41

      .= (( Sum F3) + ( 0. L)) by MATRIX_3: 11

      .= ( Sum F3) by RLVECT_1:def 4;

      

       A85: ( Sum G2) = (( Sum F2) + ( Sum ((k -' ( len F2)) |-> ( 0. L)))) by RLVECT_1: 41

      .= (( Sum F2) + ( 0. L)) by MATRIX_3: 11

      .= ( Sum F2) by RLVECT_1:def 4;

      ( Sum G1) = (( Sum F1) + ( Sum ((k -' ( len F1)) |-> ( 0. L)))) by RLVECT_1: 41

      .= (( Sum F1) + ( 0. L)) by MATRIX_3: 11

      .= ( Sum F1) by RLVECT_1:def 4;

      hence thesis by A2, A12, A8, A85, A84, A83, FVSUM_1: 76;

    end;

    theorem :: POLYNOM4:20

    

     Th20: for L be Abelian add-associative right_zeroed right_complementable unital distributive non empty doubleLoopStr holds for p be Polynomial of L holds for x be Element of L holds ( eval (( - p),x)) = ( - ( eval (p,x)))

    proof

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

      let p be Polynomial of L;

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

      consider F2 be FinSequence of the carrier of L such that

       A4: ( eval (( - p),x)) = ( Sum F2) and

       A5: ( len F2) = ( len ( - p)) and

       A6: for n be Element of NAT st n in ( dom F2) holds (F2 . n) = ((( - p) . (n -' 1)) * (( power L) . (x,(n -' 1)))) by Def2;

      ( len F2) = ( len F1) by A2, A5, Th8;

      then

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

      now

        let n be Nat;

        let v be Element of L;

        assume that

         A8: n in ( dom F2) and

         A9: v = (F1 . n);

        

        thus (F2 . n) = ((( - p) . (n -' 1)) * (( power L) . (x,(n -' 1)))) by A6, A8

        .= (( - (p . (n -' 1))) * (( power L) . (x,(n -' 1)))) by BHSP_1: 44

        .= ( - ((p . (n -' 1)) * (( power L) . (x,(n -' 1))))) by VECTSP_1: 9

        .= ( - v) by A3, A7, A8, A9;

      end;

      hence thesis by A1, A2, A4, A5, Th8, RLVECT_1: 40;

    end;

    theorem :: POLYNOM4:21

    for L be Abelian add-associative right_zeroed right_complementable unital distributive non empty doubleLoopStr holds for p,q be Polynomial of L holds for x be Element of L holds ( eval ((p - q),x)) = (( eval (p,x)) - ( eval (q,x)))

    proof

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

      let p,q be Polynomial of L;

      let x be Element of L;

      

      thus ( eval ((p - q),x)) = (( eval (p,x)) + ( eval (( - q),x))) by Th19

      .= (( eval (p,x)) + ( - ( eval (q,x)))) by Th20

      .= (( eval (p,x)) - ( eval (q,x))) by RLVECT_1:def 11;

    end;

    theorem :: POLYNOM4:22

    

     Th22: for L be add-associative right_zeroed right_complementable right_zeroed distributive unital non empty doubleLoopStr holds for p be Polynomial of L holds for x be Element of L holds ( eval (( Leading-Monomial p),x)) = ((p . (( len p) -' 1)) * (( power L) . (x,(( len p) -' 1))))

    proof

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

      let p be Polynomial of L;

      let x be Element of L;

      set LMp = ( Leading-Monomial p);

      consider F be FinSequence of the carrier of L such that

       A1: ( eval (LMp,x)) = ( Sum F) and

       A2: ( len F) = ( len LMp) and

       A3: for n be Element of NAT st n in ( dom F) holds (F . n) = ((LMp . (n -' 1)) * (( power L) . (x,(n -' 1)))) by Def2;

      

       A4: ( len F) = ( len p) by A2, Th15;

      per cases ;

        suppose ( len p) > 0 ;

        then

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

        then ( len p) in ( Seg ( len F)) by A4, FINSEQ_1: 1;

        then

         A6: ( len p) in ( dom F) by FINSEQ_1:def 3;

        

         A7: (( len p) - 1) >= 0 by A5, XREAL_1: 19;

        now

          

           A8: (( len p) -' 1) = (( len p) - 1) by A7, XREAL_0:def 2;

          let i be Element of NAT ;

          assume that

           A9: i in ( dom F) and

           A10: i <> ( len p);

          i in ( Seg ( len F)) by A9, FINSEQ_1:def 3;

          then i >= ( 0 + 1) by FINSEQ_1: 1;

          then (i - 1) >= 0 by XREAL_1: 19;

          then (i -' 1) = (i - 1) by XREAL_0:def 2;

          then

           A11: (i -' 1) <> (( len p) -' 1) by A10, A8;

          

          thus (F /. i) = (F . i) by A9, PARTFUN1:def 6

          .= ((LMp . (i -' 1)) * (( power L) . (x,(i -' 1)))) by A3, A9

          .= (( 0. L) * (( power L) . (x,(i -' 1)))) by A11, Def1

          .= ( 0. L);

        end;

        

        then ( Sum F) = (F /. ( len p)) by A6, POLYNOM2: 3

        .= (F . ( len p)) by A6, PARTFUN1:def 6

        .= ((LMp . (( len p) -' 1)) * (( power L) . (x,(( len p) -' 1)))) by A3, A6;

        hence thesis by A1, Def1;

      end;

        suppose

         A12: ( len p) = 0 ;

        then

         A13: p = ( 0_. L) by Th5;

        LMp = ( 0_. L) by A12, Th12;

        

        hence ( eval (( Leading-Monomial p),x)) = ( 0. L) by Th17

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

        .= ((p . (( len p) -' 1)) * (( power L) . (x,(( len p) -' 1)))) by A13, FUNCOP_1: 7;

      end;

    end;

    

     Lm2: for L be add-associative right_zeroed right_complementable unital distributive associative non empty doubleLoopStr holds for p,q be Polynomial of L st ( len p) > 0 & ( len q) > 0 holds for x be Element of L holds ( eval ((( Leading-Monomial p) *' ( Leading-Monomial q)),x)) = (((p . (( len p) -' 1)) * (q . (( len q) -' 1))) * (( power L) . (x,((( len p) + ( len q)) -' 2))))

    proof

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

      let p,q be Polynomial of L;

      assume that

       A1: ( len p) > 0 and

       A2: ( len q) > 0 ;

      

       A3: ( len q) >= ( 0 + 1) by A2, NAT_1: 13;

      then

       A4: (( len q) - 1) >= 0 by XREAL_1: 19;

      

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

      then (( len p) - 1) >= 0 by XREAL_1: 19;

      then

       A6: (( len p) - 1) = (( len p) -' 1) by XREAL_0:def 2;

      

       A7: (( len p) + ( len q)) >= ( 0 + (1 + 1)) by A5, A3, XREAL_1: 7;

      then

       A8: ((( len p) + ( len q)) - 1) >= 1 by XREAL_1: 19;

      then

      reconsider i1 = ((( len p) + ( len q)) - 1) as Element of NAT by INT_1: 3;

      

       A9: ((i1 -' 1) + 1) = i1 by A8, XREAL_1: 235;

      set LMp = ( Leading-Monomial p), LMq = ( Leading-Monomial q);

      let x be Element of L;

      consider F be FinSequence of the carrier of L such that

       A10: ( eval ((LMp *' LMq),x)) = ( Sum F) and

       A11: ( len F) = ( len (LMp *' LMq)) and

       A12: for n be Element of NAT st n in ( dom F) holds (F . n) = (((LMp *' LMq) . (n -' 1)) * (( power L) . (x,(n -' 1)))) by Def2;

      consider r be FinSequence of the carrier of L such that

       A13: ( len r) = ((i1 -' 1) + 1) and

       A14: ((LMp *' LMq) . (i1 -' 1)) = ( Sum r) and

       A15: for k be Element of NAT st k in ( dom r) holds (r . k) = ((LMp . (k -' 1)) * (LMq . (((i1 -' 1) + 1) -' k))) by POLYNOM3:def 9;

      (( len p) + 0 ) <= (( len p) + (( len q) - 1)) by A4, XREAL_1: 7;

      then ( len p) in ( Seg ( len r)) by A5, A9, A13, FINSEQ_1: 1;

      then

       A16: ( len p) in ( dom r) by FINSEQ_1:def 3;

      ((( len p) + (( len q) - 1)) - ( len p)) >= 0 by A3, XREAL_1: 19;

      

      then (i1 -' ( len p)) = ((( len p) + (( len q) - 1)) - ( len p)) by XREAL_0:def 2

      .= (( len q) -' 1) by A4, XREAL_0:def 2;

      then

       A17: (r . ( len p)) = ((LMp . (( len p) -' 1)) * (LMq . (( len q) -' 1))) by A9, A15, A16;

      now

        let i be Element of NAT ;

        assume that

         A18: i in ( dom r) and

         A19: i <> ( len p);

        i in ( Seg ( len r)) by A18, FINSEQ_1:def 3;

        then i >= ( 0 + 1) by FINSEQ_1: 1;

        then (i - 1) >= 0 by XREAL_1: 19;

        then (i -' 1) = (i - 1) by XREAL_0:def 2;

        then

         A20: (i -' 1) <> (( len p) -' 1) by A6, A19;

        

        thus (r /. i) = (r . i) by A18, PARTFUN1:def 6

        .= ((LMp . (i -' 1)) * (LMq . (((i1 -' 1) + 1) -' i))) by A15, A18

        .= (( 0. L) * (LMq . (((i1 -' 1) + 1) -' i))) by A20, Def1

        .= ( 0. L);

      end;

      

      then

       A21: ( Sum r) = (r /. ( len p)) by A16, POLYNOM2: 3

      .= ((LMp . (( len p) -' 1)) * (LMq . (( len q) -' 1))) by A16, A17, PARTFUN1:def 6

      .= ((p . (( len p) -' 1)) * (LMq . (( len q) -' 1))) by Def1

      .= ((p . (( len p) -' 1)) * (q . (( len q) -' 1))) by Def1;

      

       A22: (( len q) - 1) = (( len q) -' 1) by A4, XREAL_0:def 2;

       A23:

      now

        let i be Element of NAT ;

        assume that

         A24: i in ( dom F) and

         A25: i <> i1;

        consider r1 be FinSequence of the carrier of L such that

         A26: ( len r1) = ((i -' 1) + 1) and

         A27: ((LMp *' LMq) . (i -' 1)) = ( Sum r1) and

         A28: for k be Element of NAT st k in ( dom r1) holds (r1 . k) = ((LMp . (k -' 1)) * (LMq . (((i -' 1) + 1) -' k))) by POLYNOM3:def 9;

        i in ( Seg ( len F)) by A24, FINSEQ_1:def 3;

        then i >= 1 by FINSEQ_1: 1;

        then

         A29: ((i -' 1) + 1) = i by XREAL_1: 235;

         A30:

        now

          let j be Element of NAT ;

          assume

           A31: j in ( dom r1);

          then j in ( Seg ( len r1)) by FINSEQ_1:def 3;

          then j >= ( 0 + 1) by FINSEQ_1: 1;

          then (j - 1) >= 0 by XREAL_1: 19;

          then

           A32: (j -' 1) = (j - 1) by XREAL_0:def 2;

          per cases ;

            suppose j <> ( len p);

            then

             A33: (j -' 1) <> (( len p) -' 1) by A6, A32;

            

            thus (r1 . j) = ((LMp . (j -' 1)) * (LMq . (((i -' 1) + 1) -' j))) by A28, A31

            .= (( 0. L) * (LMq . (((i -' 1) + 1) -' j))) by A33, Def1

            .= ( 0. L);

          end;

            suppose

             A34: j = ( len p);

            j in ( Seg ( len r1)) by A31, FINSEQ_1:def 3;

            then i >= ( 0 + j) by A26, A29, FINSEQ_1: 1;

            then (i - j) >= 0 by XREAL_1: 19;

            then (i -' ( len p)) = (i - ( len p)) by A34, XREAL_0:def 2;

            then

             A35: (i -' ( len p)) <> (( len q) -' 1) by A22, A25;

            

            thus (r1 . j) = ((LMp . (j -' 1)) * (LMq . (i -' ( len p)))) by A28, A29, A31, A34

            .= ((LMp . (j -' 1)) * ( 0. L)) by A35, Def1

            .= ( 0. L);

          end;

        end;

        

        thus (F /. i) = (F . i) by A24, PARTFUN1:def 6

        .= (( Sum r1) * (( power L) . (x,(i -' 1)))) by A12, A24, A27

        .= (( 0. L) * (( power L) . (x,(i -' 1)))) by A30, POLYNOM3: 1

        .= ( 0. L);

      end;

      

       A36: ((( len p) + ( len q)) - 2) >= 0 by A7, XREAL_1: 19;

      ((( len p) + ( len q)) - (1 + 1)) >= 0 by A7, XREAL_1: 19;

      

      then

       A37: (i1 -' 1) = (((( len p) + ( len q)) - 1) - 1) by XREAL_0:def 2

      .= ((( len p) + ( len q)) -' 2) by A36, XREAL_0:def 2;

      per cases ;

        suppose ((LMp *' LMq) . (i1 -' 1)) <> ( 0. L);

        then ( len F) > (i1 -' 1) by A11, ALGSEQ_1: 8;

        then ( len F) >= i1 by A9, NAT_1: 13;

        then i1 in ( Seg ( len F)) by A8, FINSEQ_1: 1;

        then

         A38: i1 in ( dom F) by FINSEQ_1:def 3;

        

        hence ( eval ((( Leading-Monomial p) *' ( Leading-Monomial q)),x)) = (F /. i1) by A10, A23, POLYNOM2: 3

        .= (F . i1) by A38, PARTFUN1:def 6

        .= (((p . (( len p) -' 1)) * (q . (( len q) -' 1))) * (( power L) . (x,((( len p) + ( len q)) -' 2)))) by A12, A14, A37, A21, A38;

      end;

        suppose

         A39: ((LMp *' LMq) . (i1 -' 1)) = ( 0. L);

        now

          let j be Nat;

          assume j >= 0 ;

          j in NAT by ORDINAL1:def 12;

          then

          consider r1 be FinSequence of the carrier of L such that

           A40: ( len r1) = (j + 1) and

           A41: ((LMp *' LMq) . j) = ( Sum r1) and

           A42: for k be Element of NAT st k in ( dom r1) holds (r1 . k) = ((LMp . (k -' 1)) * (LMq . ((j + 1) -' k))) by POLYNOM3:def 9;

          now

            per cases ;

              suppose j = (i1 -' 1);

              hence ((LMp *' LMq) . j) = ( 0. L) by A39;

            end;

              suppose

               A43: j <> (i1 -' 1);

              now

                let k be Element of NAT ;

                assume

                 A44: k in ( dom r1);

                per cases ;

                  suppose

                   A45: (k -' 1) <> (( len p) -' 1);

                  

                  thus (r1 . k) = ((LMp . (k -' 1)) * (LMq . ((j + 1) -' k))) by A42, A44

                  .= (( 0. L) * (LMq . ((j + 1) -' k))) by A45, Def1

                  .= ( 0. L);

                end;

                  suppose

                   A46: (k -' 1) = (( len p) -' 1);

                  

                   A47: k in ( Seg ( len r1)) by A44, FINSEQ_1:def 3;

                  then ( 0 + 1) <= k by FINSEQ_1: 1;

                  then (k - 1) >= 0 by XREAL_1: 19;

                  then

                   A48: (k -' 1) = (k - 1) by XREAL_0:def 2;

                  ( 0 + k) <= (j + 1) by A40, A47, FINSEQ_1: 1;

                  then ((j + 1) - k) >= 0 by XREAL_1: 19;

                  then

                   A49: ((j + 1) -' k) = ((j - ( len p)) + 1) by A6, A46, A48, XREAL_0:def 2;

                  

                   A50: ((j - ( len p)) + 1) <> (((i1 -' 1) - ( len p)) + 1) by A43;

                  

                  thus (r1 . k) = ((LMp . (k -' 1)) * (LMq . ((j + 1) -' k))) by A42, A44

                  .= ((LMp . (k -' 1)) * ( 0. L)) by A22, A9, A49, A50, Def1

                  .= ( 0. L);

                end;

              end;

              hence ((LMp *' LMq) . j) = ( 0. L) by A41, POLYNOM3: 1;

            end;

          end;

          hence ((LMp *' LMq) . j) = ( 0. L);

        end;

        then 0 is_at_least_length_of (LMp *' LMq);

        then ( len (LMp *' LMq)) = 0 by ALGSEQ_1:def 3;

        then (LMp *' LMq) = ( 0_. L) by Th5;

        then ( eval ((LMp *' LMq),x)) = ( 0. L) by Th17;

        hence thesis by A14, A21, A39;

      end;

    end;

    

     Lm3: for L be add-associative right_zeroed right_complementable left_unital distributive commutative associative non trivial doubleLoopStr holds for p,q be Polynomial of L holds for x be Element of L holds ( eval ((( Leading-Monomial p) *' ( Leading-Monomial q)),x)) = (( eval (( Leading-Monomial p),x)) * ( eval (( Leading-Monomial q),x)))

    proof

      let L be add-associative right_zeroed right_complementable left_unital distributive commutative associative non trivial doubleLoopStr;

      let p,q be Polynomial of L;

      let x be Element of L;

      set p1 = (( len p) -' 1);

      set q1 = (( len q) -' 1);

      per cases ;

        suppose

         A1: ( len p) <> 0 & ( len q) <> 0 ;

        then

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

        then (( len q) - 1) >= 0 by XREAL_1: 19;

        then

         A3: (( len q) - 1) = (( len q) -' 1) by XREAL_0:def 2;

        

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

        then (( len p) - 1) >= 0 by XREAL_1: 19;

        then

         A5: (( len p) - 1) = (( len p) -' 1) by XREAL_0:def 2;

        (( len p) + ( len q)) >= ( 0 + (1 + 1)) by A4, A2, XREAL_1: 7;

        then ((( len p) + ( len q)) - 2) >= 0 by XREAL_1: 19;

        then

         A6: ((( len p) + ( len q)) -' 2) = ((( len p) + ( len q)) - 2) by XREAL_0:def 2;

        

         A7: ((( len p) + ( len q)) - (1 + 1)) = ((( len p) - 1) + (( len q) - 1));

        set P1 = (( power L) . (x,p1));

        set Q1 = (( power L) . (x,q1));

        

        thus ( eval ((( Leading-Monomial p) *' ( Leading-Monomial q)),x)) = (((p . p1) * (q . q1)) * (( power L) . (x,((( len p) + ( len q)) -' 2)))) by A1, Lm2

        .= (((p . p1) * (q . q1)) * (P1 * Q1)) by A5, A3, A6, A7, POLYNOM2: 1

        .= ((p . p1) * ((q . q1) * (P1 * Q1))) by GROUP_1:def 3

        .= ((p . p1) * (P1 * ((q . q1) * Q1))) by GROUP_1:def 3

        .= (((p . p1) * P1) * ((q . q1) * Q1)) by GROUP_1:def 3

        .= (((p . p1) * P1) * ( eval (( Leading-Monomial q),x))) by Th22

        .= (( eval (( Leading-Monomial p),x)) * ( eval (( Leading-Monomial q),x))) by Th22;

      end;

        suppose ( len p) = 0 ;

        then

         A8: ( Leading-Monomial p) = ( 0_. L) by Th12;

        

        hence ( eval ((( Leading-Monomial p) *' ( Leading-Monomial q)),x)) = ( eval (( 0_. L),x)) by Th2

        .= ( 0. L) by Th17

        .= (( 0. L) * ( eval (( Leading-Monomial q),x)))

        .= (( eval (( Leading-Monomial p),x)) * ( eval (( Leading-Monomial q),x))) by A8, Th17;

      end;

        suppose ( len q) = 0 ;

        then ( len ( Leading-Monomial q)) = 0 by Th15;

        then

         A9: ( Leading-Monomial q) = ( 0_. L) by Th5;

        

        hence ( eval ((( Leading-Monomial p) *' ( Leading-Monomial q)),x)) = ( eval (( 0_. L),x)) by POLYNOM3: 34

        .= ( 0. L) by Th17

        .= (( eval (( Leading-Monomial p),x)) * ( 0. L))

        .= (( eval (( Leading-Monomial p),x)) * ( eval (( Leading-Monomial q),x))) by A9, Th17;

      end;

    end;

    theorem :: POLYNOM4:23

    

     Th23: for L be add-associative right_zeroed right_complementable Abelian left_unital distributive commutative associative non trivial doubleLoopStr holds for p,q be Polynomial of L holds for x be Element of L holds ( eval ((( Leading-Monomial p) *' q),x)) = (( eval (( Leading-Monomial p),x)) * ( eval (q,x)))

    proof

      let L be add-associative right_zeroed right_complementable Abelian left_unital distributive commutative associative non trivial doubleLoopStr;

      let p1,q be Polynomial of L;

      let x be Element of L;

      set p = ( Leading-Monomial p1);

      defpred P[ Nat] means for q be Polynomial of L holds ( len q) = $1 implies ( eval ((p *' q),x)) = (( eval (p,x)) * ( eval (q,x)));

      

       A1: for k be Nat st for n be Nat st n < k holds P[n] holds P[k]

      proof

        let k be Nat;

        assume

         A2: for n be Nat st n < k holds for q be Polynomial of L holds ( len q) = n implies ( eval ((p *' q),x)) = (( eval (p,x)) * ( eval (q,x)));

        let q be Polynomial of L;

        assume

         A3: ( len q) = k;

        per cases ;

          suppose

           A4: ( len q) <> 0 ;

          set LMq = ( Leading-Monomial q);

          consider r be Polynomial of L such that

           A5: ( len r) < ( len q) and

           A6: q = (r + ( Leading-Monomial q)) and for n be Element of NAT st n < (( len q) - 1) holds (r . n) = (q . n) by A4, Th16;

          

          thus ( eval ((p *' q),x)) = ( eval (((p *' r) + (p *' LMq)),x)) by A6, POLYNOM3: 31

          .= (( eval ((p *' r),x)) + ( eval ((p *' LMq),x))) by Th19

          .= ((( eval (p,x)) * ( eval (r,x))) + ( eval ((p *' LMq),x))) by A2, A3, A5

          .= ((( eval (p,x)) * ( eval (r,x))) + (( eval (p,x)) * ( eval (LMq,x)))) by Lm3

          .= (( eval (p,x)) * (( eval (r,x)) + ( eval (LMq,x)))) by VECTSP_1:def 7

          .= (( eval (p,x)) * ( eval (q,x))) by A6, Th19;

        end;

          suppose ( len q) = 0 ;

          then

           A7: q = ( 0_. L) by Th5;

          

          hence ( eval ((p *' q),x)) = ( eval (( 0_. L),x)) by POLYNOM3: 34

          .= ( 0. L) by Th17

          .= (( eval (p,x)) * ( 0. L))

          .= (( eval (p,x)) * ( eval (q,x))) by A7, Th17;

        end;

      end;

      

       A8: for n be Nat holds P[n] from NAT_1:sch 4( A1);

      ( len q) = ( len q);

      hence thesis by A8;

    end;

    theorem :: POLYNOM4:24

    

     Th24: for L be add-associative right_zeroed right_complementable Abelian left_unital distributive commutative associative non trivial doubleLoopStr holds for p,q be Polynomial of L holds for x be Element of L holds ( eval ((p *' q),x)) = (( eval (p,x)) * ( eval (q,x)))

    proof

      let L be add-associative right_zeroed right_complementable Abelian left_unital distributive commutative associative non trivial doubleLoopStr;

      let p,q be Polynomial of L;

      let x be Element of L;

      defpred P[ Nat] means for p be Polynomial of L holds ( len p) = $1 implies ( eval ((p *' q),x)) = (( eval (p,x)) * ( eval (q,x)));

      

       A1: for k be Nat st for n be Nat st n < k holds P[n] holds P[k]

      proof

        let k be Nat;

        assume

         A2: for n be Nat st n < k holds for p be Polynomial of L holds ( len p) = n implies ( eval ((p *' q),x)) = (( eval (p,x)) * ( eval (q,x)));

        let p be Polynomial of L;

        assume

         A3: ( len p) = k;

        per cases ;

          suppose

           A4: ( len p) <> 0 ;

          set LMp = ( Leading-Monomial p);

          consider r be Polynomial of L such that

           A5: ( len r) < ( len p) and

           A6: p = (r + ( Leading-Monomial p)) and for n be Element of NAT st n < (( len p) - 1) holds (r . n) = (p . n) by A4, Th16;

          

          thus ( eval ((p *' q),x)) = ( eval (((r *' q) + (LMp *' q)),x)) by A6, POLYNOM3: 32

          .= (( eval ((r *' q),x)) + ( eval ((LMp *' q),x))) by Th19

          .= ((( eval (r,x)) * ( eval (q,x))) + ( eval ((LMp *' q),x))) by A2, A3, A5

          .= ((( eval (r,x)) * ( eval (q,x))) + (( eval (LMp,x)) * ( eval (q,x)))) by Th23

          .= ((( eval (r,x)) + ( eval (LMp,x))) * ( eval (q,x))) by VECTSP_1:def 7

          .= (( eval (p,x)) * ( eval (q,x))) by A6, Th19;

        end;

          suppose ( len p) = 0 ;

          then

           A7: p = ( 0_. L) by Th5;

          

          hence ( eval ((p *' q),x)) = ( eval (( 0_. L),x)) by Th2

          .= ( 0. L) by Th17

          .= (( 0. L) * ( eval (q,x)))

          .= (( eval (p,x)) * ( eval (q,x))) by A7, Th17;

        end;

      end;

      

       A8: for n be Nat holds P[n] from NAT_1:sch 4( A1);

      ( len p) = ( len p);

      hence thesis by A8;

    end;

    begin

    definition

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

      let x be Element of L;

      :: POLYNOM4:def3

      func Polynom-Evaluation (L,x) -> Function of ( Polynom-Ring L), L means

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

      existence

      proof

        defpred P[ set, set] means ex p be Polynomial of L st p = $1 & $2 = ( eval (p,x));

        

         A1: for y be Element of ( Polynom-Ring L) holds ex z be Element of L st P[y, z]

        proof

          let y be Element of ( Polynom-Ring L);

          reconsider p = y as Polynomial of L by POLYNOM3:def 10;

          take ( eval (p,x));

          take p;

          thus thesis;

        end;

        consider f be Function of the carrier of ( Polynom-Ring L), the carrier of L such that

         A2: for y be Element of ( Polynom-Ring L) holds P[y, (f . y)] from FUNCT_2:sch 3( A1);

        reconsider f as Function of ( Polynom-Ring L), L;

        take f;

        let p be Polynomial of L;

        p in the carrier of ( Polynom-Ring L) by POLYNOM3:def 10;

        then ex q be Polynomial of L st q = p & (f . p) = ( eval (q,x)) by A2;

        hence thesis;

      end;

      uniqueness

      proof

        let f1,f2 be Function of ( Polynom-Ring L), L such that

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

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

        now

          let y be Element of ( Polynom-Ring L);

          reconsider p = y as Polynomial of L by POLYNOM3:def 10;

          

          thus (f1 . y) = ( eval (p,x)) by A3

          .= (f2 . y) by A4;

        end;

        hence f1 = f2 by FUNCT_2: 63;

      end;

    end

    registration

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

      let x be Element of L;

      cluster ( Polynom-Evaluation (L,x)) -> unity-preserving;

      coherence

      proof

        

        thus (( Polynom-Evaluation (L,x)) . ( 1_ ( Polynom-Ring L))) = (( Polynom-Evaluation (L,x)) . ( 1_. L)) by POLYNOM3: 37

        .= ( eval (( 1_. L),x)) by Def3

        .= ( 1_ L) by Th18;

      end;

    end

    registration

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

      let x be Element of L;

      cluster ( Polynom-Evaluation (L,x)) -> additive;

      coherence

      proof

        let a,b be Element of ( Polynom-Ring L);

        reconsider p = a, q = b as Polynomial of L by POLYNOM3:def 10;

        

        thus (( Polynom-Evaluation (L,x)) . (a + b)) = (( Polynom-Evaluation (L,x)) . (p + q)) by POLYNOM3:def 10

        .= ( eval ((p + q),x)) by Def3

        .= (( eval (p,x)) + ( eval (q,x))) by Th19

        .= ((( Polynom-Evaluation (L,x)) . a) + ( eval (q,x))) by Def3

        .= ((( Polynom-Evaluation (L,x)) . a) + (( Polynom-Evaluation (L,x)) . b)) by Def3;

      end;

    end

    registration

      let L be add-associative right_zeroed right_complementable Abelian left_unital distributive commutative associative non trivial doubleLoopStr;

      let x be Element of L;

      cluster ( Polynom-Evaluation (L,x)) -> multiplicative;

      coherence

      proof

        let a,b be Element of ( Polynom-Ring L);

        reconsider p = a, q = b as Polynomial of L by POLYNOM3:def 10;

        

        thus (( Polynom-Evaluation (L,x)) . (a * b)) = (( Polynom-Evaluation (L,x)) . (p *' q)) by POLYNOM3:def 10

        .= ( eval ((p *' q),x)) by Def3

        .= (( eval (p,x)) * ( eval (q,x))) by Th24

        .= ((( Polynom-Evaluation (L,x)) . a) * ( eval (q,x))) by Def3

        .= ((( Polynom-Evaluation (L,x)) . a) * (( Polynom-Evaluation (L,x)) . b)) by Def3;

      end;

    end

    registration

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

      let x be Element of L;

      cluster ( Polynom-Evaluation (L,x)) -> RingHomomorphism;

      coherence ;

    end