polynom2.miz



    begin

    

     Lm1: for X be set, A be Subset of X, O be Order of X holds O is_reflexive_in A & O is_antisymmetric_in A & O is_transitive_in A

    proof

      let X be set, A be Subset of X, O be Order of X;

      

       A1: ( field O) = X by ORDERS_1: 12;

      then O is_antisymmetric_in X by RELAT_2:def 12;

      then

       A2: for x,y be object holds x in A & y in A & [x, y] in O & [y, x] in O implies x = y by RELAT_2:def 4;

      O is_transitive_in X by A1, RELAT_2:def 16;

      then

       A3: for x,y,z be object holds x in A & y in A & z in A & [x, y] in O & [y, z] in O implies [x, z] in O by RELAT_2:def 8;

      O is_reflexive_in X by A1, RELAT_2:def 9;

      then for x be object holds x in A implies [x, x] in O by RELAT_2:def 1;

      hence thesis by A2, A3, RELAT_2:def 1, RELAT_2:def 4, RELAT_2:def 8;

    end;

    

     Lm2: for X be set, A be Subset of X, O be Order of X st O is_connected_in X holds O is_connected_in A

    proof

      let X be set, A be Subset of X, O be Order of X;

      assume O is_connected_in X;

      then for x,y be object holds x in A & y in A & x <> y implies [x, y] in O or [y, x] in O by RELAT_2:def 6;

      hence thesis by RELAT_2:def 6;

    end;

    

     Lm3: for X be set, S be Subset of X, R be Order of X st R is being_linear-order holds R linearly_orders S

    proof

      let X be set, S be Subset of X, R be Order of X;

      

       A1: ( field R) = X by ORDERS_1: 12;

      then

       A2: R is_reflexive_in X by RELAT_2:def 9;

      R is_transitive_in X by A1, RELAT_2:def 16;

      then for x,y,z be object holds x in S & y in S & z in S & [x, y] in R & [y, z] in R implies [x, z] in R by RELAT_2:def 8;

      then

       A3: R is_transitive_in S by RELAT_2:def 8;

      R is_antisymmetric_in X by A1, RELAT_2:def 12;

      then for x,y be object holds x in S & y in S & [x, y] in R & [y, x] in R implies x = y by RELAT_2:def 4;

      then

       A4: R is_antisymmetric_in S by RELAT_2:def 4;

      assume R is being_linear-order;

      then R is connected by ORDERS_1:def 6;

      then

       A5: R is_connected_in ( field R) by RELAT_2:def 14;

      for x,y be object holds x in S & y in S & x <> y implies [x, y] in R or [y, x] in R

      proof

        let x,y be object;

        assume that

         A6: x in S and

         A7: y in S and

         A8: x <> y;

        

         A9: ( field R) = (( dom R) \/ ( rng R)) by RELAT_1:def 6;

         [y, y] in R by A2, A7, RELAT_2:def 1;

        then y in ( dom R) by XTUPLE_0:def 12;

        then

         A10: y in ( field R) by A9, XBOOLE_0:def 3;

         [x, x] in R by A2, A6, RELAT_2:def 1;

        then x in ( dom R) by XTUPLE_0:def 12;

        then x in ( field R) by A9, XBOOLE_0:def 3;

        hence thesis by A5, A8, A10, RELAT_2:def 6;

      end;

      then

       A11: R is_connected_in S by RELAT_2:def 6;

      for x be object holds x in S implies [x, x] in R by A2, RELAT_2:def 1;

      then R is_reflexive_in S by RELAT_2:def 1;

      hence thesis by A4, A3, A11, ORDERS_1:def 9;

    end;

    theorem :: POLYNOM2:1

    

     Th1: for L be unital associative non empty multMagma, a be Element of L, n,m be Element of NAT holds (( power L) . (a,(n + m))) = ((( power L) . (a,n)) * (( power L) . (a,m)))

    proof

      let L be unital associative non empty multMagma, a be Element of L, n,m be Element of NAT ;

      defpred P[ Nat] means (( power L) . (a,(n + $1))) = ((( power L) . (a,n)) * (( power L) . (a,$1)));

       A1:

      now

        let m be Nat;

        assume

         A2: P[m];

        (( power L) . (a,(n + (m + 1)))) = (( power L) . (a,((n + m) + 1)))

        .= (((( power L) . (a,n)) * (( power L) . (a,m))) * a) by A2, GROUP_1:def 7

        .= ((( power L) . (a,n)) * ((( power L) . (a,m)) * a)) by GROUP_1:def 3

        .= ((( power L) . (a,n)) * (( power L) . (a,(m + 1)))) by GROUP_1:def 7;

        hence P[(m + 1)];

      end;

      (( power L) . (a,(n + 0 ))) = ((( power L) . (a,n)) * ( 1_ L)) by GROUP_1:def 4

      .= ((( power L) . (a,n)) * (( power L) . (a, 0 ))) by GROUP_1:def 7;

      then

       A3: P[ 0 ];

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

      hence thesis;

    end;

    registration

      cluster Abelian right_zeroed add-associative right_complementable well-unital distributive commutative associative for non trivial doubleLoopStr;

      existence

      proof

        take F_Real ;

        thus thesis;

      end;

    end

    begin

    ::$Canceled

    theorem :: POLYNOM2:3

    

     Th2: for L be left_zeroed right_zeroed non empty addLoopStr, p be FinSequence of the carrier of L, i be Element of NAT st i in ( dom p) & for i9 be Element of NAT st i9 in ( dom p) & i9 <> i holds (p /. i9) = ( 0. L) holds ( Sum p) = (p /. i)

    proof

      let L be left_zeroed right_zeroed non empty addLoopStr, p be FinSequence of the carrier of L, i be Element of NAT ;

      assume that

       A1: i in ( dom p) and

       A2: for i9 be Element of NAT st i9 in ( dom p) & i9 <> i holds (p /. i9) = ( 0. L);

      consider fp be sequence of the carrier of L such that

       A3: ( Sum p) = (fp . ( len p)) and

       A4: (fp . 0 ) = ( 0. L) and

       A5: for j be Nat, v be Element of L st j < ( len p) & v = (p . (j + 1)) holds (fp . (j + 1)) = ((fp . j) + v) by RLVECT_1:def 12;

      defpred P[ Element of NAT ] means ($1 < i & (fp . $1) = ( 0. L)) or (i <= $1 & (fp . $1) = (p /. i));

      consider l be Nat such that

       A6: ( dom p) = ( Seg l) by FINSEQ_1:def 2;

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

      

       A7: ( len p) = l by A6, FINSEQ_1:def 3;

      i in { z where z be Nat : 1 <= z & z <= l } by A1, A6, FINSEQ_1:def 1;

      then

       A8: ex i9 be Nat st i9 = i & 1 <= i9 & i9 <= l;

      

       A9: for j be Element of NAT st 0 <= j & j < ( len p) holds P[j] implies P[(j + 1)]

      proof

        let j be Element of NAT ;

        assume that 0 <= j and

         A10: j < ( len p);

        assume

         A11: P[j];

        per cases ;

          suppose

           A12: j < i;

          per cases ;

            suppose

             A13: (j + 1) = i;

            then (p . (j + 1)) = (p /. (j + 1)) by A1, PARTFUN1:def 6;

            

            then (fp . (j + 1)) = (( 0. L) + (p /. (j + 1))) by A5, A10, A11, A12

            .= (p /. (j + 1)) by ALGSTR_1:def 2;

            hence thesis by A13;

          end;

            suppose

             A14: (j + 1) <> i;

            

             A15: (j + 1) < i

            proof

              assume i <= (j + 1);

              then i < (j + 1) by A14, XXREAL_0: 1;

              hence thesis by A12, NAT_1: 13;

            end;

            (j + 1) <= i by A12, NAT_1: 13;

            then

             A16: (j + 1) <= l by A8, XXREAL_0: 2;

            ( 0 + 1) <= (j + 1) by XREAL_1: 6;

            then

             A17: (j + 1) in ( Seg l) by A16, FINSEQ_1: 1;

            then (p . (j + 1)) = (p /. (j + 1)) by A6, PARTFUN1:def 6;

            

            then (fp . (j + 1)) = (( 0. L) + (p /. (j + 1))) by A5, A10, A11, A12

            .= (p /. (j + 1)) by ALGSTR_1:def 2

            .= ( 0. L) by A2, A6, A14, A17;

            hence thesis by A15;

          end;

        end;

          suppose

           A18: i <= j;

          j < l by A6, A10, FINSEQ_1:def 3;

          then

           A19: (j + 1) <= l by NAT_1: 13;

          

           A20: i < (j + 1) by A18, NAT_1: 13;

          ( 0 + 1) <= (j + 1) by XREAL_1: 6;

          then

           A21: (j + 1) in ( dom p) by A6, A19, FINSEQ_1: 1;

          then (p . (j + 1)) = (p /. (j + 1)) by PARTFUN1:def 6;

          

          then (fp . (j + 1)) = ((p /. i) + (p /. (j + 1))) by A5, A10, A11, A18

          .= ((p /. i) + ( 0. L)) by A2, A20, A21

          .= (p /. i) by RLVECT_1:def 4;

          hence thesis by A18, NAT_1: 13;

        end;

      end;

      

       A22: P[ 0 ] by A4, A8;

      for j be Element of NAT st 0 <= j & j <= ( len p) holds P[j] from INT_1:sch 7( A22, A9);

      hence thesis by A3, A8, A7;

    end;

    theorem :: POLYNOM2:4

    for L be add-associative right_zeroed right_complementable distributive well-unital non empty doubleLoopStr, p be FinSequence of the carrier of L st ex i be Element of NAT st i in ( dom p) & (p /. i) = ( 0. L) holds ( Product p) = ( 0. L)

    proof

      let L be add-associative right_zeroed right_complementable distributive well-unital non empty doubleLoopStr, p be FinSequence of the carrier of L;

      given i be Element of NAT such that

       A1: i in ( dom p) and

       A2: (p /. i) = ( 0. L);

      defpred P[ Nat] means for p be FinSequence of the carrier of L st ( len p) = $1 & ex i be Element of NAT st i in ( dom p) & (p /. i) = ( 0. L) holds ( Product p) = ( 0. L);

      

       A3: for j be Nat holds P[j] implies P[(j + 1)]

      proof

        let j be Nat;

        assume

         A4: P[j];

        for p be FinSequence of the carrier of L st ( len p) = (j + 1) & ex i be Element of NAT st i in ( dom p) & (p /. i) = ( 0. L) holds ( Product p) = ( 0. L)

        proof

          let p be FinSequence of the carrier of L;

          assume that

           A5: ( len p) = (j + 1) and

           A6: ex i be Element of NAT st i in ( dom p) & (p /. i) = ( 0. L);

          

           A7: ex fp be sequence of the carrier of L st (fp . 1) = (p . 1) & (for i be Nat st 0 <> i & i < ( len p) holds (fp . (i + 1)) = (the multF of L . ((fp . i),(p . (i + 1))))) & (the multF of L "**" p) = (fp . ( len p)) by A5, FINSOP_1: 1, NAT_1: 14;

          

           A8: ( len p) >= 1 by A5, NAT_1: 14;

          then

           A9: 1 in ( dom p) by FINSEQ_3: 25;

          

           A10: ( dom p) = ( Seg ( len p)) by FINSEQ_1:def 3;

          then

           A11: (j + 1) in ( dom p) by A5, A8, FINSEQ_1: 1;

          per cases ;

            suppose

             A12: j = 0 ;

            then

             A13: ( dom p) = {1} by A5, FINSEQ_1: 2, FINSEQ_1:def 3;

            ( Product p) = (p . 1) by A5, A7, A12, GROUP_4:def 2

            .= (p /. 1) by A9, PARTFUN1:def 6;

            hence thesis by A6, A13, TARSKI:def 1;

          end;

            suppose j <> 0 ;

            then

             A14: 1 <= j by NAT_1: 14;

            reconsider p9 = (p | ( Seg j)) as FinSequence of the carrier of L by FINSEQ_1: 18;

            

             A15: j <= (j + 1) by XREAL_1: 29;

            then

             A16: ( dom p9) = ( Seg j) by A5, FINSEQ_1: 17;

            p = (p9 ^ <*(p . ( len p))*>) by A5, FINSEQ_3: 55;

            then

             A17: p = (p9 ^ <*(p /. ( len p))*>) by A5, A11, PARTFUN1:def 6;

            

             A18: ( len p9) = j by A5, A15, FINSEQ_1: 17;

            per cases ;

              suppose (p /. ( len p)) = ( 0. L);

              

              hence ( Product p) = (( Product p9) * ( 0. L)) by A17, GROUP_4: 6

              .= ( 0. L);

            end;

              suppose

               A19: (p /. ( len p)) <> ( 0. L);

              consider i be Element of NAT such that

               A20: i in ( dom p) and

               A21: (p /. i) = ( 0. L) by A6;

              i <= ( len p) by A10, A20, FINSEQ_1: 1;

              then i < ( len p) by A19, A21, XXREAL_0: 1;

              then

               A22: i <= j by A5, NAT_1: 13;

              

               A23: 1 <= i by A10, A20, FINSEQ_1: 1;

              then

               A24: i in ( dom p9) by A16, A22, FINSEQ_1: 1;

              

               A25: j in ( dom p) by A5, A10, A14, A15, FINSEQ_1: 1;

              i in ( Seg j) by A23, A22, FINSEQ_1: 1;

              then ((p | j) . i) = (p . i) by A25, RFINSEQ: 6;

              then (p9 . i) = (p . i) by FINSEQ_1:def 15;

              then (p9 /. i) = (p . i) by A24, PARTFUN1:def 6;

              then

               A26: (p9 /. i) = ( 0. L) by A20, A21, PARTFUN1:def 6;

              

              thus ( Product p) = (( Product p9) * (p /. ( len p))) by A17, GROUP_4: 6

              .= (( 0. L) * (p /. ( len p))) by A4, A18, A24, A26

              .= ( 0. L);

            end;

          end;

        end;

        hence thesis;

      end;

      

       A27: ex l be Element of NAT st l = ( len p);

      

       A28: P[ 0 ]

      proof

        let p be FinSequence of L;

        assume ( len p) = 0 ;

        then p = {} ;

        hence thesis;

      end;

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

      hence thesis by A1, A2, A27;

    end;

    theorem :: POLYNOM2:5

    

     Th4: for L be Abelian add-associative non empty addLoopStr, a be Element of L, p,q be FinSequence of the carrier of L st ( len p) = ( len q) & ex i be Element of NAT st i in ( dom p) & (q /. i) = (a + (p /. i)) & for i9 be Element of NAT st i9 in ( dom p) & i9 <> i holds (q /. i9) = (p /. i9) holds ( Sum q) = (a + ( Sum p))

    proof

      let L be Abelian add-associative non empty addLoopStr, a be Element of L, p,q be FinSequence of the carrier of L;

      assume that

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

       A2: ex i be Element of NAT st i in ( dom p) & (q /. i) = (a + (p /. i)) & for i9 be Element of NAT st i9 in ( dom p) & i9 <> i holds (q /. i9) = (p /. i9);

      consider i be Element of NAT such that

       A3: i in ( dom p) and

       A4: (q /. i) = (a + (p /. i)) and

       A5: for i9 be Element of NAT st i9 in ( dom p) & i9 <> i holds (q /. i9) = (p /. i9) by A2;

      consider fq be sequence of the carrier of L such that

       A6: ( Sum q) = (fq . ( len q)) and

       A7: (fq . 0 ) = ( 0. L) and

       A8: for j be Nat, v be Element of L st j < ( len q) & v = (q . (j + 1)) holds (fq . (j + 1)) = ((fq . j) + v) by RLVECT_1:def 12;

      consider l be Nat such that

       A9: ( dom p) = ( Seg l) by FINSEQ_1:def 2;

      i in { z where z be Nat : 1 <= z & z <= l } by A3, A9, FINSEQ_1:def 1;

      then

       A10: ex i9 be Nat st i9 = i & 1 <= i9 & i9 <= l;

      consider l9 be Nat such that

       A11: ( dom q) = ( Seg l9) by FINSEQ_1:def 2;

      reconsider l, l9 as Element of NAT by ORDINAL1:def 12;

      consider fp be sequence of the carrier of L such that

       A12: ( Sum p) = (fp . ( len p)) and

       A13: (fp . 0 ) = ( 0. L) and

       A14: for j be Nat, v be Element of L st j < ( len p) & v = (p . (j + 1)) holds (fp . (j + 1)) = ((fp . j) + v) by RLVECT_1:def 12;

      

       A15: ( len p) = l by A9, FINSEQ_1:def 3;

      defpred P[ Element of NAT ] means ($1 < i & (fp . $1) = (fq . $1)) or (i <= $1 & (fq . $1) = (a + (fp . $1)));

      

       A16: l = ( len p) by A9, FINSEQ_1:def 3

      .= l9 by A1, A11, FINSEQ_1:def 3;

      

       A17: for j be Element of NAT st 0 <= j & j < ( len p) holds P[j] implies P[(j + 1)]

      proof

        let j be Element of NAT ;

        assume that 0 <= j and

         A18: j < ( len p);

        assume

         A19: P[j];

        per cases ;

          suppose

           A20: j < i;

          per cases ;

            suppose

             A21: (j + 1) = i;

            then

             A22: (p . (j + 1)) = (p /. (j + 1)) by A3, PARTFUN1:def 6;

            (q . (j + 1)) = (q /. (j + 1)) by A3, A9, A11, A16, A21, PARTFUN1:def 6;

            

            then (fq . (j + 1)) = ((fq . j) + (a + (p /. (j + 1)))) by A1, A4, A8, A18, A21

            .= (a + ((fq . j) + (p /. (j + 1)))) by RLVECT_1:def 3

            .= (a + (fp . (j + 1))) by A14, A18, A19, A20, A22;

            hence thesis by A21;

          end;

            suppose

             A23: (j + 1) <> i;

            

             A24: (j + 1) < i

            proof

              assume i <= (j + 1);

              then i < (j + 1) by A23, XXREAL_0: 1;

              hence thesis by A20, NAT_1: 13;

            end;

            (j + 1) <= i by A20, NAT_1: 13;

            then

             A25: (j + 1) <= l by A10, XXREAL_0: 2;

            ( 0 + 1) <= (j + 1) by XREAL_1: 6;

            then

             A26: (j + 1) in ( Seg l) by A25, FINSEQ_1: 1;

            then

             A27: (p . (j + 1)) = (p /. (j + 1)) by A9, PARTFUN1:def 6;

            (q . (j + 1)) = (q /. (j + 1)) by A11, A16, A26, PARTFUN1:def 6;

            

            then (fq . (j + 1)) = ((fq . j) + (q /. (j + 1))) by A1, A8, A18

            .= (fp . (j + 1)) by A5, A14, A9, A18, A19, A20, A23, A26, A27;

            hence thesis by A24;

          end;

        end;

          suppose

           A28: i <= j;

          j < l by A9, A18, FINSEQ_1:def 3;

          then

           A29: (j + 1) <= l by NAT_1: 13;

          ( 0 + 1) <= (j + 1) by XREAL_1: 6;

          then

           A30: (j + 1) in ( dom p) by A9, A29, FINSEQ_1: 1;

          then

           A31: (p . (j + 1)) = (p /. (j + 1)) by PARTFUN1:def 6;

          

           A32: i < (j + 1) by A28, NAT_1: 13;

          (q . (j + 1)) = (q /. (j + 1)) by A9, A11, A16, A30, PARTFUN1:def 6;

          

          then (fq . (j + 1)) = ((fq . j) + (q /. (j + 1))) by A1, A8, A18

          .= ((a + (fp . j)) + (p /. (j + 1))) by A5, A19, A28, A32, A30

          .= (a + ((fp . j) + (p /. (j + 1)))) by RLVECT_1:def 3

          .= (a + (fp . (j + 1))) by A14, A18, A31;

          hence thesis by A28, NAT_1: 13;

        end;

      end;

      

       A33: P[ 0 ] by A13, A7, A10;

      for j be Element of NAT st 0 <= j & j <= ( len p) holds P[j] from INT_1:sch 7( A33, A17);

      hence thesis by A1, A12, A6, A10, A15;

    end;

    theorem :: POLYNOM2:6

    

     Th5: for L be commutative associative non empty doubleLoopStr, a be Element of L, p,q be FinSequence of the carrier of L st ( len p) = ( len q) & ex i be Element of NAT st i in ( dom p) & (q /. i) = (a * (p /. i)) & for i9 be Element of NAT st i9 in ( dom p) & i9 <> i holds (q /. i9) = (p /. i9) holds ( Product q) = (a * ( Product p))

    proof

      let L be commutative associative non empty doubleLoopStr, a be Element of L, p,q be FinSequence of the carrier of L;

      assume that

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

       A2: ex i be Element of NAT st i in ( dom p) & (q /. i) = (a * (p /. i)) & for i9 be Element of NAT st i9 in ( dom p) & i9 <> i holds (q /. i9) = (p /. i9);

      consider i be Element of NAT such that

       A3: i in ( dom p) and

       A4: (q /. i) = (a * (p /. i)) and

       A5: for i9 be Element of NAT st i9 in ( dom p) & i9 <> i holds (q /. i9) = (p /. i9) by A2;

      

       A6: ( Product p) = (the multF of L "**" p) by GROUP_4:def 2;

      

       A7: ( Product q) = (the multF of L "**" q) by GROUP_4:def 2;

      per cases ;

        suppose ( len p) = 0 ;

        then p = {} ;

        hence thesis by A3;

      end;

        suppose

         A8: ( len p) <> 0 ;

        then

         A9: ( len p) >= 1 by NAT_1: 14;

        consider l9 be Nat such that

         A10: ( dom q) = ( Seg l9) by FINSEQ_1:def 2;

        consider fp be sequence of the carrier of L such that

         A11: (fp . 1) = (p . 1) and

         A12: for i be Nat st 0 <> i & i < ( len p) holds (fp . (i + 1)) = (the multF of L . ((fp . i),(p . (i + 1)))) and

         A13: ( Product p) = (fp . ( len p)) by A6, A8, FINSOP_1: 1, NAT_1: 14;

        consider fq be sequence of the carrier of L such that

         A14: (fq . 1) = (q . 1) and

         A15: for i be Nat st 0 <> i & i < ( len q) holds (fq . (i + 1)) = (the multF of L . ((fq . i),(q . (i + 1)))) and

         A16: ( Product q) = (fq . ( len p)) by A1, A7, A8, FINSOP_1: 1, NAT_1: 14;

        defpred P[ Element of NAT ] means ($1 < i & (fp . $1) = (fq . $1)) or (i <= $1 & (fq . $1) = (a * (fp . $1)));

        consider l be Nat such that

         A17: ( dom p) = ( Seg l) by FINSEQ_1:def 2;

        i in { z where z be Nat : 1 <= z & z <= l } by A3, A17, FINSEQ_1:def 1;

        then

         A18: ex i9 be Nat st i9 = i & 1 <= i9 & i9 <= l;

        reconsider l, l9 as Element of NAT by ORDINAL1:def 12;

        

         A19: ( len p) = l by A17, FINSEQ_1:def 3;

        

         A20: 1 <= l by A18, XXREAL_0: 2;

        then

         A21: 1 in ( dom p) by A17, FINSEQ_1: 1;

        

         A22: l = ( len p) by A17, FINSEQ_1:def 3

        .= l9 by A1, A10, FINSEQ_1:def 3;

        

         A23: for j be Element of NAT st 1 <= j & j < ( len p) holds P[j] implies P[(j + 1)]

        proof

          let j be Element of NAT ;

          assume that

           A24: 1 <= j and

           A25: j < ( len p);

          assume

           A26: P[j];

          per cases ;

            suppose

             A27: j < i;

            per cases ;

              suppose

               A28: (j + 1) = i;

              then

               A29: (p . (j + 1)) = (p /. (j + 1)) by A3, PARTFUN1:def 6;

              (q . (j + 1)) = (q /. (j + 1)) by A3, A17, A10, A22, A28, PARTFUN1:def 6;

              

              then (fq . (j + 1)) = ((fp . j) * (a * (p /. (j + 1)))) by A1, A4, A15, A24, A25, A26, A27, A28

              .= (((fp . j) * (p /. (j + 1))) * a) by GROUP_1:def 3

              .= ((fp . (j + 1)) * a) by A12, A24, A25, A29;

              hence thesis by A28;

            end;

              suppose

               A30: (j + 1) <> i;

              

               A31: (j + 1) < i

              proof

                assume i <= (j + 1);

                then i < (j + 1) by A30, XXREAL_0: 1;

                hence thesis by A27, NAT_1: 13;

              end;

              (j + 1) <= i by A27, NAT_1: 13;

              then

               A32: (j + 1) <= l by A18, XXREAL_0: 2;

              ( 0 + 1) <= (j + 1) by XREAL_1: 6;

              then

               A33: (j + 1) in ( Seg l) by A32, FINSEQ_1: 1;

              then

               A34: (p . (j + 1)) = (p /. (j + 1)) by A17, PARTFUN1:def 6;

              (q . (j + 1)) = (q /. (j + 1)) by A10, A22, A33, PARTFUN1:def 6;

              

              then (fq . (j + 1)) = ((fq . j) * (q /. (j + 1))) by A1, A15, A24, A25

              .= (the multF of L . ((fq . j),(p . (j + 1)))) by A5, A17, A30, A33, A34

              .= (fp . (j + 1)) by A12, A24, A25, A26, A27;

              hence thesis by A31;

            end;

          end;

            suppose

             A35: i <= j;

            j < l by A17, A25, FINSEQ_1:def 3;

            then

             A36: (j + 1) <= l by NAT_1: 13;

            ( 0 + 1) <= (j + 1) by XREAL_1: 6;

            then

             A37: (j + 1) in ( dom p) by A17, A36, FINSEQ_1: 1;

            then

             A38: (p . (j + 1)) = (p /. (j + 1)) by PARTFUN1:def 6;

            

             A39: i < (j + 1) by A35, NAT_1: 13;

            (q . (j + 1)) = (q /. (j + 1)) by A17, A10, A22, A37, PARTFUN1:def 6;

            

            then (fq . (j + 1)) = ((fq . j) * (q /. (j + 1))) by A1, A15, A24, A25

            .= ((a * (fp . j)) * (p /. (j + 1))) by A5, A26, A35, A39, A37

            .= (a * ((fp . j) * (p /. (j + 1)))) by GROUP_1:def 3

            .= (a * (fp . (j + 1))) by A12, A24, A25, A38;

            hence thesis by A35, NAT_1: 13;

          end;

        end;

        

         A40: 1 in ( dom q) by A10, A22, A20, FINSEQ_1: 1;

        now

          per cases ;

            case

             A41: 1 < i;

            

            thus (fp . 1) = (p /. 1) by A11, A21, PARTFUN1:def 6

            .= (q /. 1) by A5, A21, A41

            .= (fq . 1) by A14, A40, PARTFUN1:def 6;

          end;

            case i <= 1;

            then i = 1 by A18, XXREAL_0: 1;

            

            hence (fq . 1) = (a * (p /. 1)) by A3, A4, A14, A17, A10, A22, PARTFUN1:def 6

            .= (a * (fp . 1)) by A11, A21, PARTFUN1:def 6;

          end;

        end;

        then

         A42: P[1];

        for j be Element of NAT st 1 <= j & j <= ( len p) holds P[j] from INT_1:sch 7( A42, A23);

        hence thesis by A9, A13, A16, A18, A19;

      end;

    end;

    begin

    definition

      ::$Canceled

      let n be Ordinal, b be bag of n, L be well-unital non trivial doubleLoopStr, x be Function of n, L;

      :: POLYNOM2:def2

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

      : Def1: ex y be FinSequence of the carrier of L st ( len y) = ( len ( SgmX (( RelIncl n),( support b)))) & it = ( Product y) & for i be Element of NAT st 1 <= i & i <= ( len y) holds (y /. i) = (( power L) . (((x * ( SgmX (( RelIncl n),( support b)))) /. i),((b * ( SgmX (( RelIncl n),( support b)))) /. i)));

      existence

      proof

        set S = ( SgmX (( RelIncl n),( support b)));

        set l = ( len S);

        defpred P[ Nat, Element of L] means $2 = (( power L) . (((x * S) /. $1),((b * S) /. $1)));

        

         A1: for k be Nat st k in ( Seg l) holds ex x be Element of L st P[k, x];

        consider p be FinSequence of the carrier of L such that

         A2: ( dom p) = ( Seg l) & for k be Nat st k in ( Seg l) holds P[k, (p /. k)] from RECDEF_1:sch 17( A1);

        take ( Product p);

        

         A3: ( len p) = l by A2, FINSEQ_1:def 3;

        for m be Element of NAT st 1 <= m & m <= ( len p) holds (p /. m) = (( power L) . (((x * S) /. m),((b * S) /. m))) by A3, A2, FINSEQ_1: 1;

        hence thesis by A3;

      end;

      uniqueness

      proof

        set S = ( SgmX (( RelIncl n),( support b)));

        let a,c be Element of L;

        assume that

         A4: ex y1 be FinSequence of the carrier of L st ( len y1) = ( len ( SgmX (( RelIncl n),( support b)))) & a = ( Product y1) & for i be Element of NAT st 1 <= i & i <= ( len y1) holds (y1 /. i) = (( power L) . (((x * ( SgmX (( RelIncl n),( support b)))) /. i),((b * ( SgmX (( RelIncl n),( support b)))) /. i))) and

         A5: ex y2 be FinSequence of the carrier of L st ( len y2) = ( len ( SgmX (( RelIncl n),( support b)))) & c = ( Product y2) & for i be Element of NAT st 1 <= i & i <= ( len y2) holds (y2 /. i) = (( power L) . (((x * ( SgmX (( RelIncl n),( support b)))) /. i),((b * ( SgmX (( RelIncl n),( support b)))) /. i)));

        consider y1 be FinSequence of the carrier of L such that

         A6: ( len y1) = ( len ( SgmX (( RelIncl n),( support b)))) and

         A7: ( Product y1) = a and

         A8: for i be Element of NAT st 1 <= i & i <= ( len y1) holds (y1 /. i) = (( power L) . (((x * ( SgmX (( RelIncl n),( support b)))) /. i),((b * ( SgmX (( RelIncl n),( support b)))) /. i))) by A4;

        consider y2 be FinSequence of the carrier of L such that

         A9: ( len y2) = ( len ( SgmX (( RelIncl n),( support b)))) and

         A10: ( Product y2) = c and

         A11: for i be Element of NAT st 1 <= i & i <= ( len y2) holds (y2 /. i) = (( power L) . (((x * ( SgmX (( RelIncl n),( support b)))) /. i),((b * ( SgmX (( RelIncl n),( support b)))) /. i))) by A5;

        now

          let i be Nat;

          assume that

           A12: 1 <= i and

           A13: i <= ( len y1);

          i in ( Seg ( len y2)) by A6, A9, A12, A13, FINSEQ_1: 1;

          then

           A14: i in ( dom y2) by FINSEQ_1:def 3;

          

           A15: i in ( Seg ( len y1)) by A12, A13, FINSEQ_1: 1;

          then i in ( dom y1) by FINSEQ_1:def 3;

          

          hence (y1 . i) = (y1 /. i) by PARTFUN1:def 6

          .= (( power L) . (((x * S) /. i),((b * S) /. i))) by A8, A12, A13, A15

          .= (y2 /. i) by A6, A9, A11, A12, A13, A15

          .= (y2 . i) by A14, PARTFUN1:def 6;

        end;

        hence thesis by A6, A7, A9, A10, FINSEQ_1: 14;

      end;

    end

    ::$Canceled

    theorem :: POLYNOM2:14

    

     Th6: for n be Ordinal, L be well-unital non trivial doubleLoopStr, x be Function of n, L holds ( eval (( EmptyBag n),x)) = ( 1. L)

    proof

      let n be Ordinal, L be well-unital non trivial doubleLoopStr, x be Function of n, L;

      set b = ( EmptyBag n);

      reconsider s = ( support b) as empty Subset of n;

      consider y be FinSequence of the carrier of L such that

       A1: ( len y) = ( len ( SgmX (( RelIncl n),( support b)))) and

       A2: ( eval (b,x)) = ( Product y) and for i be Element of NAT st 1 <= i & i <= ( len y) holds (y /. i) = (( power L) . (((x * ( SgmX (( RelIncl n),( support b)))) /. i),((b * ( SgmX (( RelIncl n),( support b)))) /. i))) by Def1;

      ( SgmX (( RelIncl n),s)) = {} by PRE_POLY: 76, PRE_POLY: 82;

      then y = ( <*> the carrier of L) by A1;

      then ( eval (( EmptyBag n),x)) = ( 1_ L) by A2, GROUP_4: 8;

      hence thesis;

    end;

    theorem :: POLYNOM2:15

    

     Th7: for n be Ordinal, L be well-unital non trivial doubleLoopStr, u be set, b be bag of n st ( support b) = {u} holds for x be Function of n, L holds ( eval (b,x)) = (( power L) . ((x . u),(b . u)))

    proof

      let n be Ordinal, L be well-unital non trivial doubleLoopStr, u be set, b be bag of n;

      reconsider sb = ( support b) as finite Subset of n;

      set sg = ( SgmX (( RelIncl n),sb));

      assume

       A1: ( support b) = {u};

      then

       A2: u in ( support b) by TARSKI:def 1;

      let x be Function of n, L;

      

       A3: ( rng x) c= the carrier of L by RELAT_1:def 19;

      

       A4: n = ( dom x) by FUNCT_2:def 1;

      then (x . u) in ( rng x) by A2, FUNCT_1:def 3;

      then

      reconsider xu = (x . u) as Element of L by A3;

      

       A5: ( RelIncl n) linearly_orders sb by PRE_POLY: 82;

      then

       A6: ( rng sg) = {u} by A1, PRE_POLY:def 2;

      then

       A7: u in ( rng sg) by TARSKI:def 1;

      then

       A8: 1 in ( dom sg) by FINSEQ_3: 31;

      then

       A9: (sg . 1) in ( rng sg) by FUNCT_1:def 3;

      then

       A10: (sg . 1) = u by A6, TARSKI:def 1;

      then 1 in ( dom (x * sg)) by A4, A8, A2, FUNCT_1: 11;

      

      then

       A11: ((x * sg) /. 1) = ((x * sg) . 1) by PARTFUN1:def 6

      .= (x . (sg . 1)) by A8, FUNCT_1: 13

      .= (x . u) by A6, A9, TARSKI:def 1;

      ( dom b) = n by PARTFUN1:def 2;

      then 1 in ( dom (b * sg)) by A8, A10, A2, FUNCT_1: 11;

      

      then

       A12: ((b * sg) /. 1) = ((b * sg) . 1) by PARTFUN1:def 6

      .= (b . (sg . 1)) by A8, FUNCT_1: 13

      .= (b . u) by A6, A9, TARSKI:def 1;

      

       A13: (( power L) . (xu,(b . u))) = (( power L) . [xu, (b . u)]);

      

       A14: for v be object holds v in ( dom sg) implies v in {1}

      proof

        let v be object;

        assume

         A15: v in ( dom sg);

        assume

         A16: not v in {1};

        reconsider v as Element of NAT by A15;

        (sg /. v) = (sg . v) by A15, PARTFUN1:def 6;

        then

         A17: (sg /. v) in ( rng sg) by A15, FUNCT_1:def 3;

        

         A18: v <> 1 by A16, TARSKI:def 1;

        

         A19: 1 < v

        proof

          consider k be Nat such that

           A20: ( dom sg) = ( Seg k) by FINSEQ_1:def 2;

          ( Seg k) = { l where l be Nat : 1 <= l & l <= k } by FINSEQ_1:def 1;

          then ex m9 be Nat st m9 = v & 1 <= m9 & m9 <= k by A15, A20;

          hence thesis by A18, XXREAL_0: 1;

        end;

        (sg /. 1) = (sg . 1) by A7, A15, FINSEQ_3: 31, PARTFUN1:def 6;

        then (sg /. 1) in ( rng sg) by A8, FUNCT_1:def 3;

        

        then (sg /. 1) = u by A6, TARSKI:def 1

        .= (sg /. v) by A6, A17, TARSKI:def 1;

        hence thesis by A5, A8, A15, A19, PRE_POLY:def 2;

      end;

      consider y be FinSequence of the carrier of L such that

       A21: ( len y) = ( len ( SgmX (( RelIncl n),( support b)))) and

       A22: ( eval (b,x)) = ( Product y) and

       A23: for i be Element of NAT st 1 <= i & i <= ( len y) holds (y /. i) = (( power L) . (((x * ( SgmX (( RelIncl n),( support b)))) /. i),((b * ( SgmX (( RelIncl n),( support b)))) /. i))) by Def1;

      for v be object holds v in {1} implies v in ( dom sg) by A8, TARSKI:def 1;

      then ( dom sg) = ( Seg 1) by A14, FINSEQ_1: 2, TARSKI: 2;

      then

       A24: ( len sg) = 1 by FINSEQ_1:def 3;

      

      then (y . 1) = (y /. 1) by A21, FINSEQ_4: 15

      .= (( power L) . (((x * sg) /. 1),((b * sg) /. 1))) by A21, A23, A24;

      then y = <*(( power L) . ((x . u),(b . u)))*> by A21, A24, A12, A11, FINSEQ_1: 40;

      hence thesis by A22, A13, GROUP_4: 9;

    end;

    

     Lm4: for n be Ordinal, L be right_zeroed add-associative right_complementable well-unital distributive non trivial commutative associative non empty doubleLoopStr, b1,b2 be bag of n, u be object st not (u in ( support b1)) & ( support b2) = (( support b1) \/ {u}) & for u9 be object st u9 <> u holds (b2 . u9) = (b1 . u9) holds for x be Function of n, L holds for a be Element of L st a = (( power L) . ((x . u),(b2 . u))) holds ( eval (b2,x)) = (a * ( eval (b1,x)))

    proof

      let n be Ordinal, L be right_zeroed add-associative right_complementable well-unital distributive commutative associative non trivial doubleLoopStr, b1,b2 be bag of n, u be object;

      assume that

       A1: not u in ( support b1) and

       A2: ( support b2) = (( support b1) \/ {u}) and

       A3: for u9 be object st u9 <> u holds (b2 . u9) = (b1 . u9);

      u in {u} by TARSKI:def 1;

      then

       A4: u in ( support b2) by A2, XBOOLE_0:def 3;

      set sb2 = ( SgmX (( RelIncl n),( support b2))), sb1 = ( SgmX (( RelIncl n),( support b1)));

      let x be Function of n, L;

      

       A5: n = ( dom x) by FUNCT_2:def 1;

      let a be Element of L;

      assume

       A6: a = (( power L) . ((x . u),(b2 . u)));

      ( RelIncl n) linearly_orders ( support b2) by PRE_POLY: 82;

      then u in ( rng sb2) by A4, PRE_POLY:def 2;

      then

      consider k be Nat such that

       A7: k in ( dom sb2) and

       A8: (sb2 . k) = u by FINSEQ_2: 10;

      

       A9: (sb2 /. k) = u by A7, A8, PARTFUN1:def 6;

      reconsider u as Element of n by A4;

      

       A10: ( dom sb2) = ( Seg ( len sb2)) by FINSEQ_1:def 3;

      

       A11: k <= ( len sb2) by A7, FINSEQ_3: 25;

      

       A12: 1 <= k by A7, A10, FINSEQ_1: 1;

      then (1 - 1) <= (k - 1) by XREAL_1: 9;

      then

      reconsider k9 = (k - 1) as Element of NAT by INT_1: 3;

      

       A13: (k9 + 1) = (k + 0 );

      

       A14: ( RelIncl n) linearly_orders ( support b1) by PRE_POLY: 82;

      per cases ;

        suppose

         A15: n = {} ;

        

         A16: b2 in ( Bags n) by PRE_POLY:def 12;

        u in {u} by TARSKI:def 1;

        then u in ( support b2) by A2, XBOOLE_0:def 3;

        then

         A17: (b2 . u) <> 0 by PRE_POLY:def 7;

        ( Bags n) = {( EmptyBag n)} by A15, PRE_POLY: 51;

        then b2 = ( EmptyBag n) by A16, TARSKI:def 1;

        hence thesis by A17;

      end;

        suppose n <> {} ;

        then

        reconsider n9 = n as non empty Ordinal;

        reconsider x9 = x as Function of n9, L;

        reconsider b1, b2 as bag of n9;

        reconsider sb2, sb1 as FinSequence of n9;

        reconsider u as Element of n9;

        consider yb2 be FinSequence of the carrier of L such that

         A18: ( len yb2) = ( len sb2) and

         A19: ( eval (b2,x9)) = ( Product yb2) and

         A20: for i be Element of NAT st 1 <= i & i <= ( len yb2) holds (yb2 /. i) = (( power L) . (((x * sb2) /. i),((b2 * sb2) /. i))) by Def1;

        consider yb1 be FinSequence of the carrier of L such that

         A21: ( len yb1) = ( len sb1) and

         A22: ( eval (b1,x9)) = ( Product yb1) and

         A23: for i be Element of NAT st 1 <= i & i <= ( len yb1) holds (yb1 /. i) = (( power L) . (((x * sb1) /. i),((b1 * sb1) /. i))) by Def1;

        set ytmp = ( Ins (yb1,k9,a));

        

         A24: (( len sb1) + 1) = (( card ( support b1)) + 1) by PRE_POLY: 11, PRE_POLY: 82

        .= ( card ( support b2)) by A1, A2, CARD_2: 41

        .= ( len sb2) by PRE_POLY: 11, PRE_POLY: 82;

        then

         A25: ( len yb2) = ( len ytmp) by A18, A21, FINSEQ_5: 69;

        

         A26: sb2 = ( Ins (sb1,k9,u)) by A1, A2, A7, A9, A13, PRE_POLY: 80, PRE_POLY: 82;

        

         A27: for i be Nat st 1 <= i & i <= ( len yb2) holds (yb2 . i) = (ytmp . i)

        proof

          let i be Nat;

          assume that

           A28: 1 <= i and

           A29: i <= ( len yb2);

          

           A30: i in ( Seg ( len yb2)) by A28, A29, FINSEQ_1: 1;

          then

           A31: (yb2 /. i) = (( power L) . (((x * ( Ins (sb1,k9,u))) /. i),((b2 * ( Ins (sb1,k9,u))) /. i))) by A26, A20, A28, A29;

          

           A32: i in ( dom yb2) by A30, FINSEQ_1:def 3;

          i in ( Seg ( len ytmp)) by A25, A28, A29, FINSEQ_1: 1;

          then

           A33: i in ( dom ytmp) by FINSEQ_1:def 3;

          

           A34: (1 - 1) <= (i - 1) by A28, XREAL_1: 9;

          then

           A35: (i - 1) is Element of NAT by INT_1: 3;

          now

            per cases ;

              case

               A36: i = k;

              

               A37: (sb2 . k) in {u} by A8, TARSKI:def 1;

              then

               A38: k in ( dom (x * sb2)) by A5, A7, A8, FUNCT_1: 11;

              

              then

               A39: ((x * sb2) /. k) = ((x * sb2) . k) by PARTFUN1:def 6

              .= (x . u) by A8, A38, FUNCT_1: 12;

              

               A40: ( support b2) c= ( dom b2) by PRE_POLY: 37;

              (sb2 . k) in ( support b2) by A2, A37, XBOOLE_0:def 3;

              then

               A41: k in ( dom (b2 * sb2)) by A7, A40, FUNCT_1: 11;

              

              then ((b2 * sb2) /. k) = ((b2 * sb2) . k) by PARTFUN1:def 6

              .= (b2 . u) by A8, A41, FUNCT_1: 12;

              then

               A42: (yb2 /. i) = (( power L) . ((x . u),(b2 . u))) by A20, A28, A29, A30, A36, A39;

              

               A43: k9 <= ( len yb1) by A13, A18, A21, A24, A29, A36, XREAL_1: 6;

              (yb2 . i) = (yb2 /. i) by PARTFUN1:def 6, A32;

              hence (ytmp . i) = (yb2 . i) by A6, A13, A36, A43, A42, FINSEQ_5: 73;

            end;

              case

               A44: i <> k;

              ( len ( Ins (sb1,k9,u))) = (( len sb1) + 1) by FINSEQ_5: 69;

              then

               A45: ( dom ( Ins (sb1,k9,u))) = ( Seg (( len sb1) + 1)) by FINSEQ_1:def 3;

              now

                per cases by A44, XXREAL_0: 1;

                  case

                   A46: i < k;

                  then

                   A47: i <= k9 by A13, NAT_1: 13;

                  then

                   A48: i in ( Seg k9) by A28, FINSEQ_1: 1;

                  

                   A49: (yb1 | ( Seg k9)) is FinSequence by FINSEQ_1: 15;

                  k9 <= ( len yb1) by A11, A13, A21, A24, XREAL_1: 6;

                  then

                   W: i in ( dom (yb1 | ( Seg k9))) by A48, A49, FINSEQ_1: 17;

                  then

                   A50: i in ( dom (yb1 | k9)) by FINSEQ_1:def 15;

                  

                   A51: (sb1 | ( Seg k9)) is FinSequence by FINSEQ_1: 15;

                  

                   A52: ( rng sb1) c= n by FINSEQ_1:def 4;

                  

                   A53: i < ( len yb2) by A11, A18, A46, XXREAL_0: 2;

                  then

                   A54: i <= ( len yb1) by A18, A21, A24, NAT_1: 13;

                  

                   ST: i in ( dom yb1) by W, RELAT_1: 57;

                  i <= ( len sb1) by A18, A24, A53, NAT_1: 13;

                  then

                   A55: i in ( dom sb1) by FINSEQ_3: 25, A28;

                  then

                   A56: (sb1 . i) in ( rng sb1) by FUNCT_1:def 3;

                  then

                   A57: i in ( dom (x * sb1)) by A5, A55, A52, FUNCT_1: 11;

                   A58:

                  now

                    assume (sb1 . i) = u;

                    then u in ( rng sb1) by A55, FUNCT_1:def 3;

                    hence contradiction by A1, A14, PRE_POLY:def 2;

                  end;

                  

                   A59: (k - 1) <= ((( len sb1) + 1) - 1) by A11, A24, XREAL_1: 9;

                  

                   A60: ( rng ( Ins (sb1,k9,u))) c= n by FINSEQ_1:def 4;

                  (sb1 . i) in n by A56, A52;

                  then (sb1 . i) in ( dom b1) by PARTFUN1:def 2;

                  then

                   A61: i in ( dom (b1 * sb1)) by A55, FUNCT_1: 11;

                  i in ( Seg k9) by A28, A47, FINSEQ_1: 1;

                  then i in ( dom (sb1 | ( Seg k9))) by A59, A51, FINSEQ_1: 17;

                  then

                   A62: i in ( dom (sb1 | k9)) by FINSEQ_1:def 15;

                  i <= (( len sb1) + 1) by A11, A24, A46, XXREAL_0: 2;

                  then

                   A63: i in ( dom ( Ins (sb1,k9,u))) by A28, A45, FINSEQ_1: 1;

                  then

                   A64: (( Ins (sb1,k9,u)) . i) in ( rng ( Ins (sb1,k9,u))) by FUNCT_1:def 3;

                  then

                   A65: i in ( dom (x * ( Ins (sb1,k9,u)))) by A5, A63, A60, FUNCT_1: 11;

                  

                  then

                   A66: ((x * ( Ins (sb1,k9,u))) /. i) = ((x * ( Ins (sb1,k9,u))) . i) by PARTFUN1:def 6

                  .= (x . (( Ins (sb1,k9,u)) . i)) by A65, FUNCT_1: 12

                  .= (x . (sb1 . i)) by A62, FINSEQ_5: 72

                  .= ((x * sb1) . i) by A57, FUNCT_1: 12

                  .= ((x * sb1) /. i) by A57, PARTFUN1:def 6;

                  ( dom b2) = n by PARTFUN1:def 2;

                  then

                   A67: i in ( dom (b2 * ( Ins (sb1,k9,u)))) by A63, A64, A60, FUNCT_1: 11;

                  

                  then ((b2 * ( Ins (sb1,k9,u))) /. i) = ((b2 * ( Ins (sb1,k9,u))) . i) by PARTFUN1:def 6

                  .= (b2 . (( Ins (sb1,k9,u)) . i)) by A67, FUNCT_1: 12

                  .= (b2 . (sb1 . i)) by A62, FINSEQ_5: 72

                  .= (b1 . (sb1 . i)) by A3, A58

                  .= ((b1 * sb1) . i) by A61, FUNCT_1: 12

                  .= ((b1 * sb1) /. i) by A61, PARTFUN1:def 6;

                  

                  then

                   A68: (yb2 /. i) = (yb1 /. i) by A23, A28, A30, A31, A54, A66

                  .= (yb1 . i) by PARTFUN1:def 6, ST

                  .= (ytmp . i) by A50, FINSEQ_5: 72

                  .= (ytmp /. i) by A33, PARTFUN1:def 6;

                  

                  thus (yb2 . i) = (yb2 /. i) by A32, PARTFUN1:def 6

                  .= (ytmp . i) by A33, A68, PARTFUN1:def 6;

                end;

                  case

                   A69: i > k;

                  reconsider i1 = (i - 1) as Element of NAT by A34, INT_1: 3;

                  

                   A70: ((i - 1) + 1) = (i + 0 );

                  

                   A71: ( rng sb1) c= n by FINSEQ_1:def 4;

                  

                   A72: (i - 1) <= (( len sb2) - 1) by A18, A29, XREAL_1: 9;

                  1 < i by A12, A69, XXREAL_0: 2;

                  then

                   A73: 1 <= (i - 1) by A35, A70, NAT_1: 13;

                  then i1 in ( Seg ( len sb1)) by A24, A72, FINSEQ_1: 1;

                  then

                   A74: i1 in ( dom sb1) by FINSEQ_1:def 3;

                  then

                   A75: (sb1 . i1) in ( rng sb1) by FUNCT_1:def 3;

                  then

                   A76: i1 in ( dom (x * sb1)) by A5, A74, A71, FUNCT_1: 11;

                  ( dom b1) = n by PARTFUN1:def 2;

                  then

                   A77: i1 in ( dom (b1 * sb1)) by A74, A75, A71, FUNCT_1: 11;

                   A78:

                  now

                    assume (sb1 /. i1) = u;

                    then (sb1 . i1) = u by A74, PARTFUN1:def 6;

                    then u in ( rng sb1) by A74, FUNCT_1:def 3;

                    hence contradiction by A1, A14, PRE_POLY:def 2;

                  end;

                  

                   A79: i = (i1 + 1);

                  

                   A80: ( rng ( Ins (sb1,k9,u))) c= n by FINSEQ_1:def 4;

                  

                   A81: (i1 + 1) = (i + 0 );

                  then

                   A82: (k9 + 1) <= i1 by A69, NAT_1: 13;

                  

                   A83: i in ( dom ( Ins (sb1,k9,u))) by A18, A24, A28, A29, A45, FINSEQ_1: 1;

                  then

                   A84: (( Ins (sb1,k9,u)) . i) in ( rng ( Ins (sb1,k9,u))) by FUNCT_1:def 3;

                  then

                   A85: i in ( dom (x * ( Ins (sb1,k9,u)))) by A5, A83, A80, FUNCT_1: 11;

                  

                  then

                   A86: ((x * ( Ins (sb1,k9,u))) /. i) = ((x * ( Ins (sb1,k9,u))) . i) by PARTFUN1:def 6

                  .= (x . (( Ins (sb1,k9,u)) . i)) by A85, FUNCT_1: 12

                  .= (x . (sb1 . i1)) by A24, A72, A81, A82, FINSEQ_5: 74

                  .= ((x * sb1) . i1) by A76, FUNCT_1: 12

                  .= ((x * sb1) /. i1) by A76, PARTFUN1:def 6;

                  

                   W1: 1 <= i1 by A73;

                  i1 <= ( len sb1) by A74, FINSEQ_3: 25;

                  then i1 <= ( len yb1) by A21;

                  then

                   Ze: i1 in ( dom yb1) by W1, FINSEQ_3: 25;

                  ( dom b2) = n by PARTFUN1:def 2;

                  then

                   A87: i in ( dom (b2 * ( Ins (sb1,k9,u)))) by A83, A84, A80, FUNCT_1: 11;

                  

                  then ((b2 * ( Ins (sb1,k9,u))) /. i) = ((b2 * ( Ins (sb1,k9,u))) . i) by PARTFUN1:def 6

                  .= (b2 . (( Ins (sb1,k9,u)) . i)) by A87, FUNCT_1: 12

                  .= (b2 . (sb1 . i1)) by A24, A72, A81, A82, FINSEQ_5: 74

                  .= (b2 . (sb1 /. i1)) by A74, PARTFUN1:def 6

                  .= (b1 . (sb1 /. i1)) by A3, A78

                  .= (b1 . (sb1 . i1)) by A74, PARTFUN1:def 6

                  .= ((b1 * sb1) . i1) by A77, FUNCT_1: 12

                  .= ((b1 * sb1) /. i1) by A77, PARTFUN1:def 6;

                  

                  then

                   A88: (yb2 /. i) = (yb1 /. i1) by A21, A23, A24, A31, A73, A72, A86

                  .= (yb1 . i1) by Ze, PARTFUN1:def 6

                  .= (ytmp . i) by A21, A24, A72, A79, A82, FINSEQ_5: 74

                  .= (ytmp /. i) by A33, PARTFUN1:def 6;

                  

                  thus (yb2 . i) = (yb2 /. i) by A32, PARTFUN1:def 6

                  .= (ytmp . i) by A33, A88, PARTFUN1:def 6;

                end;

              end;

              hence thesis;

            end;

          end;

          hence thesis;

        end;

        ( Product (((yb1 | k9) ^ <*a*>) ^ (yb1 /^ k9))) = (( Product ((yb1 | k9) ^ <*a*>)) * ( Product (yb1 /^ k9))) by GROUP_4: 5

        .= ((( Product (yb1 | k9)) * ( Product <*a*>)) * ( Product (yb1 /^ k9))) by GROUP_4: 5

        .= ((( Product (yb1 | k9)) * ( Product (yb1 /^ k9))) * ( Product <*a*>)) by GROUP_1:def 3

        .= (( Product ((yb1 | k9) ^ (yb1 /^ k9))) * ( Product <*a*>)) by GROUP_4: 5

        .= (( Product yb1) * ( Product <*a*>)) by RFINSEQ: 8

        .= (( eval (b1,x9)) * a) by A22, GROUP_4: 9;

        then ( Product ytmp) = (( eval (b1,x9)) * a) by FINSEQ_5:def 4;

        hence thesis by A19, A25, A27, FINSEQ_1: 14;

      end;

    end;

    

     Lm5: for n be Ordinal, L be right_zeroed add-associative right_complementable Abelian well-unital distributive non trivial commutative associative non empty doubleLoopStr, b1 be bag of n st (ex u be set st ( support b1) = {u}) holds for b2 be bag of n, x be Function of n, L holds ( eval ((b1 + b2),x)) = (( eval (b1,x)) * ( eval (b2,x)))

    proof

      let n be Ordinal, L be right_zeroed add-associative right_complementable well-unital distributive Abelian commutative associative non trivial doubleLoopStr, b1 be bag of n;

      assume ex u be set st ( support b1) = {u};

      then

      consider u be set such that

       A1: ( support b1) = {u};

      let b2 be bag of n, x be Function of n, L;

      

       A2: ( support (b1 + b2)) = (( support b2) \/ {u}) by A1, PRE_POLY: 38;

      

       A3: for u9 be object st u9 <> u holds ((b1 + b2) . u9) = (b2 . u9)

      proof

        let u9 be object;

        assume u9 <> u;

        then

         A4: not u9 in ( support b1) by A1, TARSKI:def 1;

        

        thus ((b1 + b2) . u9) = ((b1 . u9) + (b2 . u9)) by PRE_POLY:def 5

        .= ( 0 + (b2 . u9)) by A4, PRE_POLY:def 7

        .= (b2 . u9);

      end;

      set sb2 = ( SgmX (( RelIncl n),( support b2))), sb1b2 = ( SgmX (( RelIncl n),( support (b1 + b2))));

      

       A5: n c= ( dom x) by FUNCT_2:def 1;

      

       A6: ( RelIncl n) linearly_orders ( support b2) by PRE_POLY: 82;

      consider yb1b2 be FinSequence of the carrier of L such that

       A7: ( len yb1b2) = ( len sb1b2) and

       A8: ( eval ((b1 + b2),x)) = ( Product yb1b2) and

       A9: for i be Element of NAT st 1 <= i & i <= ( len yb1b2) holds (yb1b2 /. i) = (( power L) . (((x * sb1b2) /. i),(((b1 + b2) * sb1b2) /. i))) by Def1;

      consider yb2 be FinSequence of the carrier of L such that

       A10: ( len yb2) = ( len sb2) and

       A11: ( eval (b2,x)) = ( Product yb2) and

       A12: for i be Element of NAT st 1 <= i & i <= ( len yb2) holds (yb2 /. i) = (( power L) . (((x * sb2) /. i),((b2 * sb2) /. i))) by Def1;

      per cases ;

        suppose

         A13: u in ( support b2);

        consider sb2k be Nat such that

         A14: ( dom sb2) = ( Seg sb2k) by FINSEQ_1:def 2;

        

         A15: for v be object holds v in ( support b2) implies v in ( support (b1 + b2))

        proof

          let v be object;

          assume

           A16: v in ( support b2);

          now

            per cases ;

              case u = v;

              then v in {u} by TARSKI:def 1;

              hence thesis by A2, XBOOLE_0:def 3;

            end;

              case u <> v;

              then ((b1 + b2) . v) = (b2 . v) by A3;

              then ((b1 + b2) . v) <> 0 by A16, PRE_POLY:def 7;

              hence thesis by PRE_POLY:def 7;

            end;

          end;

          hence thesis;

        end;

        

         A17: for v be object holds v in ( support (b1 + b2)) implies v in ( support b2)

        proof

          let v be object;

          assume

           A18: v in ( support (b1 + b2));

          now

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

              case v in {u};

              hence thesis by A13, TARSKI:def 1;

            end;

              case v in ( support b2);

              hence thesis;

            end;

          end;

          hence thesis;

        end;

        then

         A19: ( len yb1b2) = ( len yb2) by A7, A10, A15, TARSKI: 2;

        

         A20: ( support (b1 + b2)) = ( support b2) by A17, A15, TARSKI: 2;

        u in ( rng sb2) by A6, A13, PRE_POLY:def 2;

        then

        consider k be Nat such that

         A21: k in ( dom sb2) and

         A22: (sb2 . k) = u by FINSEQ_2: 10;

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

        

         A23: 1 <= k by A21, A14, FINSEQ_1: 1;

        

         A24: ( support b2) c= ( dom b2) by PRE_POLY: 37;

        then

         A25: k in ( dom (b2 * sb2)) by A13, A21, A22, FUNCT_1: 11;

        then ((b2 * sb2) /. k) = ((b2 * sb2) . k) by PARTFUN1:def 6;

        then

         A26: ((b2 * sb2) /. k) = (b2 . u) by A22, A25, FUNCT_1: 12;

        

         A27: ( rng x) c= the carrier of L by RELAT_1:def 19;

        consider sb1b2k be Nat such that

         A28: ( dom sb1b2) = ( Seg sb1b2k) by FINSEQ_1:def 2;

        ( support (b1 + b2)) c= ( dom (b1 + b2)) by PRE_POLY: 37;

        then

         A29: k in ( dom ((b1 + b2) * sb2)) by A13, A20, A21, A22, FUNCT_1: 11;

        

        then

         A30: (((b1 + b2) * sb2) /. k) = (((b1 + b2) * sb2) . k) by PARTFUN1:def 6

        .= ((b1 + b2) . u) by A22, A29, FUNCT_1: 12;

        consider i be Nat such that

         A31: ( dom yb2) = ( Seg i) by FINSEQ_1:def 2;

        reconsider sb2k, sb1b2k as Element of NAT by ORDINAL1:def 12;

        

         A32: k <= sb2k by A21, A14, FINSEQ_1: 1;

        i in NAT by ORDINAL1:def 12;

        then

         A33: ( len yb2) = i by A31, FINSEQ_1:def 3;

        

         A34: sb2k = ( len yb2) by A10, A14, FINSEQ_1:def 3;

        then

         A35: k in ( dom yb2) by A21, A14, FINSEQ_1:def 3;

        reconsider bbS = (b2 * sb2) as PartFunc of NAT , NAT ;

        

         A36: sb2k = ( len sb2) by A14, FINSEQ_1:def 3

        .= ( len sb1b2) by A17, A15, TARSKI: 2

        .= sb1b2k by A28, FINSEQ_1:def 3;

        then ( len yb1b2) = sb2k by A7, A28, FINSEQ_1:def 3;

        

        then

         A37: (yb1b2 /. k) = (( power L) . (((x * sb2) /. k),(((b1 + b2) * sb2) /. k))) by A9, A20, A23, A32

        .= (( power L) . (((x * sb2) /. k),((b1 . u) + (b2 . u)))) by A30, PRE_POLY:def 5

        .= ((( power L) . (((x * sb2) /. k),(b1 . u))) * (( power L) . (((x * sb2) /. k),(bbS /. k)))) by A26, Th1

        .= ((( power L) . (((x * sb2) /. k),(b1 . u))) * (yb2 /. k)) by A12, A23, A32, A34;

        

         A38: ( dom (b1 + b2)) = n by PARTFUN1:def 2;

        

         A39: for i9 be Element of NAT st i9 in ( dom yb2) & i9 <> k holds (yb1b2 /. i9) = (yb2 /. i9)

        proof

          ( rng sb1b2) c= ( dom b2) by A6, A20, A24, PRE_POLY:def 2;

          then

           A40: ( rng sb1b2) c= n by PARTFUN1:def 2;

          

           A41: ( rng sb2) c= ( dom b2) by A6, A24, PRE_POLY:def 2;

          let i9 be Element of NAT ;

          assume that

           A42: i9 in ( dom yb2) and

           A43: i9 <> k;

          

           A44: 1 <= i9 by A31, A42, FINSEQ_1: 1;

          

           A45: i9 in ( dom sb2) by A10, A31, A33, A42, FINSEQ_1:def 3;

          then (sb2 . i9) in ( rng sb2) by FUNCT_1:def 3;

          then

           A46: i9 in ( dom (b2 * sb2)) by A45, A41, FUNCT_1: 11;

          

          then

           A47: ((b2 * sb2) /. i9) = ((b2 * sb2) . i9) by PARTFUN1:def 6

          .= (b2 . (sb2 . i9)) by A46, FUNCT_1: 12

          .= (b2 . (sb2 /. i9)) by A45, PARTFUN1:def 6;

          

           A48: i9 <= ( len yb2) by A31, A33, A42, FINSEQ_1: 1;

          

           A49: i9 in ( Seg sb1b2k) by A36, A34, A42, FINSEQ_1:def 3;

          

           A50: (sb1b2 /. i9) <> u

          proof

            assume (sb1b2 /. i9) = u;

            then

             A51: (sb1b2 . i9) = u by A28, A49, PARTFUN1:def 6;

            

             A52: sb1b2 is one-to-one by PRE_POLY: 10, PRE_POLY: 82;

            (sb1b2 . k) = u by A17, A15, A22, TARSKI: 2;

            hence thesis by A21, A14, A28, A36, A43, A49, A51, A52, FUNCT_1:def 4;

          end;

          (sb1b2 . i9) in ( rng sb1b2) by A28, A49, FUNCT_1:def 3;

          then

           A53: i9 in ( dom ((b1 + b2) * sb1b2)) by A28, A38, A49, A40, FUNCT_1: 11;

          

          then (((b1 + b2) * sb1b2) /. i9) = (((b1 + b2) * sb1b2) . i9) by PARTFUN1:def 6

          .= ((b1 + b2) . (sb1b2 . i9)) by A53, FUNCT_1: 12

          .= ((b1 + b2) . (sb1b2 /. i9)) by A28, A49, PARTFUN1:def 6;

          

          hence (yb1b2 /. i9) = (( power L) . (((x * sb1b2) /. i9),((b1 + b2) . (sb1b2 /. i9)))) by A9, A19, A44, A48

          .= (( power L) . (((x * sb2) /. i9),(b2 . (sb2 /. i9)))) by A3, A20, A50

          .= (yb2 /. i9) by A12, A44, A48, A47;

        end;

        

         A54: ( support b1) c= ( dom b1) by PRE_POLY: 37;

        u in ( support b1) by A1, TARSKI:def 1;

        then

         A55: u in ( dom b1) by A54;

        

         A56: ( dom b1) = n by PARTFUN1:def 2;

        then (x . u) in ( rng x) by A5, A55, FUNCT_1:def 3;

        then

        reconsider xu = (x . u) as Element of L by A27;

        consider a be Element of L such that

         A57: a = (( power L) . (xu,(b1 . u)));

        

         A58: k in ( dom (x * sb2)) by A5, A21, A22, A55, A56, FUNCT_1: 11;

        then ((x * sb2) . k) = (x . (sb2 . k)) by FUNCT_1: 12;

        then (yb1b2 /. k) = (a * (yb2 /. k)) by A22, A37, A57, A58, PARTFUN1:def 6;

        

        hence ( eval ((b1 + b2),x)) = (a * ( Product yb2)) by A8, A19, A35, A39, Th5

        .= (( eval (b1,x)) * ( eval (b2,x))) by A1, A11, A57, Th7;

      end;

        suppose

         A59: not u in ( support b2);

        

         A60: ( support b1) c= ( dom b1) by PRE_POLY: 37;

        u in ( support b1) by A1, TARSKI:def 1;

        then

         A61: u in ( dom b1) by A60;

        

         A62: ( rng x) c= the carrier of L by RELAT_1:def 19;

        ( dom b1) = n by PARTFUN1:def 2;

        then (x . u) in ( rng x) by A5, A61, FUNCT_1:def 3;

        then

        reconsider xu = (x . u) as Element of L by A62;

        consider a be Element of L such that

         A63: a = (( power L) . (xu,((b1 + b2) . u)));

        

         A64: ((b1 + b2) . u) = ((b1 . u) + (b2 . u)) by PRE_POLY:def 5

        .= ((b1 . u) + 0 ) by A59, PRE_POLY:def 7;

        

        thus ( eval ((b1 + b2),x)) = (a * ( eval (b2,x))) by A3, A2, A59, A63, Lm4

        .= (( eval (b1,x)) * ( eval (b2,x))) by A1, A64, A63, Th7;

      end;

    end;

    theorem :: POLYNOM2:16

    

     Th8: for n be Ordinal, L be right_zeroed add-associative right_complementable well-unital distributive Abelian non trivial commutative associative non empty doubleLoopStr, b1,b2 be bag of n, x be Function of n, L holds ( eval ((b1 + b2),x)) = (( eval (b1,x)) * ( eval (b2,x)))

    proof

      let n be Ordinal, L be right_zeroed add-associative right_complementable well-unital distributive Abelian commutative associative non trivial doubleLoopStr, b1,b2 be bag of n, x be Function of n, L;

      defpred P[ Nat] means for b1 be bag of n st ( card ( support b1)) = $1 holds ( eval ((b1 + b2),x)) = (( eval (b1,x)) * ( eval (b2,x)));

      

       A1: ex k be Element of NAT st ( card ( support b1)) = k;

      

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

      proof

        let k be Nat;

        assume

         A3: P[k];

        let b1 be bag of n;

        assume

         A4: ( card ( support b1)) = (k + 1);

        set sgb1 = ( SgmX (( RelIncl n),( support b1)));

        set bg = (sgb1 /. ( len sgb1));

        

         A5: ( RelIncl n) linearly_orders ( support b1) by PRE_POLY: 82;

        then sgb1 <> {} by A4, CARD_1: 27, PRE_POLY:def 2, RELAT_1: 38;

        then 1 <= ( len sgb1) by NAT_1: 14;

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

        then

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

        then (sgb1 /. ( len sgb1)) = (sgb1 . ( len sgb1)) by PARTFUN1:def 6;

        then bg in ( rng sgb1) by A6, FUNCT_1:def 3;

        then

         A7: bg in ( support b1) by A5, PRE_POLY:def 2;

        set b19 = (b1 +* (bg, 0 ));

        ( support b1) c= ( dom b1) by PRE_POLY: 37;

        then

         A8: b19 = (b1 +* (bg .--> 0 )) by A7, FUNCT_7:def 3;

        

         A9: for u be object holds u in ( support b1) implies u in (( support b19) \/ {bg})

        proof

          let u be object;

          assume u in ( support b1);

          then

           A10: (b1 . u) <> 0 by PRE_POLY:def 7;

          per cases ;

            suppose u = bg;

            then u in {bg} by TARSKI:def 1;

            hence thesis by XBOOLE_0:def 3;

          end;

            suppose u <> bg;

            then not u in {bg} by TARSKI:def 1;

            then not u in ( dom (bg .--> 0 ));

            then (b19 . u) = (b1 . u) by A8, FUNCT_4: 11;

            then u in ( support b19) by A10, PRE_POLY:def 7;

            hence thesis by XBOOLE_0:def 3;

          end;

        end;

        bg in {bg} by TARSKI:def 1;

        then bg in ( dom (bg .--> 0 ));

        then (b19 . bg) = ((bg .--> 0 ) . bg) by A8, FUNCT_4: 13;

        then

         A11: (b19 . bg) = 0 by FUNCOP_1: 72;

        then

         A12: not bg in ( support b19) by PRE_POLY:def 7;

        for u be object holds u in (( support b19) \/ {bg}) implies u in ( support b1)

        proof

          let u be object;

          assume

           A13: u in (( support b19) \/ {bg});

          per cases by A13, XBOOLE_0:def 3;

            suppose

             A14: u in ( support b19);

            then u <> bg by A11, PRE_POLY:def 7;

            then not u in {bg} by TARSKI:def 1;

            then not u in ( dom (bg .--> 0 ));

            then

             A15: (b19 . u) = (b1 . u) by A8, FUNCT_4: 11;

            (b19 . u) <> 0 by A14, PRE_POLY:def 7;

            hence thesis by A15, PRE_POLY:def 7;

          end;

            suppose u in {bg};

            hence thesis by A7, TARSKI:def 1;

          end;

        end;

        then ( support b1) = (( support b19) \/ {bg}) by A9, TARSKI: 2;

        then

         A16: (k + 1) = (( card ( support b19)) + 1) by A4, A12, CARD_2: 41;

        set m = (( EmptyBag n) +* (bg,(b1 . bg)));

        

         A17: ( dom b1) = n by PARTFUN1:def 2;

        ( dom ( EmptyBag n)) = n by PARTFUN1:def 2;

        then

         A18: m = (( EmptyBag n) +* (bg .--> (b1 . bg))) by A7, FUNCT_7:def 3;

        

         A19: for u be object holds u in ( support m) implies u in {bg}

        proof

          let u be object;

          assume u in ( support m);

          then

           A20: (m . u) <> 0 by PRE_POLY:def 7;

          now

            assume u <> bg;

            then not u in {bg} by TARSKI:def 1;

            then not u in ( dom (bg .--> (b1 . bg)));

            then (m . u) = (( EmptyBag n) . u) by A18, FUNCT_4: 11;

            hence contradiction by A20;

          end;

          hence thesis by TARSKI:def 1;

        end;

        

         A21: (b1 . bg) <> 0 by A7, PRE_POLY:def 7;

        for u be object holds u in {bg} implies u in ( support m)

        proof

          let u be object;

          bg in {bg} by TARSKI:def 1;

          then bg in ( dom (bg .--> (b1 . bg)));

          then (m . bg) = ((bg .--> (b1 . bg)) . bg) by A18, FUNCT_4: 13;

          then

           A22: (m . bg) = (b1 . bg) by FUNCOP_1: 72;

          assume u in {bg};

          then u = bg by TARSKI:def 1;

          hence thesis by A21, A22, PRE_POLY:def 7;

        end;

        then

         A23: ( support m) = {bg} by A19, TARSKI: 2;

        

         A24: for u be object st u in n holds ((b19 + m) . u) = (b1 . u)

        proof

          let u be object;

          assume u in n;

          per cases ;

            suppose

             A25: u = bg;

            bg in {bg} by TARSKI:def 1;

            then bg in ( dom (bg .--> (b1 . bg)));

            then (m . bg) = ((bg .--> (b1 . bg)) . bg) by A18, FUNCT_4: 13;

            then

             A26: (m . bg) = (b1 . bg) by FUNCOP_1: 72;

            u in {bg} by A25, TARSKI:def 1;

            then u in ( dom (bg .--> 0 ));

            then

             A27: (b19 . u) = ((bg .--> 0 ) . bg) by A8, A25, FUNCT_4: 13;

            ((b19 + m) . u) = ((b19 . u) + (m . u)) by PRE_POLY:def 5

            .= ( 0 + (b1 . bg)) by A25, A27, A26, FUNCOP_1: 72

            .= (b1 . bg);

            hence thesis by A25;

          end;

            suppose u <> bg;

            then

             A28: not u in {bg} by TARSKI:def 1;

            then

             A29: not u in ( dom (bg .--> 0 ));

             not u in ( dom (bg .--> (b1 . bg))) by A28;

            then (m . u) = (( EmptyBag n) . u) by A18, FUNCT_4: 11;

            then

             A30: (m . u) = 0 ;

            ((b19 + m) . u) = ((b19 . u) + (m . u)) by PRE_POLY:def 5

            .= (b1 . u) by A8, A29, A30, FUNCT_4: 11;

            hence thesis;

          end;

        end;

        

         A31: ( dom (b19 + m)) = n by PARTFUN1:def 2;

        

        then ( eval (b1,x)) = ( eval ((m + b19),x)) by A17, A24, FUNCT_1: 2

        .= (( eval (b19,x)) * ( eval (m,x))) by A23, Lm5;

        

        hence (( eval (b1,x)) * ( eval (b2,x))) = ((( eval (b19,x)) * ( eval (b2,x))) * ( eval (m,x))) by GROUP_1:def 3

        .= (( eval ((b19 + b2),x)) * ( eval (m,x))) by A3, A16

        .= ( eval ((m + (b19 + b2)),x)) by A23, Lm5

        .= ( eval (((b19 + m) + b2),x)) by PRE_POLY: 35

        .= ( eval ((b1 + b2),x)) by A31, A17, A24, FUNCT_1: 2;

      end;

      

       A32: P[ 0 ]

      proof

        let b1 be bag of n;

        assume ( card ( support b1)) = 0 ;

        then ( support b1) = {} ;

        then

         A33: b1 = ( EmptyBag n) by PRE_POLY: 81;

        

        hence ( eval ((b1 + b2),x)) = (( 1. L) * ( eval (b2,x))) by PRE_POLY: 53

        .= (( eval (b1,x)) * ( eval (b2,x))) by A33, Th6;

      end;

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

      hence thesis by A1;

    end;

    begin

    registration

      let n be Ordinal, L be add-associative right_zeroed right_complementable non empty addLoopStr, p,q be Polynomial of n, L;

      cluster (p - q) -> finite-Support;

      coherence

      proof

        (p - q) = (p + ( - q)) by POLYNOM1:def 7;

        hence thesis;

      end;

    end

    theorem :: POLYNOM2:17

    

     Th9: for L be right_zeroed add-associative right_complementable well-unital distributive non trivial doubleLoopStr, n be Ordinal, p be Polynomial of n, L st ( Support p) = {} holds p = ( 0_ (n,L))

    proof

      let L be right_zeroed add-associative right_complementable well-unital distributive non trivial doubleLoopStr, n be Ordinal, p be Polynomial of n, L such that

       A1: ( Support p) = {} ;

      

       A2: for u be object st u in ( Bags n) holds (p . u) = (( 0_ (n,L)) . u)

      proof

        let u be object;

        assume

         A3: u in ( Bags n);

        then

        reconsider b = u as bag of n;

        (p . b) = ( 0. L) by A1, A3, POLYNOM1:def 4;

        hence thesis by POLYNOM1: 22;

      end;

      

       A4: ( Bags n) = ( dom ( 0_ (n,L))) by FUNCT_2:def 1;

      ( Bags n) = ( dom p) by FUNCT_2:def 1;

      hence thesis by A4, A2, FUNCT_1: 2;

    end;

    registration

      let n be Ordinal, L be right_zeroed add-associative right_complementable well-unital distributive non trivial doubleLoopStr, p be Polynomial of n, L;

      cluster ( Support p) -> finite;

      coherence by POLYNOM1:def 5;

    end

    theorem :: POLYNOM2:18

    

     Th10: for n be Ordinal, L be right_zeroed add-associative right_complementable well-unital distributive non trivial doubleLoopStr, p be Polynomial of n, L holds ( BagOrder n) linearly_orders ( Support p)

    proof

      let n be Ordinal, L be right_zeroed add-associative right_complementable well-unital distributive non trivial doubleLoopStr, p be Polynomial of n, L;

      set R = ( BagOrder n);

      R is connected by ORDERS_1:def 6;

      then

       A1: R is_connected_in ( field R) by RELAT_2:def 14;

      for x be object holds x in ( Bags n) implies x in ( field R)

      proof

        let x be object;

        assume x in ( Bags n);

        then

        reconsider x as bag of n;

        ( EmptyBag n) <=' x by PRE_POLY: 60;

        then [( EmptyBag n), x] in R by PRE_POLY:def 14;

        then

         A2: x in ( rng R) by XTUPLE_0:def 13;

        ( field R) = (( dom R) \/ ( rng R)) by RELAT_1:def 6;

        then ( rng R) c= ( field R) by XBOOLE_1: 7;

        hence thesis by A2;

      end;

      then

       A3: ( Bags n) c= ( field R) by TARSKI:def 3;

      then [:( Bags n), ( Bags n):] c= [:( field R), ( field R):] by ZFMISC_1: 96;

      then

      reconsider R9 = R as Relation of ( field R) by XBOOLE_1: 1;

      R is_reflexive_in ( field R) by RELAT_2:def 9;

      then ( dom R9) = ( field R) by ORDERS_1: 13;

      then

       A4: R9 is total by PARTFUN1:def 2;

      ( Support p) c= ( field R) by A3, XBOOLE_1: 1;

      then

       A5: R9 is_connected_in ( Support p) by A1, A4, Lm2;

      

       A6: R is_antisymmetric_in ( Support p) by Lm1;

      

       A7: R is_transitive_in ( Support p) by Lm1;

      R is_reflexive_in ( Support p) by Lm1;

      hence thesis by A6, A7, A5, ORDERS_1:def 9;

    end;

    definition

      ::$Canceled

      let n be Ordinal, L be right_zeroed add-associative right_complementable well-unital distributive non trivial doubleLoopStr, p be Polynomial of n, L, x be Function of n, L;

      :: POLYNOM2:def4

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

      : Def2: ex y be FinSequence of the carrier of L st ( len y) = ( len ( SgmX (( BagOrder n),( Support p)))) & it = ( Sum y) & for i be Element of NAT st 1 <= i & i <= ( len y) holds (y /. i) = (((p * ( SgmX (( BagOrder n),( Support p)))) /. i) * ( eval ((( SgmX (( BagOrder n),( Support p))) /. i),x)));

      existence

      proof

        set S = ( SgmX (( BagOrder n),( Support p)));

        set l = ( len S);

        defpred P[ Nat, Element of L] means $2 = (((p * S) /. $1) * ( eval ((S /. $1),x)));

        

         A1: for k be Nat st k in ( Seg l) holds ex x be Element of L st P[k, x];

        consider q be FinSequence of the carrier of L such that

         A2: ( dom q) = ( Seg l) & for m be Nat st m in ( Seg l) holds P[m, (q /. m)] from RECDEF_1:sch 17( A1);

        take ( Sum q);

        

         A3: ( len q) = l by A2, FINSEQ_1:def 3;

        for m be Element of NAT st 1 <= m & m <= ( len q) holds (q /. m) = (((p * ( SgmX (( BagOrder n),( Support p)))) /. m) * ( eval ((( SgmX (( BagOrder n),( Support p))) /. m),x))) by A2, A3, FINSEQ_1: 1;

        hence thesis by A3;

      end;

      uniqueness

      proof

        let a,c be Element of L;

        assume that

         A4: ex y1 be FinSequence of the carrier of L st ( len y1) = ( len ( SgmX (( BagOrder n),( Support p)))) & a = ( Sum y1) & for i be Element of NAT st 1 <= i & i <= ( len y1) holds (y1 /. i) = (((p * ( SgmX (( BagOrder n),( Support p)))) /. i) * ( eval ((( SgmX (( BagOrder n),( Support p))) /. i),x))) and

         A5: ex y2 be FinSequence of the carrier of L st ( len y2) = ( len ( SgmX (( BagOrder n),( Support p)))) & c = ( Sum y2) & for i be Element of NAT st 1 <= i & i <= ( len y2) holds (y2 /. i) = (((p * ( SgmX (( BagOrder n),( Support p)))) /. i) * ( eval ((( SgmX (( BagOrder n),( Support p))) /. i),x)));

        consider y1 be FinSequence of the carrier of L such that

         A6: ( len y1) = ( len ( SgmX (( BagOrder n),( Support p)))) and

         A7: a = ( Sum y1) and

         A8: for i be Element of NAT st 1 <= i & i <= ( len y1) holds (y1 /. i) = (((p * ( SgmX (( BagOrder n),( Support p)))) /. i) * ( eval ((( SgmX (( BagOrder n),( Support p))) /. i),x))) by A4;

        consider y2 be FinSequence of the carrier of L such that

         A9: ( len y2) = ( len ( SgmX (( BagOrder n),( Support p)))) and

         A10: c = ( Sum y2) and

         A11: for i be Element of NAT st 1 <= i & i <= ( len y2) holds (y2 /. i) = (((p * ( SgmX (( BagOrder n),( Support p)))) /. i) * ( eval ((( SgmX (( BagOrder n),( Support p))) /. i),x))) by A5;

        for k be Nat st 1 <= k & k <= ( len y1) holds (y1 . k) = (y2 . k)

        proof

          let k be Nat;

          assume that

           A12: 1 <= k and

           A13: k <= ( len y1);

          k in ( Seg ( len y2)) by A6, A9, A12, A13, FINSEQ_1: 1;

          then

           A14: k in ( dom y2) by FINSEQ_1:def 3;

          

           A15: k in ( Seg ( len y1)) by A12, A13, FINSEQ_1: 1;

          then k in ( dom y1) by FINSEQ_1:def 3;

          

          hence (y1 . k) = (y1 /. k) by PARTFUN1:def 6

          .= (((p * ( SgmX (( BagOrder n),( Support p)))) /. k) * ( eval ((( SgmX (( BagOrder n),( Support p))) /. k),x))) by A8, A12, A13, A15

          .= (y2 /. k) by A6, A9, A11, A12, A13, A15

          .= (y2 . k) by A14, PARTFUN1:def 6;

        end;

        hence thesis by A6, A7, A9, A10, FINSEQ_1: 14;

      end;

    end

    theorem :: POLYNOM2:19

    

     Th11: for n be Ordinal, L be right_zeroed add-associative right_complementable well-unital distributive non trivial doubleLoopStr, p be Polynomial of n, L, b be bag of n st ( Support p) = {b} holds for x be Function of n, L holds ( eval (p,x)) = ((p . b) * ( eval (b,x)))

    proof

      let n be Ordinal, L be right_zeroed add-associative right_complementable well-unital distributive non trivial doubleLoopStr, p be Polynomial of n, L, b be bag of n;

      reconsider sp = ( Support p) as finite Subset of ( Bags n);

      set sg = ( SgmX (( BagOrder n),sp));

      

       A1: b in ( Bags n) by PRE_POLY:def 12;

      

       A2: ( dom p) = ( Bags n) by FUNCT_2:def 1;

      

       A3: ( BagOrder n) linearly_orders sp by Th10;

      assume ( Support p) = {b};

      then

       A4: ( rng sg) = {b} by A3, PRE_POLY:def 2;

      then

       A5: b in ( rng sg) by TARSKI:def 1;

      then

       A6: 1 in ( dom sg) by FINSEQ_3: 31;

      then

       A7: (sg /. 1) = (sg . 1) by PARTFUN1:def 6;

      

       A8: for u be object holds u in ( dom sg) implies u in {1}

      proof

        let u be object;

        assume

         A9: u in ( dom sg);

        assume

         A10: not u in {1};

        reconsider u as Element of NAT by A9;

        (sg /. u) = (sg . u) by A9, PARTFUN1:def 6;

        then

         A11: (sg /. u) in ( rng sg) by A9, FUNCT_1:def 3;

        

         A12: u <> 1 by A10, TARSKI:def 1;

        

         A13: 1 < u

        proof

          consider k be Nat such that

           A14: ( dom sg) = ( Seg k) by FINSEQ_1:def 2;

          ( Seg k) = { l where l be Nat : 1 <= l & l <= k } by FINSEQ_1:def 1;

          then ex m9 be Nat st m9 = u & 1 <= m9 & m9 <= k by A9, A14;

          hence thesis by A12, XXREAL_0: 1;

        end;

        (sg /. 1) = (sg . 1) by A5, A9, FINSEQ_3: 31, PARTFUN1:def 6;

        then (sg /. 1) in ( rng sg) by A6, FUNCT_1:def 3;

        

        then (sg /. 1) = b by A4, TARSKI:def 1

        .= (sg /. u) by A4, A11, TARSKI:def 1;

        hence thesis by A3, A6, A9, A13, PRE_POLY:def 2;

      end;

      for u be object holds u in {1} implies u in ( dom sg) by A6, TARSKI:def 1;

      then

       A15: ( dom sg) = ( Seg 1) by A8, FINSEQ_1: 2, TARSKI: 2;

      then

       A16: ( len sg) = 1 by FINSEQ_1:def 3;

      

       A17: (sg . 1) in ( rng sg) by A6, FUNCT_1:def 3;

      then (sg . 1) = b by A4, TARSKI:def 1;

      then 1 in ( dom (p * sg)) by A6, A1, A2, FUNCT_1: 11;

      

      then

       A18: ((p * sg) /. 1) = ((p * sg) . 1) by PARTFUN1:def 6

      .= (p . (sg . 1)) by A6, FUNCT_1: 13

      .= (p . b) by A4, A17, TARSKI:def 1;

      1 in ( dom sg) by A15, FINSEQ_1: 2, TARSKI:def 1;

      then

       A19: (sg /. 1) in ( rng sg) by A7, FUNCT_1:def 3;

      let x be Function of n, L;

      consider y be FinSequence of the carrier of L such that

       A20: ( len y) = ( len ( SgmX (( BagOrder n),( Support p)))) and

       A21: ( eval (p,x)) = ( Sum y) and

       A22: for i be Element of NAT st 1 <= i & i <= ( len y) holds (y /. i) = (((p * ( SgmX (( BagOrder n),( Support p)))) /. i) * ( eval ((( SgmX (( BagOrder n),( Support p))) /. i),x))) by Def2;

      (y . 1) = (y /. 1) by A20, A16, FINSEQ_4: 15

      .= (((p * sg) /. 1) * ( eval ((sg /. 1),x))) by A20, A22, A16

      .= (((p * sg) /. 1) * ( eval (b,x))) by A4, A19, TARSKI:def 1;

      then y = <*((p . b) * ( eval (b,x)))*> by A20, A16, A18, FINSEQ_1: 40;

      hence thesis by A21, RLVECT_1: 44;

    end;

    theorem :: POLYNOM2:20

    

     Th12: for n be Ordinal, L be right_zeroed add-associative right_complementable well-unital distributive non trivial doubleLoopStr, x be Function of n, L holds ( eval (( 0_ (n,L)),x)) = ( 0. L)

    proof

      let n be Ordinal, L be right_zeroed add-associative right_complementable well-unital distributive non trivial doubleLoopStr, x be Function of n, L;

      set 0p = ( 0_ (n,L));

      consider y be FinSequence of the carrier of L such that

       A1: ( len y) = ( len ( SgmX (( BagOrder n),( Support 0p)))) and

       A2: ( Sum y) = ( eval (0p,x)) and for i be Element of NAT st 1 <= i & i <= ( len y) holds (y /. i) = (((0p * ( SgmX (( BagOrder n),( Support 0p)))) /. i) * ( eval ((( SgmX (( BagOrder n),( Support 0p))) /. i),x))) by Def2;

      ( Support 0p) = {}

      proof

        set u = the Element of ( Support 0p);

        assume ( Support 0p) <> {} ;

        then

         A3: u in ( Support 0p);

        then

         A4: u is Element of ( Bags n);

        (0p . u) <> ( 0. L) by A3, POLYNOM1:def 4;

        hence thesis by A4, POLYNOM1: 22;

      end;

      then ( SgmX (( BagOrder n),( Support 0p))) = {} by Th10, PRE_POLY: 76;

      then y = ( <*> the carrier of L) by A1;

      hence thesis by A2, RLVECT_1: 43;

    end;

    theorem :: POLYNOM2:21

    

     Th13: for n be Ordinal, L be right_zeroed add-associative right_complementable well-unital distributive non trivial doubleLoopStr, x be Function of n, L holds ( eval (( 1_ (n,L)),x)) = ( 1. L)

    proof

      let n be Ordinal, L be right_zeroed add-associative right_complementable well-unital distributive non trivial doubleLoopStr, x be Function of n, L;

      set 1p = ( 1_ (n,L));

      

       A1: for u be object holds u in {( EmptyBag n)} implies u in ( Support 1p)

      proof

        let u be object;

        assume

         A2: u in {( EmptyBag n)};

        then

         A3: u = ( EmptyBag n) by TARSKI:def 1;

        reconsider u as Element of ( Bags n) by A2, TARSKI:def 1;

        (1p . u) = ( 1. L) by A3, POLYNOM1: 25;

        then (1p . u) <> ( 0. L);

        hence thesis by POLYNOM1:def 4;

      end;

      reconsider s1p = ( Support 1p) as finite Subset of ( Bags n);

      set sg1p = ( SgmX (( BagOrder n),s1p));

      

       A4: ( BagOrder n) linearly_orders ( Support 1p) by Th10;

      for u be object holds u in ( Support 1p) implies u in {( EmptyBag n)}

      proof

        let u be object;

        assume

         A5: u in ( Support 1p);

        then

        reconsider u as Element of ( Bags n);

        (1p . u) <> ( 0. L) by A5, POLYNOM1:def 4;

        then u = ( EmptyBag n) by POLYNOM1: 25;

        hence thesis by TARSKI:def 1;

      end;

      then

       A6: ( Support 1p) = {( EmptyBag n)} by A1, TARSKI: 2;

      then

       A7: ( rng sg1p) = {( EmptyBag n)} by A4, PRE_POLY:def 2;

      then

       A8: ( EmptyBag n) in ( rng sg1p) by TARSKI:def 1;

      then

       A9: 1 in ( dom sg1p) by FINSEQ_3: 31;

      then (sg1p /. 1) = (sg1p . 1) by PARTFUN1:def 6;

      then (sg1p /. 1) in ( rng sg1p) by A9, FUNCT_1:def 3;

      then

       A10: (sg1p /. 1) = ( EmptyBag n) by A7, TARSKI:def 1;

      

       A11: for u be object holds u in ( dom sg1p) implies u in {1}

      proof

        let u be object;

        assume

         A12: u in ( dom sg1p);

        assume

         A13: not u in {1};

        reconsider u as Element of NAT by A12;

        (sg1p /. u) = (sg1p . u) by A12, PARTFUN1:def 6;

        then

         A14: (sg1p /. u) in ( rng sg1p) by A12, FUNCT_1:def 3;

        

         A15: u <> 1 by A13, TARSKI:def 1;

        

         A16: 1 < u

        proof

          consider k be Nat such that

           A17: ( dom sg1p) = ( Seg k) by FINSEQ_1:def 2;

          ( Seg k) = { m where m be Nat : 1 <= m & m <= k } by FINSEQ_1:def 1;

          then ex m9 be Nat st m9 = u & 1 <= m9 & m9 <= k by A12, A17;

          hence thesis by A15, XXREAL_0: 1;

        end;

        (sg1p /. 1) = (sg1p . 1) by A8, A12, FINSEQ_3: 31, PARTFUN1:def 6;

        then (sg1p /. 1) in ( rng sg1p) by A9, FUNCT_1:def 3;

        

        then (sg1p /. 1) = ( EmptyBag n) by A7, TARSKI:def 1

        .= (sg1p /. u) by A7, A14, TARSKI:def 1;

        hence thesis by A4, A9, A12, A16, PRE_POLY:def 2;

      end;

      

       A18: ( dom 1p) = ( Bags n) by FUNCT_2:def 1;

      

       A19: 1 in ( dom sg1p) by A8, FINSEQ_3: 31;

      

       A20: (sg1p . 1) in ( rng sg1p) by A9, FUNCT_1:def 3;

      then (sg1p . 1) in {( EmptyBag n)} by A6, A4, PRE_POLY:def 2;

      then (sg1p . 1) = ( EmptyBag n) by TARSKI:def 1;

      then 1 in ( dom (1p * sg1p)) by A19, A18, FUNCT_1: 11;

      

      then

       A21: ((1p * sg1p) /. 1) = ((1p * sg1p) . 1) by PARTFUN1:def 6

      .= (1p . (sg1p . 1)) by A9, FUNCT_1: 13

      .= (1p . ( EmptyBag n)) by A7, A20, TARSKI:def 1

      .= ( 1. L) by POLYNOM1: 25;

      consider y be FinSequence of the carrier of L such that

       A22: ( len y) = ( len sg1p) and

       A23: ( Sum y) = ( eval (1p,x)) and

       A24: for i be Element of NAT st 1 <= i & i <= ( len y) holds (y /. i) = (((1p * sg1p) /. i) * ( eval ((sg1p /. i),x))) by Def2;

      for u be object holds u in {1} implies u in ( dom sg1p) by A9, TARSKI:def 1;

      then ( dom sg1p) = ( Seg 1) by A11, FINSEQ_1: 2, TARSKI: 2;

      then

       A25: ( len sg1p) = 1 by FINSEQ_1:def 3;

      

      then (y . 1) = (y /. 1) by A22, FINSEQ_4: 15

      .= (((1p * sg1p) /. 1) * ( eval ((sg1p /. 1),x))) by A25, A22, A24

      .= (((1p * sg1p) /. 1) * ( 1. L)) by A10, Th6

      .= ((1p * sg1p) /. 1);

      then y = <*( 1. L)*> by A25, A22, A21, FINSEQ_1: 40;

      hence thesis by A23, RLVECT_1: 44;

    end;

    theorem :: POLYNOM2:22

    

     Th14: for n be Ordinal, L be right_zeroed add-associative right_complementable well-unital distributive non trivial doubleLoopStr, p be Polynomial of n, L, x be Function of n, L holds ( eval (( - p),x)) = ( - ( eval (p,x)))

    proof

      let n be Ordinal, L be right_zeroed add-associative right_complementable well-unital distributive non trivial doubleLoopStr, p be Polynomial of n, L, x be Function of n, L;

      set mp = ( - p);

      

       A1: for u be object holds u in ( Support p) implies u in ( Support mp)

      proof

        let u be object;

        assume

         A2: u in ( Support p);

        then

        reconsider u as Element of ( Bags n);

        reconsider u as bag of n;

        

         A3: (p . u) <> ( 0. L) by A2, POLYNOM1:def 4;

        (mp . u) <> ( 0. L)

        proof

          assume (mp . u) = ( 0. L);

          then ( - ( - (p . u))) = ( - ( 0. L)) by POLYNOM1: 17;

          then (p . u) = ( - ( 0. L)) by RLVECT_1: 17;

          hence thesis by A3, RLVECT_1: 12;

        end;

        hence thesis by POLYNOM1:def 4;

      end;

      consider ymp be FinSequence of the carrier of L such that

       A4: ( len ymp) = ( len ( SgmX (( BagOrder n),( Support mp)))) and

       A5: ( Sum ymp) = ( eval (mp,x)) and

       A6: for i be Element of NAT st 1 <= i & i <= ( len ymp) holds (ymp /. i) = (((mp * ( SgmX (( BagOrder n),( Support mp)))) /. i) * ( eval ((( SgmX (( BagOrder n),( Support mp))) /. i),x))) by Def2;

      consider yp be FinSequence of the carrier of L such that

       A7: ( len yp) = ( len ( SgmX (( BagOrder n),( Support p)))) and

       A8: ( Sum yp) = ( eval (p,x)) and

       A9: for i be Element of NAT st 1 <= i & i <= ( len yp) holds (yp /. i) = (((p * ( SgmX (( BagOrder n),( Support p)))) /. i) * ( eval ((( SgmX (( BagOrder n),( Support p))) /. i),x))) by Def2;

      

       A10: for u be object holds u in ( Support mp) implies u in ( Support p)

      proof

        let u be object;

        assume

         A11: u in ( Support mp);

        then

        reconsider u as Element of ( Bags n);

        reconsider u as bag of n;

        (mp . u) <> ( 0. L) by A11, POLYNOM1:def 4;

        then ( - (p . u)) <> ( 0. L) by POLYNOM1: 17;

        then (p . u) <> ( 0. L) by RLVECT_1: 12;

        hence thesis by POLYNOM1:def 4;

      end;

      then

       A12: ( len ymp) = ( len yp) by A1, A7, A4, TARSKI: 2;

      

       A13: ( dom (( - ( 1. L)) * yp)) = ( dom yp) by POLYNOM1:def 1;

      consider k be Element of NAT such that

       A14: k = ( len (( - ( 1. L)) * yp));

      consider l be Element of NAT such that

       A15: l = ( len yp);

      

       A16: ( dom (( - ( 1. L)) * yp)) = ( Seg k) by A14, FINSEQ_1:def 3;

      

       A17: ( SgmX (( BagOrder n),( Support p))) = ( SgmX (( BagOrder n),( Support mp))) by A1, A10, TARSKI: 2;

      

       A18: for k be Nat st 1 <= k & k <= ( len ymp) holds (ymp . k) = ((( - ( 1. L)) * yp) . k)

      proof

        let k be Nat;

        assume that

         A19: 1 <= k and

         A20: k <= ( len ymp);

        

         A21: k <= ( len (( - ( 1. L)) * yp)) by A12, A13, A14, A16, A20, FINSEQ_1:def 3;

        

         A22: ((mp * ( SgmX (( BagOrder n),( Support p)))) /. k) = (( - ( 1. L)) * ((p * ( SgmX (( BagOrder n),( Support p)))) /. k))

        proof

          reconsider b = (( SgmX (( BagOrder n),( Support p))) /. k) as bag of n;

          k in ( Seg ( len ( SgmX (( BagOrder n),( Support p))))) by A7, A12, A19, A20, FINSEQ_1: 1;

          then

           A23: k in ( dom ( SgmX (( BagOrder n),( Support p)))) by FINSEQ_1:def 3;

          

           A24: ( dom p) = ( Bags n) by FUNCT_2:def 1;

          then b in ( dom p);

          then

           A25: k in ( dom (p * ( SgmX (( BagOrder n),( Support p))))) by A23, PARTFUN2: 3;

          

           A26: ( dom mp) = ( Bags n) by FUNCT_2:def 1;

          then b in ( dom mp);

          then k in ( dom (mp * ( SgmX (( BagOrder n),( Support p))))) by A23, PARTFUN2: 3;

          

          hence ((mp * ( SgmX (( BagOrder n),( Support p)))) /. k) = (mp /. b) by PARTFUN2: 3

          .= (mp . b) by A26, PARTFUN1:def 6

          .= ( - (p . b)) by POLYNOM1: 17

          .= ( - (( 1. L) * (p /. b))) by A24, PARTFUN1:def 6

          .= (( - ( 1. L)) * (p /. b)) by VECTSP_1: 9

          .= (( - ( 1. L)) * ((p * ( SgmX (( BagOrder n),( Support p)))) /. k)) by A25, PARTFUN2: 3;

        end;

        

         A27: k in ( Seg l) by A12, A15, A19, A20, FINSEQ_1: 1;

        then

         A28: k in ( dom yp) by A15, FINSEQ_1:def 3;

        

        thus (ymp . k) = (ymp /. k) by A19, A20, FINSEQ_4: 15

        .= ((( - ( 1. L)) * ((p * ( SgmX (( BagOrder n),( Support p)))) /. k)) * ( eval ((( SgmX (( BagOrder n),( Support p))) /. k),x))) by A17, A6, A19, A20, A27, A22

        .= (( - (( 1. L) * ((p * ( SgmX (( BagOrder n),( Support p)))) /. k))) * ( eval ((( SgmX (( BagOrder n),( Support p))) /. k),x))) by VECTSP_1: 9

        .= ( - (((p * ( SgmX (( BagOrder n),( Support p)))) /. k) * ( eval ((( SgmX (( BagOrder n),( Support p))) /. k),x)))) by VECTSP_1: 9

        .= ( - (yp /. k)) by A9, A12, A19, A20, A27

        .= ( - (( 1. L) * (yp /. k)))

        .= (( - ( 1. L)) * (yp /. k)) by VECTSP_1: 9

        .= ((( - ( 1. L)) * yp) /. k) by A28, POLYNOM1:def 1

        .= ((( - ( 1. L)) * yp) . k) by A19, A21, FINSEQ_4: 15;

      end;

      ( dom yp) = ( Seg l) by A15, FINSEQ_1:def 3;

      

      hence ( eval (mp,x)) = ( Sum (( - ( 1. L)) * yp)) by A5, A12, A13, A14, A15, A16, A18, FINSEQ_1: 6, FINSEQ_1: 14

      .= (( - ( 1. L)) * ( Sum yp)) by POLYNOM1: 12

      .= ( - (( 1. L) * ( eval (p,x)))) by VECTSP_1: 9, A8

      .= ( - ( eval (p,x)));

    end;

    

     Lm6: for n be Ordinal, L be right_zeroed add-associative right_complementable Abelian well-unital distributive non trivial doubleLoopStr, p,q be Polynomial of n, L, x be Function of n, L, b be bag of n st not (b in ( Support p)) & ( Support q) = (( Support p) \/ {b}) & for b9 be bag of n st b9 <> b holds (q . b9) = (p . b9) holds ( eval (q,x)) = (( eval (p,x)) + ((q . b) * ( eval (b,x))))

    proof

      let n be Ordinal, L be right_zeroed add-associative right_complementable Abelian well-unital distributive non trivial doubleLoopStr, p,q be Polynomial of n, L, x be Function of n, L, b be bag of n;

      assume that

       A1: not b in ( Support p) and

       A2: ( Support q) = (( Support p) \/ {b}) and

       A3: for b9 be bag of n st b9 <> b holds (q . b9) = (p . b9);

      set sq = ( SgmX (( BagOrder n),( Support q))), sp = ( SgmX (( BagOrder n),( Support p)));

      

       A4: ( BagOrder n) linearly_orders ( Support q) by Th10;

      b in {b} by TARSKI:def 1;

      then b in ( Support q) by A2, XBOOLE_0:def 3;

      then b in ( rng sq) by A4, PRE_POLY:def 2;

      then

      consider k be Nat such that

       A5: k in ( dom sq) and

       A6: (sq . k) = b by FINSEQ_2: 10;

      

       A7: (sq /. k) = b by A5, A6, PARTFUN1:def 6;

      reconsider b as Element of ( Bags n) by PRE_POLY:def 12;

      

       A8: ( dom sq) = ( Seg ( len sq)) by FINSEQ_1:def 3;

      then

       A9: k <= ( len sq) by A5, FINSEQ_1: 1;

      1 <= k by A5, A8, FINSEQ_1: 1;

      then (1 - 1) <= (k - 1) by XREAL_1: 9;

      then

      reconsider k9 = (k - 1) as Element of NAT by INT_1: 3;

      

       A10: (k9 + 1) = (k + 0 );

      then

       A11: sq = ( Ins (sp,k9,b)) by A1, A2, A5, A7, Th10, PRE_POLY: 80;

      consider yp be FinSequence of the carrier of L such that

       A12: ( len yp) = ( len sp) and

       A13: ( Sum yp) = ( eval (p,x)) and

       A14: for i be Element of NAT st 1 <= i & i <= ( len yp) holds (yp /. i) = (((p * sp) /. i) * ( eval ((sp /. i),x))) by Def2;

      consider yq be FinSequence of the carrier of L such that

       A15: ( len yq) = ( len sq) and

       A16: ( Sum yq) = ( eval (q,x)) and

       A17: for i be Element of NAT st 1 <= i & i <= ( len yq) holds (yq /. i) = (((q * sq) /. i) * ( eval ((sq /. i),x))) by Def2;

      

       VA: ( dom yq) = ( dom sq) by A15, FINSEQ_3: 29;

      reconsider b as Element of ( Bags n);

      set ytmp = ( Ins (yp,k9,((q . b) * ( eval (b,x)))));

      

       A18: (( len sp) + 1) = (( card ( Support p)) + 1) by Th10, PRE_POLY: 11

      .= ( card ( Support q)) by A1, A2, CARD_2: 41

      .= ( len sq) by Th10, PRE_POLY: 11;

      then

       A19: ( len yq) = ( len ytmp) by A15, A12, FINSEQ_5: 69;

      

       A20: ( BagOrder n) linearly_orders ( Support p) by Th10;

      

       A21: for i be Nat st 1 <= i & i <= ( len yq) holds (yq . i) = (ytmp . i)

      proof

        let i be Nat;

        assume that

         A22: 1 <= i and

         A23: i <= ( len yq);

        

         A24: i in ( dom yq) by A22, A23, FINSEQ_3: 25;

        i in ( Seg ( len ytmp)) by A19, A22, A23, FINSEQ_1: 1;

        then

         A25: i in ( dom ytmp) by FINSEQ_1:def 3;

        per cases ;

          suppose

           A26: i = k;

          ( dom q) = ( Bags n) by FUNCT_2:def 1;

          then (sq . k) in ( dom q) by A6, PRE_POLY:def 12;

          then

           A27: k in ( dom (q * sq)) by A5, FUNCT_1: 11;

          

          then

           A28: ((q * sq) /. k) = ((q * sq) . k) by PARTFUN1:def 6

          .= (q . b) by A6, A27, FUNCT_1: 12;

          

           A29: (yq /. i) = (((q * sq) /. k) * ( eval ((sq /. k),x))) by A5, A17, A22, A23, A26

          .= ((q . b) * ( eval (b,x))) by A5, A6, A28, PARTFUN1:def 6;

          

           A30: k9 <= ( len yp) by A9, A10, A12, A18, XREAL_1: 6;

          

          thus (ytmp . i) = ((q . b) * ( eval (b,x))) by A10, A26, A30, FINSEQ_5: 73

          .= (yq . i) by A24, A29, PARTFUN1:def 6;

        end;

          suppose

           A31: i <> k;

          ( len ( Ins (sp,k9,b))) = (( len sp) + 1) by FINSEQ_5: 69;

          then

           A32: ( dom ( Ins (sp,k9,b))) = ( Seg (( len sp) + 1)) by FINSEQ_1:def 3;

          now

            per cases by A31, XXREAL_0: 1;

              case

               A33: i < k;

              k9 < k by A10, NAT_1: 19;

              then k9 < ( len yq) by A9, A15, XXREAL_0: 2;

              then

               A34: k9 <= ( len yp) by A15, A12, A18, NAT_1: 13;

              

               A35: (yp | ( Seg k9)) is FinSequence by FINSEQ_1: 15;

              

               A36: i <= k9 by A10, A33, NAT_1: 13;

              then i in ( Seg k9) by A22, FINSEQ_1: 1;

              then i in ( dom (yp | ( Seg k9))) by A34, A35, FINSEQ_1: 17;

              then

               A37: i in ( dom (yp | k9)) by FINSEQ_1:def 15;

              

               A38: (k - 1) <= ((( len sp) + 1) - 1) by A9, A18, XREAL_1: 9;

              then

               A39: i <= ( len sp) by A36, XXREAL_0: 2;

              then

               A40: i in ( dom sp) by A22, FINSEQ_3: 25;

               A41:

              now

                assume (sp /. i) = b;

                then (sp . i) = b by A40, PARTFUN1:def 6;

                then b in ( rng sp) by A40, FUNCT_1:def 3;

                hence contradiction by A1, A20, PRE_POLY:def 2;

              end;

              i < ( len yq) by A9, A15, A33, XXREAL_0: 2;

              then

               A42: i <= ( len yp) by A15, A12, A18, NAT_1: 13;

              then

               VV: i in ( dom yp) by FINSEQ_3: 25, A22;

              

               A43: (sp | ( Seg k9)) is FinSequence by FINSEQ_1: 15;

              

               A44: ( rng ( Ins (sp,k9,b))) c= ( Bags n) by FINSEQ_1:def 4;

              

               A45: ( dom q) = ( Bags n) by FUNCT_2:def 1;

              

               A46: ( rng sp) c= ( Bags n) by FINSEQ_1:def 4;

              i in ( Seg k9) by A22, A36, FINSEQ_1: 1;

              then i in ( dom (sp | ( Seg k9))) by A38, A43, FINSEQ_1: 17;

              then

               A47: i in ( dom (sp | k9)) by FINSEQ_1:def 15;

              (sp . i) in ( rng sp) by A40, FUNCT_1:def 3;

              then (sp . i) in ( Bags n) by A46;

              then (sp . i) in ( dom p) by FUNCT_2:def 1;

              then

               A48: i in ( dom (p * sp)) by A40, FUNCT_1: 11;

              ( len sp) <= (( len sp) + 1) by XREAL_1: 29;

              then i <= (( len sp) + 1) by A39, XXREAL_0: 2;

              then

               A49: i in ( dom ( Ins (sp,k9,b))) by A22, A32, FINSEQ_1: 1;

              then (( Ins (sp,k9,b)) . i) in ( rng ( Ins (sp,k9,b))) by FUNCT_1:def 3;

              then

               A50: i in ( dom (q * ( Ins (sp,k9,b)))) by A49, A44, A45, FUNCT_1: 11;

              

              then

               A51: ((q * ( Ins (sp,k9,b))) . i) = (q . (( Ins (sp,k9,b)) . i)) by FUNCT_1: 12

              .= (q . (sp . i)) by A47, FINSEQ_5: 72

              .= (q . (sp /. i)) by A40, PARTFUN1:def 6

              .= (p . (sp /. i)) by A3, A41

              .= (p . (sp . i)) by A40, PARTFUN1:def 6

              .= ((p * sp) . i) by A48, FUNCT_1: 12;

              i in ( dom (q * sq)) by A50, A11;

              then

               Z: ((q * sq) /. i) = ((q * sq) . i) & ((p * sp) /. i) = ((p * sp) . i) by A48, PARTFUN1:def 6;

              i in ( dom sq) by A24, VA;

              then

               Z1: (sq /. i) = (sq . i) & (sp /. i) = (sp . i) by A40, PARTFUN1:def 6;

              

               A52: (yq /. i) = (((q * sq) /. i) * ( eval ((sq /. i),x))) by A17, A22, A23, A49

              .= (((p * sp) /. i) * ( eval ((sp /. i),x))) by A11, A47, A51, FINSEQ_5: 72, Z, Z1

              .= (yp /. i) by A14, A22, A49, A42

              .= (yp . i) by PARTFUN1:def 6, VV

              .= (ytmp . i) by A37, FINSEQ_5: 72

              .= (ytmp /. i) by A25, PARTFUN1:def 6;

              

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

              .= (ytmp . i) by A25, A52, PARTFUN1:def 6;

            end;

              case

               A53: i > k;

              then (i - 1) > k9 by XREAL_1: 9;

              then

              reconsider i1 = (i - 1) as Element of NAT by INT_1: 3;

              

               A54: ((i - 1) + 1) = (i + 0 );

              then

               A55: (k9 + 1) <= i1 by A53, NAT_1: 13;

              

               A56: ( dom q) = ( Bags n) by FUNCT_2:def 1;

              

               A57: ( rng ( Ins (sp,k9,b))) c= ( Bags n) by FINSEQ_1:def 4;

              

               A58: ( dom p) = ( Bags n) by FUNCT_2:def 1;

              

               A59: ( rng sp) c= ( Bags n) by FINSEQ_1:def 4;

              

               A60: (i - 1) <= ((( len yp) + 1) - 1) by A15, A12, A18, A23, XREAL_1: 9;

              ( 0 + 1) <= (k9 + 1) by XREAL_1: 6;

              then 1 < i by A53, XXREAL_0: 2;

              then

               A61: 1 <= i1 by A54, NAT_1: 13;

              then i1 in ( Seg ( len sp)) by A12, A60, FINSEQ_1: 1;

              then

               A62: i1 in ( dom sp) by FINSEQ_1:def 3;

              ( dom yp) = ( dom sp) by A12, FINSEQ_3: 29;

              then

               AA: i1 in ( dom yp) by A62;

               A63:

              now

                assume (sp /. i1) = b;

                then (sp . i1) = b by A62, PARTFUN1:def 6;

                then b in ( rng sp) by A62, FUNCT_1:def 3;

                hence contradiction by A1, A20, PRE_POLY:def 2;

              end;

              (sp . i1) in ( rng sp) by A62, FUNCT_1:def 3;

              then

               A64: i1 in ( dom (p * sp)) by A62, A59, A58, FUNCT_1: 11;

              

               A65: i = (i1 + 1);

              

               A66: i in ( dom ( Ins (sp,k9,b))) by A15, A18, A22, A23, A32, FINSEQ_1: 1;

              then (( Ins (sp,k9,b)) . i) in ( rng ( Ins (sp,k9,b))) by FUNCT_1:def 3;

              then

               A67: i in ( dom (q * ( Ins (sp,k9,b)))) by A66, A57, A56, FUNCT_1: 11;

              

              then

               A68: ((q * ( Ins (sp,k9,b))) . i) = (q . (( Ins (sp,k9,b)) . i)) by FUNCT_1: 12

              .= (q . (sp . i1)) by A12, A60, A65, A55, FINSEQ_5: 74

              .= (q . (sp /. i1)) by A62, PARTFUN1:def 6

              .= (p . (sp /. i1)) by A3, A63

              .= (p . (sp . i1)) by A62, PARTFUN1:def 6

              .= ((p * sp) . i1) by A64, FUNCT_1: 12;

              

               BB: ( dom yq) = ( dom sq) by FINSEQ_3: 29, A15;

              

               SS: ((q * sq) /. i) = ((q * sq) . i) by A67, PARTFUN1:def 6, A11

              .= ((p * sp) /. i1) by A64, PARTFUN1:def 6, A68, A11;

              

               SA: (sq /. i) = (sq . i) by A24, BB, PARTFUN1:def 6

              .= (sp . i1) by A12, A60, A65, A55, A11, FINSEQ_5: 74

              .= (sp /. i1) by PARTFUN1:def 6, A62;

              

               A69: (yq /. i) = (((q * sq) /. i) * ( eval ((sq /. i),x))) by A17, A22, A23, A66

              .= (yp /. i1) by A14, A60, A61, SS, SA

              .= (yp . i1) by PARTFUN1:def 6, AA

              .= (ytmp . i) by A60, A65, A55, FINSEQ_5: 74

              .= (ytmp /. i) by PARTFUN1:def 6, A25;

              

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

              .= (ytmp . i) by A25, A69, PARTFUN1:def 6;

            end;

          end;

          hence thesis;

        end;

      end;

      ( Sum (((yp | k9) ^ <*((q . b) * ( eval (b,x)))*>) ^ (yp /^ k9))) = (( Sum ((yp | k9) ^ <*((q . b) * ( eval (b,x)))*>)) + ( Sum (yp /^ k9))) by RLVECT_1: 41

      .= ((( Sum (yp | k9)) + ( Sum <*((q . b) * ( eval (b,x)))*>)) + ( Sum (yp /^ k9))) by RLVECT_1: 41

      .= ((( Sum (yp | k9)) + ( Sum (yp /^ k9))) + ( Sum <*((q . b) * ( eval (b,x)))*>)) by RLVECT_1:def 3

      .= (( Sum ((yp | k9) ^ (yp /^ k9))) + ( Sum <*((q . b) * ( eval (b,x)))*>)) by RLVECT_1: 41

      .= (( Sum yp) + ( Sum <*((q . b) * ( eval (b,x)))*>)) by RFINSEQ: 8

      .= (( eval (p,x)) + ((q . b) * ( eval (b,x)))) by A13, RLVECT_1: 44;

      then ( Sum ytmp) = (( eval (p,x)) + ((q . b) * ( eval (b,x)))) by FINSEQ_5:def 4;

      hence thesis by A16, A19, A21, FINSEQ_1: 14;

    end;

    

     Lm7: for n be Ordinal, L be right_zeroed add-associative right_complementable Abelian well-unital distributive non trivial doubleLoopStr, p be Polynomial of n, L st (ex b be bag of n st ( Support p) = {b}) holds for q be Polynomial of n, L, x be Function of n, L holds ( eval ((p + q),x)) = (( eval (p,x)) + ( eval (q,x)))

    proof

      let n be Ordinal, L be right_zeroed add-associative right_complementable well-unital distributive Abelian non trivial doubleLoopStr, p be Polynomial of n, L;

      assume ex b be bag of n st ( Support p) = {b};

      then

      consider b be bag of n such that

       A1: ( Support p) = {b};

      b in ( Support p) by A1, TARSKI:def 1;

      then

       A2: (p . b) <> ( 0. L) by POLYNOM1:def 4;

      let q be Polynomial of n, L, x be Function of n, L;

      

       A3: for b9 be bag of n st b9 <> b holds ((p + q) . b9) = (q . b9)

      proof

        let b9 be bag of n;

        

         A4: b9 is Element of ( Bags n) by PRE_POLY:def 12;

        assume b9 <> b;

        then

         A5: not b9 in ( Support p) by A1, TARSKI:def 1;

        

        thus ((p + q) . b9) = ((p . b9) + (q . b9)) by POLYNOM1: 15

        .= (( 0. L) + (q . b9)) by A5, A4, POLYNOM1:def 4

        .= (q . b9) by RLVECT_1:def 4;

      end;

      set sq = ( SgmX (( BagOrder n),( Support q))), spq = ( SgmX (( BagOrder n),( Support (p + q))));

      

       A6: b is Element of ( Bags n) by PRE_POLY:def 12;

      

       A7: ( Support (p + q)) c= (( Support p) \/ ( Support q)) by POLYNOM1: 20;

      consider yq be FinSequence of the carrier of L such that

       A8: ( len yq) = ( len sq) and

       A9: ( eval (q,x)) = ( Sum yq) and

       A10: for i be Element of NAT st 1 <= i & i <= ( len yq) holds (yq /. i) = (((q * sq) /. i) * ( eval ((sq /. i),x))) by Def2;

      consider ypq be FinSequence of the carrier of L such that

       A11: ( len ypq) = ( len spq) and

       A12: ( eval ((p + q),x)) = ( Sum ypq) and

       A13: for i be Element of NAT st 1 <= i & i <= ( len ypq) holds (ypq /. i) = ((((p + q) * spq) /. i) * ( eval ((spq /. i),x))) by Def2;

      

       A14: ( BagOrder n) linearly_orders ( Support q) by Th10;

      now

        per cases ;

          case

           A15: b in ( Support q);

          now

            per cases ;

              case

               A16: (p . b) = ( - (q . b));

              

               A17: for u be object holds u in ( Support q) implies u in (( Support (p + q)) \/ {b})

              proof

                let u be object;

                assume

                 A18: u in ( Support q);

                then

                reconsider u as bag of n;

                per cases ;

                  suppose u = b;

                  then u in {b} by TARSKI:def 1;

                  hence thesis by XBOOLE_0:def 3;

                end;

                  suppose u <> b;

                  then ((p + q) . u) = (q . u) by A3;

                  then

                   A19: ((p + q) . u) <> ( 0. L) by A18, POLYNOM1:def 4;

                  u is Element of ( Bags n) by PRE_POLY:def 12;

                  then u in ( Support (p + q)) by A19, POLYNOM1:def 4;

                  hence thesis by XBOOLE_0:def 3;

                end;

              end;

              ((p + q) . b) = ((p . b) + (q . b)) by POLYNOM1: 15

              .= ( 0. L) by A16, RLVECT_1: 5;

              then

               A20: not b in ( Support (p + q)) by POLYNOM1:def 4;

              for u be object holds u in (( Support (p + q)) \/ {b}) implies u in ( Support q)

              proof

                let u be object;

                assume

                 A21: u in (( Support (p + q)) \/ {b});

                per cases by A21, XBOOLE_0:def 3;

                  suppose

                   A22: u in ( Support (p + q));

                  then not u in {b} by A20, TARSKI:def 1;

                  hence thesis by A1, A7, A22, XBOOLE_0:def 3;

                end;

                  suppose u in {b};

                  hence thesis by A15, TARSKI:def 1;

                end;

              end;

              then

               A23: (( Support (p + q)) \/ {b}) = ( Support q) by A17, TARSKI: 2;

              

              thus ( eval ((p + q),x)) = (( eval ((p + q),x)) + ( 0. L)) by RLVECT_1:def 4

              .= (( eval ((p + q),x)) + (((q . b) * ( eval (b,x))) + ( - ((q . b) * ( eval (b,x)))))) by RLVECT_1: 5

              .= ((( eval ((p + q),x)) + ((q . b) * ( eval (b,x)))) + ( - ((q . b) * ( eval (b,x))))) by RLVECT_1:def 3

              .= (( eval (q,x)) + ( - ((q . b) * ( eval (b,x))))) by A3, A20, A23, Lm6

              .= (( eval (q,x)) + ((p . b) * ( eval (b,x)))) by A16, VECTSP_1: 9

              .= (( eval (q,x)) + ( eval (p,x))) by A1, Th11;

            end;

              case

               A24: (p . b) <> ( - (q . b));

              ((p . b) + (q . b)) <> (( - (q . b)) + (q . b))

              proof

                assume

                 A25: ((p . b) + (q . b)) = (( - (q . b)) + (q . b));

                (p . b) = ((p . b) + ( 0. L)) by RLVECT_1:def 4

                .= ((p . b) + ((q . b) + ( - (q . b)))) by RLVECT_1: 5

                .= ((( - (q . b)) + (q . b)) + ( - (q . b))) by A25, RLVECT_1:def 3

                .= (( 0. L) + ( - (q . b))) by RLVECT_1: 5

                .= ( - (q . b)) by RLVECT_1:def 4;

                hence thesis by A24;

              end;

              then ((p . b) + (q . b)) <> ( 0. L) by RLVECT_1: 5;

              then

               A26: ((p + q) . b) <> ( 0. L) by POLYNOM1: 15;

              

               A27: for u be object holds u in ( Support q) implies u in ( Support (p + q))

              proof

                let u be object;

                assume

                 A28: u in ( Support q);

                then

                reconsider u as bag of n;

                per cases ;

                  suppose u = b;

                  hence thesis by A6, A26, POLYNOM1:def 4;

                end;

                  suppose u <> b;

                  then ((p + q) . u) = (q . u) by A3;

                  then

                   A29: ((p + q) . u) <> ( 0. L) by A28, POLYNOM1:def 4;

                  u is Element of ( Bags n) by PRE_POLY:def 12;

                  hence thesis by A29, POLYNOM1:def 4;

                end;

              end;

              

               A30: for u be object holds u in ( Support (p + q)) implies u in ( Support q)

              proof

                let u be object;

                assume

                 A31: u in ( Support (p + q));

                then

                reconsider u as bag of n;

                per cases by A7, A31, XBOOLE_0:def 3;

                  suppose u in ( Support p);

                  hence thesis by A1, A15, TARSKI:def 1;

                end;

                  suppose u in ( Support q);

                  hence thesis;

                end;

              end;

              then

               A32: ( Support (p + q)) = ( Support q) by A27, TARSKI: 2;

              

               A33: ( len ypq) = ( len yq) by A11, A8, A30, A27, TARSKI: 2;

              consider spqk be Nat such that

               A34: ( dom spq) = ( Seg spqk) by FINSEQ_1:def 2;

              b in ( rng sq) by A14, A15, PRE_POLY:def 2;

              then

              consider k be Nat such that

               A35: k in ( dom sq) and

               A36: (sq . k) = b by FINSEQ_2: 10;

              consider sqk be Nat such that

               A37: ( dom sq) = ( Seg sqk) by FINSEQ_1:def 2;

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

              reconsider k, sqk, spqk as Element of NAT by ORDINAL1:def 12;

              

               A38: 1 <= k by A35, A37, FINSEQ_1: 1;

              

               A39: ( dom (p + q)) = ( Bags n) by FUNCT_2:def 1;

              then (sq . k) in ( dom (p + q)) by A36, PRE_POLY:def 12;

              then

               A40: k in ( dom ((p + q) * sq)) by A35, FUNCT_1: 11;

              

              then

               A41: (((p + q) * sq) /. k) = (((p + q) * sq) . k) by PARTFUN1:def 6

              .= ((p + q) . b) by A36, A40, FUNCT_1: 12;

              

               A42: k <= sqk by A35, A37, FINSEQ_1: 1;

              

               A43: ( dom q) = ( Bags n) by FUNCT_2:def 1;

              then (sq . k) in ( dom q) by A36, PRE_POLY:def 12;

              then

               A44: k in ( dom (q * sq)) by A35, FUNCT_1: 11;

              

              then

               A45: ((q * sq) /. k) = ((q * sq) . k) by PARTFUN1:def 6

              .= (q . b) by A36, A44, FUNCT_1: 12;

              consider i be Nat such that

               A46: ( dom yq) = ( Seg i) by FINSEQ_1:def 2;

              

               A47: sqk = ( len sq) by A37, FINSEQ_1:def 3

              .= ( len spq) by A30, A27, TARSKI: 2

              .= spqk by A34, FINSEQ_1:def 3;

              

               A48: i in NAT by ORDINAL1:def 12;

              then

               A49: ( len yq) = i by A46, FINSEQ_1:def 3;

              

               A50: for i9 be Element of NAT st i9 in ( dom yq) & i9 <> k holds (ypq /. i9) = (yq /. i9)

              proof

                let i9 be Element of NAT ;

                assume that

                 A51: i9 in ( dom yq) and

                 A52: i9 <> k;

                

                 A53: 1 <= i9 by A46, A51, FINSEQ_1: 1;

                i9 in ( Seg ( len spq)) by A11, A33, A51, FINSEQ_1:def 3;

                then

                 A54: i9 in ( dom spq) by FINSEQ_1:def 3;

                then (spq /. i9) = (spq . i9) by PARTFUN1:def 6;

                then

                 A55: i9 in ( dom ((p + q) * spq)) by A39, A54, FUNCT_1: 11;

                

                then

                 A56: (((p + q) * spq) /. i9) = (((p + q) * spq) . i9) by PARTFUN1:def 6

                .= ((p + q) . (spq . i9)) by A55, FUNCT_1: 12

                .= ((p + q) . (spq /. i9)) by A54, PARTFUN1:def 6;

                

                 A57: (spq /. i9) <> b

                proof

                  assume (spq /. i9) = b;

                  then

                   A58: (spq . i9) = b by A54, PARTFUN1:def 6;

                  

                   A59: spq is one-to-one by Th10, PRE_POLY: 10;

                  (spq . k) = b by A30, A27, A36, TARSKI: 2;

                  hence thesis by A35, A37, A34, A47, A52, A54, A58, A59, FUNCT_1:def 4;

                end;

                

                 A60: i9 in ( dom sq) by A8, A46, A49, A51, FINSEQ_1:def 3;

                (sq /. i9) = (sq . i9) by A37, A34, A47, A54, PARTFUN1:def 6;

                then

                 A61: i9 in ( dom (q * sq)) by A43, A60, FUNCT_1: 11;

                

                then

                 A62: ((q * sq) /. i9) = ((q * sq) . i9) by PARTFUN1:def 6

                .= (q . (sq . i9)) by A61, FUNCT_1: 12

                .= (q . (sq /. i9)) by A60, PARTFUN1:def 6;

                

                 A63: i9 <= ( len yq) by A46, A49, A51, FINSEQ_1: 1;

                

                hence (ypq /. i9) = ((((p + q) * spq) /. i9) * ( eval ((spq /. i9),x))) by A13, A33, A53

                .= ((q . (sq /. i9)) * ( eval ((sq /. i9),x))) by A3, A32, A57, A56

                .= (yq /. i9) by A10, A53, A63, A62;

              end;

              

               A64: (sq /. k) = b by A35, A36, PARTFUN1:def 6;

              

               A65: sqk = ( len yq) by A8, A37, FINSEQ_1:def 3;

              then k <= i by A42, A46, A48, FINSEQ_1:def 3;

              then

               A66: k in ( dom yq) by A38, A46, FINSEQ_1: 1;

              ( len ypq) = sqk by A11, A34, A47, FINSEQ_1:def 3;

              

              then (ypq /. k) = ((((p + q) * spq) /. k) * ( eval ((spq /. k),x))) by A13, A38, A42

              .= (((p . b) + (q . b)) * ( eval (b,x))) by A32, A64, A41, POLYNOM1: 15

              .= (((p . b) * ( eval (b,x))) + (((q * sq) /. k) * ( eval ((sq /. k),x)))) by A64, A45, VECTSP_1:def 7

              .= (((p . b) * ( eval (b,x))) + (yq /. k)) by A10, A38, A42, A65;

              

              hence ( eval ((p + q),x)) = (((p . b) * ( eval (b,x))) + ( Sum yq)) by A12, A33, A66, A50, Th4

              .= (( eval (p,x)) + ( eval (q,x))) by A1, A9, Th11;

            end;

          end;

          hence thesis;

        end;

          case

           A67: not b in ( Support q);

          

           A68: ((p + q) . b) = ((p . b) + (q . b)) by POLYNOM1: 15

          .= ((p . b) + ( 0. L)) by A6, A67, POLYNOM1:def 4

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

          

           A69: for u be object holds u in (( Support p) \/ ( Support q)) implies u in ( Support (p + q))

          proof

            let u be object;

            assume

             A70: u in (( Support p) \/ ( Support q));

            per cases by A70, XBOOLE_0:def 3;

              suppose u in ( Support p);

              then u = b by A1, TARSKI:def 1;

              hence thesis by A6, A2, A68, POLYNOM1:def 4;

            end;

              suppose

               A71: u in ( Support q);

              then

              reconsider u as bag of n;

              

               A72: (q . u) <> ( 0. L) by A71, POLYNOM1:def 4;

              ((p + q) . u) = (q . u) by A3, A67, A71;

              hence thesis by A71, A72, POLYNOM1:def 4;

            end;

          end;

          for u be object holds u in ( Support (p + q)) implies u in (( Support p) \/ ( Support q)) by A7;

          then ( Support (p + q)) = ( {b} \/ ( Support q)) by A1, A69, TARSKI: 2;

          

          hence ( eval ((p + q),x)) = (( eval (q,x)) + (((p + q) . b) * ( eval (b,x)))) by A3, A67, Lm6

          .= (( eval (q,x)) + ( eval (p,x))) by A1, A68, Th11;

        end;

      end;

      hence thesis;

    end;

    theorem :: POLYNOM2:23

    

     Th15: for n be Ordinal, L be right_zeroed add-associative right_complementable Abelian well-unital distributive non trivial doubleLoopStr, p,q be Polynomial of n, L, x be Function of n, L holds ( eval ((p + q),x)) = (( eval (p,x)) + ( eval (q,x)))

    proof

      let n be Ordinal, L be right_zeroed add-associative right_complementable Abelian well-unital distributive non trivial doubleLoopStr, p,q be Polynomial of n, L, x be Function of n, L;

      defpred P[ Nat] means for p be Polynomial of n, L st ( card ( Support p)) = $1 holds ( eval ((p + q),x)) = (( eval (p,x)) + ( eval (q,x)));

      

       A1: ex k be Element of NAT st ( card ( Support p)) = k;

      

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

      proof

        let k be Nat;

        assume

         A3: P[k];

        let p be Polynomial of n, L;

        assume

         A4: ( card ( Support p)) = (k + 1);

        set sgp = ( SgmX (( BagOrder n),( Support p)));

        set bg = (sgp /. ( len sgp));

        

         A5: ( BagOrder n) linearly_orders ( Support p) by Th10;

        then sgp <> {} by A4, CARD_1: 27, PRE_POLY:def 2, RELAT_1: 38;

        then 1 <= ( len sgp) by NAT_1: 14;

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

        then

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

        then (sgp /. ( len sgp)) = (sgp . ( len sgp)) by PARTFUN1:def 6;

        then bg in ( rng sgp) by A6, FUNCT_1:def 3;

        then

         A7: bg in ( Support p) by A5, PRE_POLY:def 2;

        then

         A8: (p . bg) <> ( 0. L) by POLYNOM1:def 4;

        set m = (( 0_ (n,L)) +* (bg,(p . bg)));

        set p9 = (p +* (bg,( 0. L)));

        reconsider bg as bag of n;

        ( dom p) = ( Bags n) by FUNCT_2:def 1;

        then

         A9: p9 = (p +* (bg .--> ( 0. L))) by FUNCT_7:def 3;

        reconsider p9 as Function of ( Bags n), the carrier of L;

        reconsider p9 as Function of ( Bags n), L;

        for u be object holds u in ( Support p9) implies u in ( Support p)

        proof

          let u be object;

          assume

           A10: u in ( Support p9);

          then

          reconsider u as Element of ( Bags n);

          reconsider u as bag of n;

          now

            assume

             A11: u = bg;

            then u in {bg} by TARSKI:def 1;

            then u in ( dom (bg .--> ( 0. L)));

            then (p9 . u) = ((bg .--> ( 0. L)) . bg) by A9, A11, FUNCT_4: 13;

            then (p9 . u) = ( 0. L) by FUNCOP_1: 72;

            hence contradiction by A10, POLYNOM1:def 4;

          end;

          then not u in {bg} by TARSKI:def 1;

          then not u in ( dom (bg .--> ( 0. L)));

          then (p . u) = (p9 . u) by A9, FUNCT_4: 11;

          then (p . u) <> ( 0. L) by A10, POLYNOM1:def 4;

          hence thesis by POLYNOM1:def 4;

        end;

        then ( Support p9) c= ( Support p) by TARSKI:def 3;

        then

        reconsider p9 as Polynomial of n, L by POLYNOM1:def 5;

        

         A12: ( dom p) = ( Bags n) by FUNCT_2:def 1;

        

         A13: for u be object holds u in ( Support p) implies u in (( Support p9) \/ {bg})

        proof

          let u be object;

          assume

           A14: u in ( Support p);

          then

          reconsider u as Element of ( Bags n);

          

           A15: (p . u) <> ( 0. L) by A14, POLYNOM1:def 4;

          per cases ;

            suppose u = bg;

            then u in {bg} by TARSKI:def 1;

            hence thesis by XBOOLE_0:def 3;

          end;

            suppose u <> bg;

            then not u in {bg} by TARSKI:def 1;

            then not u in ( dom (bg .--> ( 0. L)));

            then (p9 . u) = (p . u) by A9, FUNCT_4: 11;

            then u in ( Support p9) by A15, POLYNOM1:def 4;

            hence thesis by XBOOLE_0:def 3;

          end;

        end;

        bg in {bg} by TARSKI:def 1;

        then bg in ( dom (bg .--> ( 0. L)));

        then (p9 . bg) = ((bg .--> ( 0. L)) . bg) by A9, FUNCT_4: 13;

        then

         A16: (p9 . bg) = ( 0. L) by FUNCOP_1: 72;

        then

         A17: not bg in ( Support p9) by POLYNOM1:def 4;

        for u be object holds u in (( Support p9) \/ {bg}) implies u in ( Support p)

        proof

          let u be object;

          assume

           A18: u in (( Support p9) \/ {bg});

          per cases by A18, XBOOLE_0:def 3;

            suppose

             A19: u in ( Support p9);

            then

            reconsider u as Element of ( Bags n);

            u <> bg by A16, A19, POLYNOM1:def 4;

            then not u in {bg} by TARSKI:def 1;

            then not u in ( dom (bg .--> ( 0. L)));

            then

             A20: (p9 . u) = (p . u) by A9, FUNCT_4: 11;

            (p9 . u) <> ( 0. L) by A19, POLYNOM1:def 4;

            hence thesis by A20, POLYNOM1:def 4;

          end;

            suppose u in {bg};

            hence thesis by A7, TARSKI:def 1;

          end;

        end;

        then ( Support p) = (( Support p9) \/ {bg}) by A13, TARSKI: 2;

        then

         A21: (k + 1) = (( card ( Support p9)) + 1) by A4, A17, CARD_2: 41;

        ( dom ( 0_ (n,L))) = ( Bags n) by FUNCT_2:def 1;

        then

         A22: m = (( 0_ (n,L)) +* (bg .--> (p . bg))) by FUNCT_7:def 3;

        reconsider m as Function of ( Bags n), the carrier of L;

        reconsider m as Function of ( Bags n), L;

        

         A23: for u be object holds u in ( Support m) implies u in {bg}

        proof

          let u be object;

          assume

           A24: u in ( Support m);

          then

          reconsider u as Element of ( Bags n);

          

           A25: (m . u) <> ( 0. L) by A24, POLYNOM1:def 4;

          now

            assume u <> bg;

            then not u in {bg} by TARSKI:def 1;

            then not u in ( dom (bg .--> (p . bg)));

            then (m . u) = (( 0_ (n,L)) . u) by A22, FUNCT_4: 11;

            hence contradiction by A25, POLYNOM1: 22;

          end;

          hence thesis by TARSKI:def 1;

        end;

        for u be object holds u in {bg} implies u in ( Support m)

        proof

          let u be object;

          bg in {bg} by TARSKI:def 1;

          then bg in ( dom (bg .--> (p . bg)));

          then (m . bg) = ((bg .--> (p . bg)) . bg) by A22, FUNCT_4: 13;

          then

           A26: (m . bg) = (p . bg) by FUNCOP_1: 72;

          assume u in {bg};

          then u = bg by TARSKI:def 1;

          hence thesis by A8, A26, POLYNOM1:def 4;

        end;

        then

         A27: ( Support m) = {bg} by A23, TARSKI: 2;

        then

        reconsider m as Polynomial of n, L by POLYNOM1:def 5;

        reconsider m as Polynomial of n, L;

        

         A28: for u be object st u in ( Bags n) holds ((p9 + m) . u) = (p . u)

        proof

          let u be object;

          assume u in ( Bags n);

          then

          reconsider u as bag of n;

          per cases ;

            suppose

             A29: u = bg;

            bg in {bg} by TARSKI:def 1;

            then bg in ( dom (bg .--> (p . bg)));

            then (m . bg) = ((bg .--> (p . bg)) . bg) by A22, FUNCT_4: 13;

            then

             A30: (m . bg) = (p . bg) by FUNCOP_1: 72;

            u in {bg} by A29, TARSKI:def 1;

            then u in ( dom (bg .--> ( 0. L)));

            then

             A31: (p9 . u) = ((bg .--> ( 0. L)) . bg) by A9, A29, FUNCT_4: 13;

            ((p9 + m) . u) = ((p9 . u) + (m . u)) by POLYNOM1: 15

            .= (( 0. L) + (p . bg)) by A29, A31, A30, FUNCOP_1: 72

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

            hence thesis by A29;

          end;

            suppose u <> bg;

            then

             A32: not u in {bg} by TARSKI:def 1;

            then

             A33: not u in ( dom (bg .--> ( 0. L)));

             not u in ( dom (bg .--> (p . bg))) by A32;

            then (m . u) = (( 0_ (n,L)) . u) by A22, FUNCT_4: 11;

            then

             A34: (m . u) = ( 0. L) by POLYNOM1: 22;

            ((p9 + m) . u) = ((p9 . u) + (m . u)) by POLYNOM1: 15

            .= ((p . u) + ( 0. L)) by A9, A33, A34, FUNCT_4: 11

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

            hence thesis;

          end;

        end;

        

         A35: ( dom (p9 + m)) = ( Bags n) by FUNCT_2:def 1;

        

        then ( eval (p,x)) = ( eval ((m + p9),x)) by A12, A28, FUNCT_1: 2

        .= (( eval (p9,x)) + ( eval (m,x))) by A27, Lm7;

        

        hence (( eval (p,x)) + ( eval (q,x))) = ((( eval (p9,x)) + ( eval (q,x))) + ( eval (m,x))) by RLVECT_1:def 3

        .= (( eval ((p9 + q),x)) + ( eval (m,x))) by A3, A21

        .= ( eval ((m + (p9 + q)),x)) by A27, Lm7

        .= ( eval (((p9 + m) + q),x)) by POLYNOM1: 21

        .= ( eval ((p + q),x)) by A35, A12, A28, FUNCT_1: 2;

      end;

      

       A36: P[ 0 ]

      proof

        let p be Polynomial of n, L;

        assume ( card ( Support p)) = 0 ;

        then ( Support p) = {} ;

        then

         A37: p = ( 0_ (n,L)) by Th9;

        

        hence ( eval ((p + q),x)) = ( eval (q,x)) by POLYNOM1: 23

        .= (( 0. L) + ( eval (q,x))) by RLVECT_1: 4

        .= (( eval (p,x)) + ( eval (q,x))) by A37, Th12;

      end;

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

      hence thesis by A1;

    end;

    theorem :: POLYNOM2:24

    for n be Ordinal, L be right_zeroed add-associative right_complementable Abelian well-unital distributive non trivial doubleLoopStr, p,q be Polynomial of n, L, x be Function of n, L holds ( eval ((p - q),x)) = (( eval (p,x)) - ( eval (q,x)))

    proof

      let n be Ordinal, L be right_zeroed add-associative right_complementable Abelian well-unital distributive non trivial doubleLoopStr, p,q be Polynomial of n, L, x be Function of n, L;

      

      thus ( eval ((p - q),x)) = ( eval ((p + ( - q)),x)) by POLYNOM1:def 7

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

      .= (( eval (p,x)) - ( eval (q,x))) by Th14;

    end;

    

     Lm8: for n be Ordinal, L be right_zeroed add-associative right_complementable Abelian well-unital distributive non trivial commutative associative non empty doubleLoopStr, p,q be Polynomial of n, L, b1,b2 be bag of n st ( Support p) = {b1} & ( Support q) = {b2} holds for x be Function of n, L holds ( eval ((p *' q),x)) = (( eval (p,x)) * ( eval (q,x)))

    proof

      let n be Ordinal, L be right_zeroed add-associative right_complementable Abelian well-unital distributive commutative associative non trivial doubleLoopStr, p,q be Polynomial of n, L, b1,b2 be bag of n;

      assume that

       A1: ( Support p) = {b1} and

       A2: ( Support q) = {b2};

      consider s be FinSequence of the carrier of L such that

       A3: ((p *' q) . (b1 + b2)) = ( Sum s) and

       A4: ( len s) = ( len ( decomp (b1 + b2))) and

       A5: for k be Element of NAT st k in ( dom s) holds ex u1,u2 be bag of n st (( decomp (b1 + b2)) /. k) = <*u1, u2*> & (s /. k) = ((p . u1) * (q . u2)) by POLYNOM1:def 10;

      

       A6: (b1 + b2) is Element of ( Bags n) by PRE_POLY:def 12;

      let x be Function of n, L;

      

       A7: (((p . b1) * (q . b2)) * (( eval (b1,x)) * ( eval (b2,x)))) = ((((p . b1) * (q . b2)) * ( eval (b1,x))) * ( eval (b2,x))) by GROUP_1:def 3

      .= ((((p . b1) * ( eval (b1,x))) * (q . b2)) * ( eval (b2,x))) by GROUP_1:def 3

      .= (((p . b1) * ( eval (b1,x))) * ((q . b2) * ( eval (b2,x)))) by GROUP_1:def 3

      .= (( eval (p,x)) * ((q . b2) * ( eval (b2,x)))) by A1, Th11

      .= (( eval (p,x)) * ( eval (q,x))) by A2, Th11;

      

       A8: for b be bag of n st b <> b2 holds (q . b) = ( 0. L)

      proof

        let b be bag of n;

        assume b <> b2;

        then

         A9: not b in ( Support q) by A2, TARSKI:def 1;

        b is Element of ( Bags n) by PRE_POLY:def 12;

        hence thesis by A9, POLYNOM1:def 4;

      end;

      

       A10: for b be bag of n st b <> b1 holds (p . b) = ( 0. L)

      proof

        let b be bag of n;

        assume b <> b1;

        then

         A11: not b in ( Support p) by A1, TARSKI:def 1;

        b is Element of ( Bags n) by PRE_POLY:def 12;

        hence thesis by A11, POLYNOM1:def 4;

      end;

      

       A12: for u be object holds u in ( Support (p *' q)) implies u in {(b1 + b2)}

      proof

        let u be object;

        assume

         A13: u in ( Support (p *' q));

        assume

         A14: not u in {(b1 + b2)};

        reconsider u as bag of n by A13;

        consider t be FinSequence of the carrier of L such that

         A15: ((p *' q) . u) = ( Sum t) and

         A16: ( len t) = ( len ( decomp u)) and

         A17: for k be Element of NAT st k in ( dom t) holds ex b19,b29 be bag of n st (( decomp u) /. k) = <*b19, b29*> & (t /. k) = ((p . b19) * (q . b29)) by POLYNOM1:def 10;

        1 <= ( len t) by A16, NAT_1: 14;

        then

         A18: 1 in ( dom t) by FINSEQ_3: 25;

        

         A19: ( dom t) = ( Seg ( len t)) by FINSEQ_1:def 3

        .= ( dom ( decomp u)) by A16, FINSEQ_1:def 3;

        

         A20: for i be Element of NAT st i in ( dom t) holds (t /. i) = ( 0. L)

        proof

          let i be Element of NAT ;

          consider S be non empty finite Subset of ( Bags n) such that

           A21: ( divisors u) = ( SgmX (( BagOrder n),S)) and

           A22: for b be bag of n holds b in S iff b divides u by PRE_POLY:def 16;

          ( BagOrder n) linearly_orders S by Lm3;

          then

           A23: S = ( rng ( divisors u)) by A21, PRE_POLY:def 2;

          assume

           A24: i in ( dom t);

          then

          consider b19,b29 be bag of n such that

           A25: (( decomp u) /. i) = <*b19, b29*> and

           A26: (t /. i) = ((p . b19) * (q . b29)) by A17;

          

           A27: b19 = (( divisors u) /. i) by A19, A24, A25, PRE_POLY: 70;

          

           A28: i in ( dom ( divisors u)) by A19, A24, PRE_POLY:def 17;

          then b19 = (( divisors u) . i) by A27, PARTFUN1:def 6;

          then b19 in ( rng ( divisors u)) by A28, FUNCT_1:def 3;

          then

           A29: b19 divides u by A22, A23;

          per cases ;

            suppose

             A30: b19 = b1 & b29 = b2;

            b2 = ( <*b1, b2*> . 2) by FINSEQ_1: 44

            .= ( <*b1, (u -' b1)*> . 2) by A19, A24, A25, A27, A30, PRE_POLY:def 17

            .= (u -' b1) by FINSEQ_1: 44;

            then (b1 + b2) = u by A29, A30, PRE_POLY: 47;

            hence thesis by A14, TARSKI:def 1;

          end;

            suppose b19 <> b1;

            then (p . b19) = ( 0. L) by A10;

            hence thesis by A26;

          end;

            suppose b29 <> b2;

            then (q . b29) = ( 0. L) by A8;

            hence thesis by A26;

          end;

        end;

        then for i be Element of NAT st i in ( dom t) & i <> 1 holds (t /. i) = ( 0. L);

        

        then ( Sum t) = (t /. 1) by A18, Th2

        .= ( 0. L) by A18, A20;

        hence thesis by A13, A15, POLYNOM1:def 4;

      end;

      consider k be Element of NAT such that

       A31: k in ( dom ( decomp (b1 + b2))) and

       A32: (( decomp (b1 + b2)) /. k) = <*b1, b2*> by PRE_POLY: 69;

      

       A33: ( dom s) = ( Seg ( len s)) by FINSEQ_1:def 3

      .= ( dom ( decomp (b1 + b2))) by A4, FINSEQ_1:def 3;

      then

      consider b19,b29 be bag of n such that

       A34: (( decomp (b1 + b2)) /. k) = <*b19, b29*> and

       A35: (s /. k) = ((p . b19) * (q . b29)) by A5, A31;

      

       A36: b2 = ( <*b1, b2*> . 2) by FINSEQ_1: 44

      .= b29 by A32, A34, FINSEQ_1: 44;

      

       A37: for k9 be Element of NAT st k9 in ( dom s) & k9 <> k holds (s /. k9) = ( 0. L)

      proof

        let k9 be Element of NAT ;

        assume that

         A38: k9 in ( dom s) and

         A39: k9 <> k;

        consider b19,b29 be bag of n such that

         A40: (( decomp (b1 + b2)) /. k9) = <*b19, b29*> and

         A41: (s /. k9) = ((p . b19) * (q . b29)) by A5, A38;

        per cases ;

          suppose

           A42: b19 = b1 & b29 = b2;

          (( decomp (b1 + b2)) . k9) = (( decomp (b1 + b2)) /. k9) by A33, A38, PARTFUN1:def 6

          .= (( decomp (b1 + b2)) . k) by A31, A32, A40, A42, PARTFUN1:def 6;

          hence thesis by A33, A31, A38, A39, FUNCT_1:def 4;

        end;

          suppose b19 <> b1;

          then (p . b19) = ( 0. L) by A10;

          hence thesis by A41;

        end;

          suppose b29 <> b2;

          then (q . b29) = ( 0. L) by A8;

          hence thesis by A41;

        end;

      end;

      b1 = ( <*b19, b29*> . 1) by A32, A34, FINSEQ_1: 44

      .= b19 by FINSEQ_1: 44;

      then

       A43: ((p *' q) . (b1 + b2)) = ((p . b1) * (q . b2)) by A3, A33, A31, A35, A36, A37, Th2;

      per cases ;

        suppose

         A44: ((p . b1) * (q . b2)) = ( 0. L);

        then

         A45: not (b1 + b2) in ( Support (p *' q)) by A43, POLYNOM1:def 4;

        ( Support (p *' q)) = {}

        proof

          set u = the Element of ( Support (p *' q));

          assume

           A46: ( Support (p *' q)) <> {} ;

          then

           A47: u in ( Support (p *' q));

          u in {(b1 + b2)} by A12, A46;

          hence thesis by A45, A47, TARSKI:def 1;

        end;

        then (p *' q) = ( 0_ (n,L)) by Th9;

        hence ( eval ((p *' q),x)) = (( eval (p,x)) * ( eval (q,x))) by A7, A44, Th12;

      end;

        suppose ((p . b1) * (q . b2)) <> ( 0. L);

        then (b1 + b2) in ( Support (p *' q)) by A43, A6, POLYNOM1:def 4;

        then for u be object holds u in {(b1 + b2)} implies u in ( Support (p *' q)) by TARSKI:def 1;

        then ( Support (p *' q)) = {(b1 + b2)} by A12, TARSKI: 2;

        

        hence ( eval ((p *' q),x)) = (((p *' q) . (b1 + b2)) * ( eval ((b1 + b2),x))) by Th11

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

      end;

    end;

    

     Lm9: for n be Ordinal, L be right_zeroed add-associative right_complementable Abelian well-unital distributive non trivial commutative associative non empty doubleLoopStr, q be Polynomial of n, L st ex b be bag of n st ( Support q) = {b} holds for p be Polynomial of n, L, x be Function of n, L holds ( eval ((p *' q),x)) = (( eval (p,x)) * ( eval (q,x)))

    proof

      let n be Ordinal, L be right_zeroed add-associative right_complementable Abelian well-unital distributive commutative associative non trivial doubleLoopStr, q be Polynomial of n, L;

      given b be bag of n such that

       A1: ( Support q) = {b};

      let p be Polynomial of n, L;

      let x be Function of n, L;

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

      

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

      proof

        let k be Nat;

        assume

         A3: P[k];

        let p be Polynomial of n, L;

        assume

         A4: ( card ( Support p)) = (k + 1);

        set sgp = ( SgmX (( BagOrder n),( Support p)));

        set bg = (sgp /. ( len sgp));

        

         A5: ( BagOrder n) linearly_orders ( Support p) by Th10;

        then sgp <> {} by A4, CARD_1: 27, PRE_POLY:def 2, RELAT_1: 38;

        then 1 <= ( len sgp) by NAT_1: 14;

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

        then

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

        then (sgp /. ( len sgp)) = (sgp . ( len sgp)) by PARTFUN1:def 6;

        then bg in ( rng sgp) by A6, FUNCT_1:def 3;

        then

         A7: bg in ( Support p) by A5, PRE_POLY:def 2;

        then

         A8: (p . bg) <> ( 0. L) by POLYNOM1:def 4;

        set m = (( 0_ (n,L)) +* (bg,(p . bg)));

        set p9 = (p +* (bg,( 0. L)));

        reconsider bg as bag of n;

        ( dom p) = ( Bags n) by FUNCT_2:def 1;

        then

         A9: p9 = (p +* (bg .--> ( 0. L))) by FUNCT_7:def 3;

        reconsider p9 as Function of ( Bags n), the carrier of L;

        reconsider p9 as Function of ( Bags n), L;

        for u be object holds u in ( Support p9) implies u in ( Support p)

        proof

          let u be object;

          assume

           A10: u in ( Support p9);

          then

          reconsider u as Element of ( Bags n);

          reconsider u as bag of n;

          now

            assume

             A11: u = bg;

            then u in {bg} by TARSKI:def 1;

            then u in ( dom (bg .--> ( 0. L)));

            then (p9 . u) = ((bg .--> ( 0. L)) . bg) by A9, A11, FUNCT_4: 13;

            then (p9 . u) = ( 0. L) by FUNCOP_1: 72;

            hence contradiction by A10, POLYNOM1:def 4;

          end;

          then not u in {bg} by TARSKI:def 1;

          then not u in ( dom (bg .--> ( 0. L)));

          then (p . u) = (p9 . u) by A9, FUNCT_4: 11;

          then (p . u) <> ( 0. L) by A10, POLYNOM1:def 4;

          hence thesis by POLYNOM1:def 4;

        end;

        then ( Support p9) c= ( Support p) by TARSKI:def 3;

        then

        reconsider p9 as Polynomial of n, L by POLYNOM1:def 5;

        

         A12: ( dom p) = ( Bags n) by FUNCT_2:def 1;

        

         A13: for u be object holds u in ( Support p) implies u in (( Support p9) \/ {bg})

        proof

          let u be object;

          assume

           A14: u in ( Support p);

          then

          reconsider u as Element of ( Bags n);

          

           A15: (p . u) <> ( 0. L) by A14, POLYNOM1:def 4;

          per cases ;

            suppose u = bg;

            then u in {bg} by TARSKI:def 1;

            hence thesis by XBOOLE_0:def 3;

          end;

            suppose u <> bg;

            then not u in {bg} by TARSKI:def 1;

            then not u in ( dom (bg .--> ( 0. L)));

            then (p9 . u) = (p . u) by A9, FUNCT_4: 11;

            then u in ( Support p9) by A15, POLYNOM1:def 4;

            hence thesis by XBOOLE_0:def 3;

          end;

        end;

        bg in {bg} by TARSKI:def 1;

        then bg in ( dom (bg .--> ( 0. L)));

        then (p9 . bg) = ((bg .--> ( 0. L)) . bg) by A9, FUNCT_4: 13;

        then

         A16: (p9 . bg) = ( 0. L) by FUNCOP_1: 72;

        then

         A17: not bg in ( Support p9) by POLYNOM1:def 4;

        for u be object holds u in (( Support p9) \/ {bg}) implies u in ( Support p)

        proof

          let u be object;

          assume

           A18: u in (( Support p9) \/ {bg});

          per cases by A18, XBOOLE_0:def 3;

            suppose

             A19: u in ( Support p9);

            then

            reconsider u as Element of ( Bags n);

            u <> bg by A16, A19, POLYNOM1:def 4;

            then not u in {bg} by TARSKI:def 1;

            then not u in ( dom (bg .--> ( 0. L)));

            then

             A20: (p9 . u) = (p . u) by A9, FUNCT_4: 11;

            (p9 . u) <> ( 0. L) by A19, POLYNOM1:def 4;

            hence thesis by A20, POLYNOM1:def 4;

          end;

            suppose u in {bg};

            hence thesis by A7, TARSKI:def 1;

          end;

        end;

        then ( Support p) = (( Support p9) \/ {bg}) by A13, TARSKI: 2;

        then

         A21: (k + 1) = (( card ( Support p9)) + 1) by A4, A17, CARD_2: 41;

        ( dom ( 0_ (n,L))) = ( Bags n) by FUNCT_2:def 1;

        then

         A22: m = (( 0_ (n,L)) +* (bg .--> (p . bg))) by FUNCT_7:def 3;

        reconsider m as Function of ( Bags n), the carrier of L;

        reconsider m as Function of ( Bags n), L;

        

         A23: for u be object holds u in ( Support m) implies u in {bg}

        proof

          let u be object;

          assume

           A24: u in ( Support m);

          then

          reconsider u as Element of ( Bags n);

          

           A25: (m . u) <> ( 0. L) by A24, POLYNOM1:def 4;

          now

            assume u <> bg;

            then not u in {bg} by TARSKI:def 1;

            then not u in ( dom (bg .--> (p . bg)));

            then (m . u) = (( 0_ (n,L)) . u) by A22, FUNCT_4: 11;

            hence contradiction by A25, POLYNOM1: 22;

          end;

          hence thesis by TARSKI:def 1;

        end;

        for u be object holds u in {bg} implies u in ( Support m)

        proof

          let u be object;

          bg in {bg} by TARSKI:def 1;

          then bg in ( dom (bg .--> (p . bg)));

          then (m . bg) = ((bg .--> (p . bg)) . bg) by A22, FUNCT_4: 13;

          then

           A26: (m . bg) = (p . bg) by FUNCOP_1: 72;

          assume u in {bg};

          then u = bg by TARSKI:def 1;

          hence thesis by A8, A26, POLYNOM1:def 4;

        end;

        then

         A27: ( Support m) = {bg} by A23, TARSKI: 2;

        then

        reconsider m as Polynomial of n, L by POLYNOM1:def 5;

        reconsider m as Polynomial of n, L;

        

         A28: for u be object st u in ( Bags n) holds ((p9 + m) . u) = (p . u)

        proof

          let u be object;

          assume u in ( Bags n);

          then

          reconsider u as bag of n;

          per cases ;

            suppose

             A29: u = bg;

            bg in {bg} by TARSKI:def 1;

            then bg in ( dom (bg .--> (p . bg)));

            then (m . bg) = ((bg .--> (p . bg)) . bg) by A22, FUNCT_4: 13;

            then

             A30: (m . bg) = (p . bg) by FUNCOP_1: 72;

            u in {bg} by A29, TARSKI:def 1;

            then u in ( dom (bg .--> ( 0. L)));

            then

             A31: (p9 . u) = ((bg .--> ( 0. L)) . bg) by A9, A29, FUNCT_4: 13;

            ((p9 + m) . u) = ((p9 . u) + (m . u)) by POLYNOM1: 15

            .= (( 0. L) + (p . bg)) by A29, A31, A30, FUNCOP_1: 72

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

            hence thesis by A29;

          end;

            suppose u <> bg;

            then

             A32: not u in {bg} by TARSKI:def 1;

            then

             A33: not u in ( dom (bg .--> ( 0. L)));

             not u in ( dom (bg .--> (p . bg))) by A32;

            then (m . u) = (( 0_ (n,L)) . u) by A22, FUNCT_4: 11;

            then

             A34: (m . u) = ( 0. L) by POLYNOM1: 22;

            ((p9 + m) . u) = ((p9 . u) + (m . u)) by POLYNOM1: 15

            .= ((p . u) + ( 0. L)) by A9, A33, A34, FUNCT_4: 11

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

            hence thesis;

          end;

        end;

        

         A35: ( dom (p9 + m)) = ( Bags n) by FUNCT_2:def 1;

        

        then ( eval (p,x)) = ( eval ((m + p9),x)) by A12, A28, FUNCT_1: 2

        .= (( eval (p9,x)) + ( eval (m,x))) by A27, Lm7;

        

        hence (( eval (p,x)) * ( eval (q,x))) = ((( eval (p9,x)) * ( eval (q,x))) + (( eval (m,x)) * ( eval (q,x)))) by VECTSP_1:def 7

        .= (( eval ((p9 *' q),x)) + (( eval (m,x)) * ( eval (q,x)))) by A3, A21

        .= (( eval ((p9 *' q),x)) + ( eval ((m *' q),x))) by A1, A27, Lm8

        .= ( eval (((p9 *' q) + (m *' q)),x)) by Th15

        .= ( eval ((q *' (p9 + m)),x)) by POLYNOM1: 26

        .= ( eval ((p *' q),x)) by A35, A12, A28, FUNCT_1: 2;

      end;

      

       A36: ex k be Element of NAT st ( card ( Support p)) = k;

      

       A37: P[ 0 ]

      proof

        let p be Polynomial of n, L;

        assume ( card ( Support p)) = 0 ;

        then ( Support p) = {} ;

        then

         A38: p = ( 0_ (n,L)) by Th9;

        

        hence ( eval ((p *' q),x)) = ( eval (p,x)) by POLYNOM1: 28

        .= (( 0. L) * ( eval (q,x))) by A38, Th12

        .= (( eval (p,x)) * ( eval (q,x))) by A38, Th12;

      end;

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

      hence thesis by A36;

    end;

    theorem :: POLYNOM2:25

    

     Th17: for n be Ordinal, L be right_zeroed add-associative right_complementable Abelian well-unital distributive non trivial commutative associative non empty doubleLoopStr, p,q be Polynomial of n, L, x be Function of n, L holds ( eval ((p *' q),x)) = (( eval (p,x)) * ( eval (q,x)))

    proof

      let n be Ordinal, L be right_zeroed add-associative right_complementable Abelian well-unital distributive commutative associative non trivial doubleLoopStr, p,q be Polynomial of n, L, x be Function of n, L;

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

      

       A1: ex k be Element of NAT st ( card ( Support p)) = k;

      

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

      proof

        let k be Nat;

        assume

         A3: P[k];

        let p be Polynomial of n, L;

        assume

         A4: ( card ( Support p)) = (k + 1);

        set sgp = ( SgmX (( BagOrder n),( Support p)));

        set bg = (sgp /. ( len sgp));

        

         A5: ( BagOrder n) linearly_orders ( Support p) by Th10;

        then sgp <> {} by A4, CARD_1: 27, PRE_POLY:def 2, RELAT_1: 38;

        then 1 <= ( len sgp) by NAT_1: 14;

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

        then

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

        then (sgp /. ( len sgp)) = (sgp . ( len sgp)) by PARTFUN1:def 6;

        then bg in ( rng sgp) by A6, FUNCT_1:def 3;

        then

         A7: bg in ( Support p) by A5, PRE_POLY:def 2;

        then

         A8: (p . bg) <> ( 0. L) by POLYNOM1:def 4;

        set m = (( 0_ (n,L)) +* (bg,(p . bg)));

        set p9 = (p +* (bg,( 0. L)));

        reconsider bg as bag of n;

        ( dom p) = ( Bags n) by FUNCT_2:def 1;

        then

         A9: p9 = (p +* (bg .--> ( 0. L))) by FUNCT_7:def 3;

        reconsider p9 as Function of ( Bags n), L;

        for u be object holds u in ( Support p9) implies u in ( Support p)

        proof

          let u be object;

          assume

           A10: u in ( Support p9);

          then

          reconsider u as Element of ( Bags n);

          reconsider u as bag of n;

          now

            assume

             A11: u = bg;

            then u in {bg} by TARSKI:def 1;

            then u in ( dom (bg .--> ( 0. L)));

            then (p9 . u) = ((bg .--> ( 0. L)) . bg) by A9, A11, FUNCT_4: 13;

            then (p9 . u) = ( 0. L) by FUNCOP_1: 72;

            hence contradiction by A10, POLYNOM1:def 4;

          end;

          then not u in {bg} by TARSKI:def 1;

          then not u in ( dom (bg .--> ( 0. L)));

          then (p . u) = (p9 . u) by A9, FUNCT_4: 11;

          then (p . u) <> ( 0. L) by A10, POLYNOM1:def 4;

          hence thesis by POLYNOM1:def 4;

        end;

        then ( Support p9) c= ( Support p) by TARSKI:def 3;

        then

        reconsider p9 as Polynomial of n, L by POLYNOM1:def 5;

        

         A12: ( dom p) = ( Bags n) by FUNCT_2:def 1;

        

         A13: for u be object holds u in ( Support p) implies u in (( Support p9) \/ {bg})

        proof

          let u be object;

          assume

           A14: u in ( Support p);

          then

          reconsider u as Element of ( Bags n);

          

           A15: (p . u) <> ( 0. L) by A14, POLYNOM1:def 4;

          per cases ;

            suppose u = bg;

            then u in {bg} by TARSKI:def 1;

            hence thesis by XBOOLE_0:def 3;

          end;

            suppose u <> bg;

            then not u in {bg} by TARSKI:def 1;

            then not u in ( dom (bg .--> ( 0. L)));

            then (p9 . u) = (p . u) by A9, FUNCT_4: 11;

            then u in ( Support p9) by A15, POLYNOM1:def 4;

            hence thesis by XBOOLE_0:def 3;

          end;

        end;

        bg in {bg} by TARSKI:def 1;

        then bg in ( dom (bg .--> ( 0. L)));

        then (p9 . bg) = ((bg .--> ( 0. L)) . bg) by A9, FUNCT_4: 13;

        then

         A16: (p9 . bg) = ( 0. L) by FUNCOP_1: 72;

        then

         A17: not bg in ( Support p9) by POLYNOM1:def 4;

        for u be object holds u in (( Support p9) \/ {bg}) implies u in ( Support p)

        proof

          let u be object;

          assume

           A18: u in (( Support p9) \/ {bg});

          per cases by A18, XBOOLE_0:def 3;

            suppose

             A19: u in ( Support p9);

            then

            reconsider u as Element of ( Bags n);

            u <> bg by A16, A19, POLYNOM1:def 4;

            then not u in {bg} by TARSKI:def 1;

            then not u in ( dom (bg .--> ( 0. L)));

            then

             A20: (p9 . u) = (p . u) by A9, FUNCT_4: 11;

            (p9 . u) <> ( 0. L) by A19, POLYNOM1:def 4;

            hence thesis by A20, POLYNOM1:def 4;

          end;

            suppose u in {bg};

            hence thesis by A7, TARSKI:def 1;

          end;

        end;

        then ( Support p) = (( Support p9) \/ {bg}) by A13, TARSKI: 2;

        then

         A21: (k + 1) = (( card ( Support p9)) + 1) by A4, A17, CARD_2: 41;

        ( dom ( 0_ (n,L))) = ( Bags n) by FUNCT_2:def 1;

        then

         A22: m = (( 0_ (n,L)) +* (bg .--> (p . bg))) by FUNCT_7:def 3;

        reconsider m as Function of ( Bags n), the carrier of L;

        reconsider m as Function of ( Bags n), L;

        

         A23: for u be object holds u in ( Support m) implies u in {bg}

        proof

          let u be object;

          assume

           A24: u in ( Support m);

          then

          reconsider u as Element of ( Bags n);

          

           A25: (m . u) <> ( 0. L) by A24, POLYNOM1:def 4;

          now

            assume u <> bg;

            then not u in {bg} by TARSKI:def 1;

            then not u in ( dom (bg .--> (p . bg)));

            then (m . u) = (( 0_ (n,L)) . u) by A22, FUNCT_4: 11;

            hence contradiction by A25, POLYNOM1: 22;

          end;

          hence thesis by TARSKI:def 1;

        end;

        for u be object holds u in {bg} implies u in ( Support m)

        proof

          let u be object;

          bg in {bg} by TARSKI:def 1;

          then bg in ( dom (bg .--> (p . bg)));

          then (m . bg) = ((bg .--> (p . bg)) . bg) by A22, FUNCT_4: 13;

          then

           A26: (m . bg) = (p . bg) by FUNCOP_1: 72;

          assume u in {bg};

          then u = bg by TARSKI:def 1;

          hence thesis by A8, A26, POLYNOM1:def 4;

        end;

        then

         A27: ( Support m) = {bg} by A23, TARSKI: 2;

        then

        reconsider m as Polynomial of n, L by POLYNOM1:def 5;

        reconsider m as Polynomial of n, L;

        

         A28: for u be object st u in ( Bags n) holds ((p9 + m) . u) = (p . u)

        proof

          let u be object;

          assume u in ( Bags n);

          then

          reconsider u as bag of n;

          per cases ;

            suppose

             A29: u = bg;

            bg in {bg} by TARSKI:def 1;

            then bg in ( dom (bg .--> (p . bg)));

            then (m . bg) = ((bg .--> (p . bg)) . bg) by A22, FUNCT_4: 13;

            then

             A30: (m . bg) = (p . bg) by FUNCOP_1: 72;

            u in {bg} by A29, TARSKI:def 1;

            then u in ( dom (bg .--> ( 0. L)));

            then

             A31: (p9 . u) = ((bg .--> ( 0. L)) . bg) by A9, A29, FUNCT_4: 13;

            ((p9 + m) . u) = ((p9 . u) + (m . u)) by POLYNOM1: 15

            .= (( 0. L) + (p . bg)) by A29, A31, A30, FUNCOP_1: 72

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

            hence thesis by A29;

          end;

            suppose u <> bg;

            then

             A32: not u in {bg} by TARSKI:def 1;

            then

             A33: not u in ( dom (bg .--> ( 0. L)));

             not u in ( dom (bg .--> (p . bg))) by A32;

            then (m . u) = (( 0_ (n,L)) . u) by A22, FUNCT_4: 11;

            then

             A34: (m . u) = ( 0. L) by POLYNOM1: 22;

            ((p9 + m) . u) = ((p9 . u) + (m . u)) by POLYNOM1: 15

            .= ((p . u) + ( 0. L)) by A9, A33, A34, FUNCT_4: 11

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

            hence thesis;

          end;

        end;

        

         A35: ( dom (p9 + m)) = ( Bags n) by FUNCT_2:def 1;

        

        then ( eval (p,x)) = ( eval ((m + p9),x)) by A12, A28, FUNCT_1: 2

        .= (( eval (p9,x)) + ( eval (m,x))) by A27, Lm7;

        

        hence (( eval (p,x)) * ( eval (q,x))) = ((( eval (p9,x)) * ( eval (q,x))) + (( eval (m,x)) * ( eval (q,x)))) by VECTSP_1:def 7

        .= (( eval ((p9 *' q),x)) + (( eval (m,x)) * ( eval (q,x)))) by A3, A21

        .= (( eval ((p9 *' q),x)) + ( eval ((m *' q),x))) by A27, Lm9

        .= ( eval (((p9 *' q) + (m *' q)),x)) by Th15

        .= ( eval ((q *' (p9 + m)),x)) by POLYNOM1: 26

        .= ( eval ((p *' q),x)) by A35, A12, A28, FUNCT_1: 2;

      end;

      

       A36: P[ 0 ]

      proof

        let p be Polynomial of n, L;

        assume ( card ( Support p)) = 0 ;

        then ( Support p) = {} ;

        then

         A37: p = ( 0_ (n,L)) by Th9;

        

        hence ( eval ((p *' q),x)) = ( eval (p,x)) by POLYNOM1: 28

        .= (( 0. L) * ( eval (q,x))) by A37, Th12

        .= (( eval (p,x)) * ( eval (q,x))) by A37, Th12;

      end;

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

      hence thesis by A1;

    end;

    begin

    definition

      let n be Ordinal, L be right_zeroed add-associative right_complementable well-unital distributive non trivial doubleLoopStr, x be Function of n, L;

      :: POLYNOM2:def5

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

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

      existence

      proof

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

         A1:

        now

          let p be object;

          assume p in the carrier of ( Polynom-Ring (n,L));

          then

          reconsider p9 = p as Polynomial of n, L by POLYNOM1:def 11;

          thus ex y be object st y in the carrier of L & P[p, y]

          proof

            take ( eval (p9,x));

            thus thesis;

          end;

        end;

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

         A2: for x be object st x in the carrier of ( Polynom-Ring (n,L)) holds P[x, (f . x)] from FUNCT_2:sch 1( A1);

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

        take f;

        let p be Polynomial of n, L;

        p in the carrier of ( Polynom-Ring (n,L)) by POLYNOM1:def 11;

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

        hence thesis;

      end;

      uniqueness

      proof

        let f,g be Function of ( Polynom-Ring (n,L)), L such that

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

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

        reconsider f, g as Function of the carrier of ( Polynom-Ring (n,L)), the carrier of L;

         A5:

        now

          let p be object;

          assume p in the carrier of ( Polynom-Ring (n,L));

          then

          reconsider p9 = p as Polynomial of n, L by POLYNOM1:def 11;

          (f . p9) = ( eval (p9,x)) by A3

          .= (g . p9) by A4;

          hence (f . p) = (g . p);

        end;

        

         A6: ( dom g) = the carrier of ( Polynom-Ring (n,L)) by FUNCT_2:def 1;

        ( dom f) = the carrier of ( Polynom-Ring (n,L)) by FUNCT_2:def 1;

        hence thesis by A6, A5, FUNCT_1: 2;

      end;

    end

    registration

      let n be Ordinal, L be right_zeroed Abelian add-associative right_complementable well-unital distributive associative non trivial non empty doubleLoopStr;

      cluster ( Polynom-Ring (n,L)) -> well-unital;

      coherence ;

    end

    registration

      let n be Ordinal, L be Abelian right_zeroed add-associative right_complementable well-unital distributive associative non trivial non empty doubleLoopStr, x be Function of n, L;

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

      coherence

      proof

        set f = ( Polynom-Evaluation (n,L,x));

        

        thus (f . ( 1_ ( Polynom-Ring (n,L)))) = (f . ( 1_ (n,L))) by POLYNOM1: 31

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

        .= ( 1_ L) by Th13;

      end;

    end

    registration

      let n be Ordinal, L be right_zeroed add-associative right_complementable Abelian well-unital distributive non trivial doubleLoopStr, x be Function of n, L;

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

      coherence

      proof

        set f = ( Polynom-Evaluation (n,L,x));

        for p,q be Element of ( Polynom-Ring (n,L)) holds (f . (p + q)) = ((f . p) + (f . q))

        proof

          let p,q be Element of ( Polynom-Ring (n,L));

          reconsider p9 = p, q9 = q as Polynomial of n, L by POLYNOM1:def 11;

          reconsider p, q as Element of ( Polynom-Ring (n,L));

          

           A1: (f . p) = ( eval (p9,x)) by Def3;

          (f . (p + q)) = (f . (p9 + q9)) by POLYNOM1:def 11

          .= ( eval ((p9 + q9),x)) by Def3

          .= (( eval (p9,x)) + ( eval (q9,x))) by Th15;

          hence thesis by A1, Def3;

        end;

        hence thesis by VECTSP_1:def 20;

      end;

    end

    registration

      let n be Ordinal, L be right_zeroed add-associative right_complementable Abelian well-unital distributive commutative associative non trivial doubleLoopStr, x be Function of n, L;

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

      coherence

      proof

        set f = ( Polynom-Evaluation (n,L,x));

        for p,q be Element of ( Polynom-Ring (n,L)) holds (f . (p * q)) = ((f . p) * (f . q))

        proof

          let p,q be Element of ( Polynom-Ring (n,L));

          reconsider p9 = p, q9 = q as Polynomial of n, L by POLYNOM1:def 11;

          reconsider p, q as Element of ( Polynom-Ring (n,L));

          

           A1: (f . p) = ( eval (p9,x)) by Def3;

          (f . (p * q)) = (f . (p9 *' q9)) by POLYNOM1:def 11

          .= ( eval ((p9 *' q9),x)) by Def3

          .= (( eval (p9,x)) * ( eval (q9,x))) by Th17;

          hence thesis by A1, Def3;

        end;

        hence thesis by GROUP_6:def 6;

      end;

    end

    registration

      let n be Ordinal, L be right_zeroed add-associative right_complementable Abelian well-unital distributive commutative associative non trivial doubleLoopStr, x be Function of n, L;

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

      coherence ;

    end