polynom7.miz



    begin

    registration

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

      existence

      proof

        set R = the domRing;

        take R;

        thus thesis;

      end;

    end

    definition

      let X be set, R be non empty ZeroStr, p be Series of X, R;

      :: POLYNOM7:def1

      attr p is non-zero means p <> ( 0_ (X,R));

    end

    registration

      let X be set, R be non trivial ZeroStr;

      cluster non-zero for Series of X, R;

      existence

      proof

        set a = the Element of ( NonZero R);

        

         A1: not a in {( 0. R)} by XBOOLE_0:def 5;

        reconsider a as Element of R;

        set p = (( 0_ (X,R)) +* (( EmptyBag X),a));

        reconsider p as Function of ( Bags X), the carrier of R;

        reconsider p as Function of ( Bags X), R;

        reconsider p as Series of X, R;

        take p;

        ( 0_ (X,R)) = (( Bags X) --> ( 0. R)) by POLYNOM1:def 8;

        then ( dom ( 0_ (X,R))) = ( Bags X);

        then

         A2: (p . ( EmptyBag X)) = a by FUNCT_7: 31;

        a <> ( 0. R) by A1, TARSKI:def 1;

        then p <> ( 0_ (X,R)) by A2, POLYNOM1: 22;

        hence thesis;

      end;

    end

    registration

      let n be Ordinal, R be non trivial ZeroStr;

      cluster non-zero for Polynomial of n, R;

      existence

      proof

        set a = the Element of ( NonZero R);

        

         A1: not a in {( 0. R)} by XBOOLE_0:def 5;

        reconsider a as Element of R;

        set p = (( 0_ (n,R)) +* (( EmptyBag n),a));

        reconsider p as Function of ( Bags n), the carrier of R;

        reconsider p as Function of ( Bags n), R;

        reconsider p as Series of n, R;

         A2:

        now

          let u be object;

          assume

           A3: u in ( Support p);

          then u is Element of ( Bags n);

          then

           A4: u is bag of n;

          now

            assume u <> ( EmptyBag n);

            

            then (p . u) = (( 0_ (n,R)) . u) by FUNCT_7: 32

            .= ( 0. R) by A4, POLYNOM1: 22;

            hence contradiction by A3, POLYNOM1:def 4;

          end;

          hence u in {( EmptyBag n)} by TARSKI:def 1;

        end;

        ( 0_ (n,R)) = (( Bags n) --> ( 0. R)) by POLYNOM1:def 8;

        then ( dom ( 0_ (n,R))) = ( Bags n);

        then

         A5: (p . ( EmptyBag n)) = a by FUNCT_7: 31;

        now

          let u be object;

          assume u in {( EmptyBag n)};

          then

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

          a <> ( 0. R) by A1, TARSKI:def 1;

          hence u in ( Support p) by A5, A6, POLYNOM1:def 4;

        end;

        then ( Support p) = {( EmptyBag n)} by A2, TARSKI: 2;

        then

        reconsider p as Polynomial of n, R by POLYNOM1:def 5;

        take p;

        a <> ( 0. R) by A1, TARSKI:def 1;

        then p <> ( 0_ (n,R)) by A5, POLYNOM1: 22;

        hence thesis;

      end;

    end

    theorem :: POLYNOM7:1

    

     Th1: for X be set, R be non empty ZeroStr, s be Series of X, R holds s = ( 0_ (X,R)) iff ( Support s) = {}

    proof

      let X be set, R be non empty ZeroStr, s be Series of X, R;

       A1:

      now

        assume

         A2: ( Support s) = {} ;

        now

          let x be object;

          assume x in ( Bags X);

          then

          reconsider x9 = x as Element of ( Bags X);

          (s . x9) = ( 0. R) by A2, POLYNOM1:def 4;

          hence (s . x) = (( 0_ (X,R)) . x) by POLYNOM1: 22;

        end;

        hence s = ( 0_ (X,R));

      end;

      now

        assume

         A3: s = ( 0_ (X,R));

        now

          set x = the Element of ( Support s);

          assume ( Support s) <> {} ;

          then

           A4: x in ( Support s);

          then

          reconsider x as bag of X;

          (s . x) <> ( 0. R) by A4, POLYNOM1:def 4;

          hence contradiction by A3, POLYNOM1: 22;

        end;

        hence ( Support s) = {} ;

      end;

      hence thesis by A1;

    end;

    theorem :: POLYNOM7:2

    for X be set, R be non empty ZeroStr holds R is non trivial iff ex s be Series of X, R st ( Support s) <> {}

    proof

      let X be set, R be non empty ZeroStr;

       A1:

      now

        set x = ( EmptyBag X);

        assume R is non trivial;

        then

        consider a be Element of R such that

         A2: a <> ( 0. R);

        take s = (( Bags X) --> a);

        (s . x) = a;

        then ( EmptyBag X) in ( Support s) by A2, POLYNOM1:def 4;

        hence ex s be Series of X, R st ( Support s) <> {} ;

      end;

      now

        assume ex s be Series of X, R st ( Support s) <> {} ;

        then

        consider s be Series of X, R such that

         A3: ( Support s) <> {} ;

        set b = the Element of ( Support s);

        b in ( Support s) by A3;

        then

        reconsider b as Element of ( Bags X);

        now

          given x be object such that

           A4: the carrier of R = {x};

          ( 0. R) = x by A4, TARSKI:def 1

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

          hence contradiction by A3, POLYNOM1:def 4;

        end;

        hence R is non trivial by ZFMISC_1: 131;

      end;

      hence thesis by A1;

    end;

    definition

      let X be set, b be bag of X;

      :: POLYNOM7:def2

      attr b is univariate means ex u be Element of X st ( support b) = {u};

    end

    registration

      let X be non empty set;

      cluster univariate for bag of X;

      existence

      proof

        set x = the Element of X;

        set b = (( EmptyBag X) +* (x,1));

        take b;

        

         A1: ( dom ( EmptyBag X)) = X by PARTFUN1:def 2;

        then

         A2: (b . x) = ((( EmptyBag X) +* (x .--> 1)) . x) by FUNCT_7:def 3;

        

         A4: for u be object holds u in ( support b) implies u in {x}

        proof

          let u be object;

          assume

           A5: u in ( support b);

          now

            assume u <> x;

            then

             A6: not u in ( dom (x .--> 1)) by TARSKI:def 1;

            (b . u) = ((( EmptyBag X) +* (x .--> 1)) . u) by A1, FUNCT_7:def 3;

            

            then (b . u) = (( EmptyBag X) . u) by A6, FUNCT_4: 11

            .= 0 by PBOOLE: 5;

            hence contradiction by A5, PRE_POLY:def 7;

          end;

          hence thesis by TARSKI:def 1;

        end;

        x in ( dom (x .--> 1)) by TARSKI:def 1;

        

        then

         A7: (b . x) = ((x .--> 1) . x) by A2, FUNCT_4: 13

        .= 1 by FUNCOP_1: 72;

        for u be object holds u in {x} implies u in ( support b)

        proof

          let u be object;

          assume u in {x};

          then u = x by TARSKI:def 1;

          hence thesis by A7, PRE_POLY:def 7;

        end;

        then ( support b) = {x} by A4, TARSKI: 2;

        hence thesis;

      end;

    end

    registration

      let X be non empty set;

      cluster univariate -> non empty-yielding for bag of X;

      coherence

      proof

        let b be bag of X;

        assume b is univariate;

        then

        consider x be Element of X such that

         A1: ( support b) = {x};

        x in ( support b) by A1, TARSKI:def 1;

        then (b . x) <> 0 by PRE_POLY:def 7;

        then (b . x) <> (( EmptyBag X) . x) by PBOOLE: 5;

        hence thesis by PRE_POLY:def 18;

      end;

    end

    begin

    theorem :: POLYNOM7:3

    for b be bag of {} holds b = ( EmptyBag {} )

    proof

      set n = {} ;

      let b be bag of {} ;

      

       A1: for b be bag of n holds b = {}

      proof

        let b be bag of n;

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

        hence thesis by PRE_POLY: 51, TARSKI:def 1;

      end;

      then ( EmptyBag n) = {} ;

      hence thesis by A1;

    end;

    

     Lm1: for L be non empty doubleLoopStr, p be Polynomial of {} , L holds ex a be Element of L st p = ( {( EmptyBag {} )} --> a)

    proof

      set n = {} ;

      let L be non empty doubleLoopStr, p be Polynomial of {} , L;

      

       A1: for b be bag of {} holds b = {}

      proof

        let b be bag of {} ;

        b in ( Bags {} ) by PRE_POLY:def 12;

        hence thesis by PRE_POLY: 51, TARSKI:def 1;

      end;

      reconsider p as Function of ( Bags {} ), L;

      reconsider p as Function of { {} }, the carrier of L by PRE_POLY: 51;

      set a = (p /. {} );

      

       A2: ( dom p) = { {} } by FUNCT_2:def 1

      .= {( EmptyBag n)} by A1;

      

       A3: for u be object holds u in p implies u in [: {( EmptyBag n)}, {a}:]

      proof

        let u be object;

        assume

         A4: u in p;

        then

        consider p1,p2 be object such that

         A5: u = [p1, p2] by RELAT_1:def 1;

        

         A6: p1 in ( dom p) by A4, A5, XTUPLE_0:def 12;

        then

        reconsider p1 as bag of n by A2;

        

         A7: p2 is set by TARSKI: 1;

        

         A8: p1 = {} by A1;

        

        then p2 = (p . {} ) by A4, A5, A6, FUNCT_1:def 2, A7

        .= (p /. {} ) by A6, A8, PARTFUN1:def 6;

        then p2 in {a} by TARSKI:def 1;

        hence thesis by A2, A5, A6, ZFMISC_1:def 2;

      end;

      take a;

      

       A9: ( EmptyBag n) = {} by A1;

      for u be object holds u in [: {( EmptyBag n)}, {a}:] implies u in p

      proof

        let u be object;

        assume u in [: {( EmptyBag n)}, {a}:];

        then

        consider u1,u2 be object such that

         A10: u1 in {( EmptyBag n)} and

         A11: u2 in {a} and

         A12: u = [u1, u2] by ZFMISC_1:def 2;

        

         A13: u1 = {} by A9, A10, TARSKI:def 1;

        u2 = a by A11, TARSKI:def 1

        .= (p . {} ) by A2, A10, A13, PARTFUN1:def 6;

        hence thesis by A2, A10, A12, A13, FUNCT_1: 1;

      end;

      hence thesis by A3, TARSKI: 2;

    end;

    theorem :: POLYNOM7:4

    for L be right_zeroed add-associative right_complementable well-unital distributive non trivial doubleLoopStr, p be Polynomial of {} , L, x be Function of {} , L holds ( eval (p,x)) = (p . ( EmptyBag {} ))

    proof

      set n = {} ;

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

      

       A1: for b be bag of n holds b = {}

      proof

        let b be bag of n;

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

        hence thesis by PRE_POLY: 51, TARSKI:def 1;

      end;

      then

       A2: ( EmptyBag n) = {} ;

      consider a be Element of L such that

       A3: p = ( {( EmptyBag n)} --> a) by Lm1;

      

       A4: (p . ( EmptyBag n)) = a by A3;

      

       A5: ( dom p) = {( EmptyBag n)} by A3;

      now

        per cases ;

          case

           A6: a = ( 0. L);

          ( Support p) = {}

          proof

            set u = the Element of ( Support p);

            assume

             A7: ( Support p) <> {} ;

            then u in ( Support p);

            then

            reconsider u as Element of ( Bags n);

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

            hence thesis by A1, A2, A4, A6;

          end;

          then

          reconsider Sp = ( Support p) as empty Subset of ( Bags n);

          consider y be FinSequence of the carrier of L such that

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

           A9: ( eval (p,x)) = ( Sum y) and 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 POLYNOM2:def 4;

          ( SgmX (( BagOrder n),Sp)) = {} by POLYNOM2: 18, PRE_POLY: 76;

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

          hence ( eval (p,x)) = a by A6, A9, RLVECT_1: 43;

        end;

          case

           A10: a <> ( 0. L);

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

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

          

           A11: ( BagOrder n) linearly_orders sp by POLYNOM2: 18;

          

           A12: for u be object holds u in ( Support p) implies u in { {} }

          proof

            let u be object;

            assume u in ( Support p);

            then

            reconsider u as Element of ( Bags n);

            u = {} by A1;

            hence thesis by TARSKI:def 1;

          end;

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

          proof

            let u be object;

            assume u in { {} };

            then u = ( EmptyBag n) by A2, TARSKI:def 1;

            hence thesis by A4, A10, POLYNOM1:def 4;

          end;

          then ( Support p) = { {} } by A12, TARSKI: 2;

          then

           A13: ( rng sg) = { {} } by A11, PRE_POLY:def 2;

          then

           A14: {} in ( rng sg) by TARSKI:def 1;

          then

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

          then (sg . 1) in ( dom p) by A2, A5, A13, FUNCT_1: 3;

          then 1 in ( dom (p * sg)) by A15, FUNCT_1: 11;

          

          then

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

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

          .= a by A2, A3, A13, A15, FUNCOP_1: 7, FUNCT_1: 3;

          

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

          proof

            let u be object;

            assume

             A18: u in ( dom sg);

            assume

             A19: not u in {1};

            reconsider u as Element of NAT by A18;

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

            then

             A20: (sg /. u) in ( rng sg) by A18, FUNCT_1: 3;

            

             A21: u <> 1 by A19, TARSKI:def 1;

            

             A22: 1 < u

            proof

              consider k be Nat such that

               A23: ( dom sg) = ( 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 A18, A23;

              hence thesis by A21, XXREAL_0: 1;

            end;

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

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

            

            then (sg /. 1) = {} by A13, TARSKI:def 1

            .= (sg /. u) by A13, A20, TARSKI:def 1;

            hence thesis by A11, A15, A18, A22, PRE_POLY:def 2;

          end;

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

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

          then

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

          consider y be FinSequence of the carrier of L such that

           A25: ( len y) = ( len sg) and

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

           A27: for i be Element of NAT st 1 <= i & i <= ( len y) holds (y /. i) = (((p * sg) /. i) * ( eval ((sg /. i),x))) by POLYNOM2:def 4;

          ( dom y) = ( Seg ( len y)) by FINSEQ_1:def 3

          .= ( dom sg) by A25, FINSEQ_1:def 3;

          

          then (y . 1) = (y /. 1) by A14, FINSEQ_3: 31, PARTFUN1:def 6

          .= (((p * sg) /. 1) * ( eval ((sg /. 1),x))) by A24, A25, A27

          .= (((p * sg) /. 1) * ( eval (( EmptyBag n),x))) by A1, A2

          .= (((p * sg) /. 1) * ( 1. L)) by POLYNOM2: 14

          .= a by A16;

          then y = <*a*> by A24, A25, FINSEQ_1: 40;

          hence ( eval (p,x)) = a by A26, RLVECT_1: 44;

        end;

      end;

      hence thesis by A3;

    end;

    theorem :: POLYNOM7:5

    for L be right_zeroed add-associative right_complementable Abelian well-unital distributive associative non trivial non trivial doubleLoopStr holds ( Polynom-Ring ( {} ,L)) is_ringisomorph_to L

    proof

      set n = {} ;

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

      set PL = ( Polynom-Ring (n,L));

      defpred P[ set, set] means ex p be Polynomial of n, L st p = $1 & (p . {} ) = $2;

      

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

      

       A2: ( EmptyBag n) in ( dom (( EmptyBag n) .--> ( 1_ L))) by TARSKI:def 1;

      

       A3: for b be bag of {} holds b = {}

      proof

        let b be bag of {} ;

        b in ( Bags {} ) by PRE_POLY:def 12;

        hence thesis by PRE_POLY: 51, TARSKI:def 1;

      end;

      then

       A4: ( EmptyBag n) = {} ;

      then

      reconsider i = {} as bag of n;

      

       A5: for x be Element of PL holds ex y be Element of L st P[x, y]

      proof

        let x be Element of PL;

        reconsider p = x as Polynomial of n, L by POLYNOM1:def 11;

        take (p . {} );

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

        then

         A6: (p . {} ) in ( rng p) by A4, FUNCT_1: 3;

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

        hence thesis by A6;

      end;

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

       A7: for x be Element of PL holds P[x, (f . x)] from FUNCT_2:sch 3( A5);

      

       A8: ( dom f) = the carrier of PL by FUNCT_2:def 1;

      reconsider f as Function of PL, L;

      consider p be Polynomial of n, L such that

       A9: p = ( 1_ PL) and

       A10: (p . {} ) = (f . ( 1. PL)) by A7;

      

       A11: p = ( 1_ (n,L)) by A9, POLYNOM1: 31

      .= (( 0_ (n,L)) +* (( EmptyBag n),( 1_ L))) by POLYNOM1:def 9;

      for x,y be Element of PL holds (f . (x * y)) = ((f . x) * (f . y))

      proof

        let x,y be Element of PL;

        consider p be Polynomial of n, L such that

         A12: p = x & (p . {} ) = (f . x) by A7;

        consider q be Polynomial of n, L such that

         A13: q = y & (q . {} ) = (f . y) by A7;

        

         A14: ((p *' q) . {} ) = ((p . i) * (q . i))

        proof

          

           A15: ( decomp ( EmptyBag n)) = <* <*( EmptyBag n), ( EmptyBag n)*>*> by PRE_POLY: 73;

          then

           A16: ( len ( decomp ( EmptyBag n))) = 1 by FINSEQ_1: 39;

          set z = ((p . i) * (q . i));

          consider s be FinSequence of the carrier of L such that

           A17: ((p *' q) . ( EmptyBag n)) = ( Sum s) and

           A18: ( len s) = ( len ( decomp ( EmptyBag n))) and

           A19: for k be Element of NAT st k in ( dom s) holds ex b1,b2 be bag of n st (( decomp ( EmptyBag n)) /. k) = <*b1, b2*> & (s /. k) = ((p . b1) * (q . b2)) by POLYNOM1:def 10;

          ( len s) = 1 by A15, A18, FINSEQ_1: 39;

          then ( Seg 1) = ( dom s) by FINSEQ_1:def 3;

          then

           A20: 1 in ( dom s) by FINSEQ_1: 2, TARSKI:def 1;

          then

          consider b1,b2 be bag of n such that (( decomp ( EmptyBag n)) /. 1) = <*b1, b2*> and

           A21: (s /. 1) = ((p . b1) * (q . b2)) by A19;

          (s . 1) = ((p . b1) * (q . b2)) by A20, A21, PARTFUN1:def 6

          .= ((p . i) * (q . b2)) by A3

          .= ((p . i) * (q . i)) by A3;

          then s = <*z*> by A16, A18, FINSEQ_1: 40;

          then ( Sum s) = z by RLVECT_1: 44;

          hence thesis by A3, A17;

        end;

        ex pq be Polynomial of n, L st pq = (x * y) & (pq . {} ) = (f . (x * y)) by A7;

        hence thesis by A12, A13, A14, POLYNOM1:def 11;

      end;

      then

       A22: f is multiplicative by GROUP_6:def 6;

      for x,y be Element of PL holds (f . (x + y)) = ((f . x) + (f . y))

      proof

        let x,y be Element of PL;

        consider p be Polynomial of n, L such that

         A23: p = x and

         A24: (p . {} ) = (f . x) by A7;

        consider q be Polynomial of n, L such that

         A25: q = y and

         A26: (q . {} ) = (f . y) by A7;

        consider a be Element of L such that

         A27: p = ( {( EmptyBag n)} --> a) by Lm1;

        

         A28: ex pq be Polynomial of n, L st pq = (x + y) & (pq . {} ) = (f . (x + y)) by A7;

        consider b be Element of L such that

         A29: q = ( {( EmptyBag n)} --> b) by Lm1;

        

         A30: (p . {} ) = a by A4, A27;

        

         A31: ((p + q) . {} ) = ((p . i) + (q . i)) by POLYNOM1: 15

        .= (a + b) by A4, A30, A29;

        (q . {} ) = b by A4, A29;

        then ((f . x) + (f . y)) = (a + b) by A4, A24, A26, A27;

        hence thesis by A23, A25, A28, A31, POLYNOM1:def 11;

      end;

      then

       A32: f is additive by VECTSP_1:def 20;

      (p . i) = (p . ( EmptyBag n)) by A3

      .= ((( 0_ (n,L)) +* (( EmptyBag n) .--> ( 1_ L))) . ( EmptyBag n)) by A11, A1, FUNCT_7:def 3

      .= ((( EmptyBag n) .--> ( 1_ L)) . ( EmptyBag n)) by A2, FUNCT_4: 13

      .= ( 1_ L) by FUNCOP_1: 72;

      then f is unity-preserving by A9, A10, GROUP_1:def 13;

      then

       A33: f is RingHomomorphism by A32, A22;

      

       A34: for u be object holds u in the carrier of L implies u in ( rng f)

      proof

        let u be object;

        assume u in the carrier of L;

        then

        reconsider u as Element of L;

        set p = (( EmptyBag n) .--> u);

        reconsider p as Function;

        ( rng p) = {u} & ( dom p) = ( Bags n) by FUNCOP_1: 8, PRE_POLY: 51, TARSKI:def 1;

        then

        reconsider p as Function of ( Bags n), the carrier of L by FUNCT_2: 2;

        reconsider p as Function of ( Bags n), L;

        reconsider p as Series of n, L;

        now

          per cases ;

            case

             A35: u = ( 0. L);

            ( Support p) = {}

            proof

              set v = the Element of ( Support p);

              assume ( Support p) <> {} ;

              then

               A36: v in ( Support p);

              then v is bag of n;

              

              then (p . v) = (p . ( EmptyBag n)) by A3, A4

              .= u by FUNCOP_1: 72;

              hence thesis by A35, A36, POLYNOM1:def 4;

            end;

            hence ( Support p) is finite;

          end;

            case

             A37: u <> ( 0. L);

            

             A38: for v be object holds v in {( EmptyBag n)} implies v in ( Support p)

            proof

              let v be object;

              assume

               A39: v in {( EmptyBag n)};

              then

              reconsider v as Element of ( Bags n);

              (p . v) = (p . ( EmptyBag n)) by A39, TARSKI:def 1

              .= u by FUNCOP_1: 72;

              hence thesis by A37, POLYNOM1:def 4;

            end;

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

            proof

              let v be object;

              assume v in ( Support p);

              then

              reconsider v as bag of n;

              v = ( EmptyBag n) by A3, A4;

              hence thesis by TARSKI:def 1;

            end;

            hence ( Support p) is finite by A38, TARSKI: 2;

          end;

        end;

        then

        reconsider p as Polynomial of n, L by POLYNOM1:def 5;

        reconsider p9 = p as Element of PL by POLYNOM1:def 11;

        consider q be Polynomial of n, L such that

         A40: q = p9 and

         A41: (q . {} ) = (f . p9) by A7;

        (q . {} ) = (p . ( EmptyBag n)) by A3, A40

        .= u by FUNCOP_1: 72;

        hence thesis by A8, A41, FUNCT_1: 3;

      end;

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

      then for u be object holds u in ( rng f) implies u in the carrier of L;

      then ( rng f) = the carrier of L by A34, TARSKI: 2;

      then f is onto;

      then

       A42: f is RingEpimorphism by A33;

      for x1,x2 be object st x1 in ( dom f) & x2 in ( dom f) & (f . x1) = (f . x2) holds x1 = x2

      proof

        let x1,x2 be object;

        assume that

         A43: x1 in ( dom f) & x2 in ( dom f) and

         A44: (f . x1) = (f . x2);

        reconsider x1, x2 as Element of PL by A43;

        consider p be Polynomial of n, L such that

         A45: p = x1 & (p . {} ) = (f . x1) by A7;

        consider q be Polynomial of n, L such that

         A46: q = x2 & (q . {} ) = (f . x2) by A7;

        consider a2 be Element of L such that

         A47: q = ( {( EmptyBag n)} --> a2) by Lm1;

        

         A48: (q . ( EmptyBag n)) = a2 by A47;

        

         A49: (p . {} ) = (p . ( EmptyBag n)) by A3;

        consider a1 be Element of L such that

         A50: p = ( {( EmptyBag n)} --> a1) by Lm1;

        thus thesis by A3, A44, A45, A46, A50, A47, A48, A49;

      end;

      then f is one-to-one by FUNCT_1:def 4;

      then f is RingMonomorphism by A33;

      then f is RingIsomorphism by A42;

      hence thesis by QUOFIELD:def 23;

    end;

    begin

    definition

      let X be set, L be non empty ZeroStr, p be Series of X, L;

      :: POLYNOM7:def3

      attr p is monomial-like means

      : Def3: ex b be bag of X st for b9 be bag of X st b9 <> b holds (p . b9) = ( 0. L);

    end

    registration

      let X be set, L be non empty ZeroStr;

      cluster monomial-like for Series of X, L;

      existence

      proof

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

        take p;

        for b9 be bag of X st b9 <> ( EmptyBag X) holds (p . b9) = ( 0. L) by POLYNOM1: 22;

        hence thesis;

      end;

    end

    definition

      let X be set, L be non empty ZeroStr;

      mode Monomial of X,L is monomial-like Series of X, L;

    end

    registration

      let X be set, L be non empty ZeroStr;

      cluster monomial-like -> finite-Support for Series of X, L;

      coherence

      proof

        let s be Series of X, L;

        assume s is monomial-like;

        then

        consider b be bag of X such that

         A1: for b9 be bag of X st b9 <> b holds (s . b9) = ( 0. L);

        per cases ;

          suppose

           A2: (s . b) = ( 0. L);

          now

            assume ( Support s) <> {} ;

            then

            reconsider sp = ( Support s) as non empty Subset of ( Bags X);

            set c = the Element of sp;

            (s . c) <> ( 0. L) by POLYNOM1:def 4;

            hence contradiction by A1, A2;

          end;

          hence thesis by POLYNOM1:def 5;

        end;

          suppose

           A3: (s . b) <> ( 0. L);

           A4:

          now

            let u be object;

            assume

             A5: u in ( Support s);

            then

            reconsider u9 = u as Element of ( Bags X);

            (s . u9) <> ( 0. L) by A5, POLYNOM1:def 4;

            then u9 = b by A1;

            hence u in {b} by TARSKI:def 1;

          end;

          now

            let u be object;

            assume u in {b};

            then

             A6: u = b by TARSKI:def 1;

            then

            reconsider u9 = u as Element of ( Bags X) by PRE_POLY:def 12;

            u9 in ( Support s) by A3, A6, POLYNOM1:def 4;

            hence u in ( Support s);

          end;

          then ( Support s) = {b} by A4, TARSKI: 2;

          hence thesis by POLYNOM1:def 5;

        end;

      end;

    end

    theorem :: POLYNOM7:6

    

     Th6: for X be set, L be non empty ZeroStr, p be Series of X, L holds p is Monomial of X, L iff (( Support p) = {} or ex b be bag of X st ( Support p) = {b})

    proof

      let n be set, L be non empty ZeroStr, p be Series of n, L;

       A1:

      now

        assume ex b be bag of n st ( Support p) = {b};

        then

        consider b be bag of n such that

         A2: ( Support p) = {b};

        for b9 be bag of n st b9 <> b holds (p . b9) = ( 0. L)

        proof

          let b9 be bag of n;

          assume

           A3: b9 <> b;

          assume

           A4: (p . b9) <> ( 0. L);

          reconsider b9 as Element of ( Bags n) by PRE_POLY:def 12;

          b9 in ( Support p) by A4, POLYNOM1:def 4;

          hence thesis by A2, A3, TARSKI:def 1;

        end;

        hence p is Monomial of n, L by Def3;

      end;

       A5:

      now

        assume p is Monomial of n, L;

        then

        consider b be bag of n such that

         A6: for b9 be bag of n st b9 <> b holds (p . b9) = ( 0. L) by Def3;

        now

          per cases ;

            case

             A7: (p . b) <> ( 0. L);

            

             A8: for u be object holds u in {b} implies u in ( Support p)

            proof

              let u be object;

              assume

               A9: u in {b};

              then u = b by TARSKI:def 1;

              then

              reconsider u9 = u as Element of ( Bags n) by PRE_POLY:def 12;

              (p . u9) <> ( 0. L) by A7, A9, TARSKI:def 1;

              hence thesis by POLYNOM1:def 4;

            end;

            for u be object holds u in ( Support p) implies u in {b}

            proof

              let u be object;

              assume

               A10: u in ( Support p);

              then

              reconsider u9 = u as bag of n;

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

              then u9 = b by A6;

              hence thesis by TARSKI:def 1;

            end;

            then ( Support p) = {b} by A8, TARSKI: 2;

            hence ex b be bag of n st ( Support p) = {b};

          end;

            case

             A11: (p . b) = ( 0. L);

            thus ( Support p) = {}

            proof

              assume ( Support p) <> {} ;

              then

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

              set c = the Element of sp;

              (p . c) <> ( 0. L) by POLYNOM1:def 4;

              hence thesis by A6, A11;

            end;

          end;

        end;

        hence ( Support p) = {} or ex b be bag of n st ( Support p) = {b};

      end;

      now

        set b = the bag of n;

        assume

         A12: ( Support p) = {} ;

        for b9 be bag of n st b9 <> b holds (p . b9) = ( 0. L)

        proof

          let b9 be bag of n;

          assume b9 <> b;

          reconsider c = b9 as Element of ( Bags n) by PRE_POLY:def 12;

          assume (p . b9) <> ( 0. L);

          then c in ( Support p) by POLYNOM1:def 4;

          hence thesis by A12;

        end;

        hence p is Monomial of n, L by Def3;

      end;

      hence thesis by A1, A5;

    end;

    definition

      let X be set, L be non empty ZeroStr, a be Element of L, b be bag of X;

      :: POLYNOM7:def4

      func Monom (a,b) -> Monomial of X, L equals (( 0_ (X,L)) +* (b,a));

      coherence

      proof

        

         A1: b in ( dom (b .--> a)) by TARSKI:def 1;

        set m = (( 0_ (X,L)) +* (b,a));

        reconsider m as Function of ( Bags X), the carrier of L;

        reconsider m as Function of ( Bags X), L;

        reconsider m as Series of X, L;

        

         A2: b in ( Bags X) by PRE_POLY:def 12;

        

         A3: ( dom ( 0_ (X,L))) = ( dom (( Bags X) --> ( 0. L))) by POLYNOM1:def 8

        .= ( Bags X);

        then

         A4: m = (( 0_ (X,L)) +* (b .--> a)) by A2, FUNCT_7:def 3;

        

         A5: (m . b) = ((( 0_ (X,L)) +* (b .--> a)) . b) by A3, A2, FUNCT_7:def 3

        .= ((b .--> a) . b) by A1, FUNCT_4: 13

        .= a by FUNCOP_1: 72;

        now

          per cases ;

            case

             A6: a <> ( 0. L);

            

             A7: for u be object holds u in ( Support m) implies u in {b}

            proof

              let u be object;

              assume

               A8: u in ( Support m);

              assume not u in {b};

              then

               A9: not u in ( dom (b .--> a));

              reconsider u as bag of X by A8;

              (m . u) = (( 0_ (X,L)) . u) by A4, A9, FUNCT_4: 11

              .= ( 0. L) by POLYNOM1: 22;

              hence thesis by A8, POLYNOM1:def 4;

            end;

            b in ( Support m) by A2, A5, A6, POLYNOM1:def 4;

            then for u be object holds u in {b} implies u in ( Support m) by TARSKI:def 1;

            then ( Support m) = {b} by A7, TARSKI: 2;

            hence thesis by Th6;

          end;

            case

             A10: a = ( 0. L);

            now

              assume ( Support m) <> {} ;

              then

              reconsider sm = ( Support m) as non empty Subset of ( Bags X);

              set c = the Element of sm;

              (m . c) <> ( 0. L) by POLYNOM1:def 4;

              then not c in {b} by A5, A10, TARSKI:def 1;

              then

               A11: not c in ( dom (b .--> a));

              reconsider c as bag of X;

              (m . c) = (( 0_ (X,L)) . c) by A4, A11, FUNCT_4: 11

              .= ( 0. L) by POLYNOM1: 22;

              hence contradiction by POLYNOM1:def 4;

            end;

            hence thesis by Th6;

          end;

        end;

        hence thesis;

      end;

    end

    definition

      let X be set, L be non empty ZeroStr, m be Monomial of X, L;

      :: POLYNOM7:def5

      func term (m) -> bag of X means

      : Def5: (m . it ) <> ( 0. L) or ( Support m) = {} & it = ( EmptyBag X);

      existence

      proof

        consider b be bag of X such that

         A1: for b9 be bag of X st b9 <> b holds (m . b9) = ( 0. L) by Def3;

        now

          per cases ;

            case (m . b) <> ( 0. L);

            hence thesis;

          end;

            case

             A2: (m . b) = ( 0. L);

            ( Support m) = {}

            proof

              assume ( Support m) <> {} ;

              then

              reconsider sm = ( Support m) as non empty Subset of ( Bags X);

              set c = the Element of sm;

              (m . c) <> ( 0. L) by POLYNOM1:def 4;

              hence thesis by A1, A2;

            end;

            hence thesis;

          end;

        end;

        hence thesis;

      end;

      uniqueness

      proof

        let b1,b2 be bag of X;

        assume

         A3: (m . b1) <> ( 0. L) or ( Support m) = {} & b1 = ( EmptyBag X);

        consider b be bag of X such that

         A4: for b9 be bag of X st b9 <> b holds (m . b9) = ( 0. L) by Def3;

        assume

         A5: (m . b2) <> ( 0. L) or ( Support m) = {} & b2 = ( EmptyBag X);

        now

          per cases ;

            case

             A6: (m . b1) <> ( 0. L);

            reconsider b19 = b1 as Element of ( Bags X) by PRE_POLY:def 12;

            

             A7: b19 in ( Support m) by A6, POLYNOM1:def 4;

            

            thus b1 = b by A4, A6

            .= b2 by A5, A4, A7;

          end;

            case

             A8: (m . b1) = ( 0. L);

            now

              per cases by A5;

                case

                 A9: (m . b2) <> ( 0. L);

                reconsider b29 = b2 as Element of ( Bags X) by PRE_POLY:def 12;

                b29 in ( Support m) by A9, POLYNOM1:def 4;

                hence thesis by A3, A8;

              end;

                case ( Support m) = {} & b2 = ( EmptyBag X);

                hence thesis by A3, A8;

              end;

            end;

            hence thesis;

          end;

        end;

        hence thesis;

      end;

    end

    definition

      let X be set, L be non empty ZeroStr, m be Monomial of X, L;

      :: POLYNOM7:def6

      func coefficient (m) -> Element of L equals (m . ( term m));

      coherence ;

    end

    theorem :: POLYNOM7:7

    

     Th7: for X be set, L be non empty ZeroStr, m be Monomial of X, L holds ( Support m) = {} or ( Support m) = {( term m)}

    proof

      let X be set, L be non empty ZeroStr, m be Monomial of X, L;

      

       A1: ( term m) is Element of ( Bags X) by PRE_POLY:def 12;

      assume

       A2: ( Support m) <> {} ;

      then (m . ( term m)) <> ( 0. L) by Def5;

      then

       A3: ( term m) in ( Support m) by A1, POLYNOM1:def 4;

      ex b be bag of X st ( Support m) = {b} by A2, Th6;

      hence thesis by A3, TARSKI:def 1;

    end;

    theorem :: POLYNOM7:8

    

     Th8: for X be set, L be non empty ZeroStr, b be bag of X holds ( coefficient ( Monom (( 0. L),b))) = ( 0. L) & ( term ( Monom (( 0. L),b))) = ( EmptyBag X)

    proof

      let n be set, L be non empty ZeroStr, b be bag of n;

      set m = (( 0_ (n,L)) +* (b,( 0. L)));

      reconsider m as Function of ( Bags n), the carrier of L;

      reconsider m as Function of ( Bags n), L;

      reconsider m as Series of n, L;

      

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

      

       A2: ( dom ( 0_ (n,L))) = ( dom (( Bags n) --> ( 0. L))) by POLYNOM1:def 8

      .= ( Bags n);

      then

       A3: m = (( 0_ (n,L)) +* (b .--> ( 0. L))) by A1, FUNCT_7:def 3;

      

       A4: b in ( dom (b .--> ( 0. L))) by TARSKI:def 1;

      

       A5: (m . b) = ((( 0_ (n,L)) +* (b .--> ( 0. L))) . b) by A2, A1, FUNCT_7:def 3

      .= ((b .--> ( 0. L)) . b) by A4, FUNCT_4: 13

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

       A6:

      now

        let b9 be bag of n;

        now

          per cases ;

            case b9 = b;

            hence (m . b9) = ( 0. L) by A5;

          end;

            case b9 <> b;

            then not b9 in ( dom (b .--> ( 0. L))) by TARSKI:def 1;

            

            hence (m . b9) = (( 0_ (n,L)) . b9) by A3, FUNCT_4: 11

            .= ( 0. L) by POLYNOM1: 22;

          end;

        end;

        hence (m . b9) = ( 0. L);

      end;

      hence ( coefficient ( Monom (( 0. L),b))) = ( 0. L);

      (( Monom (( 0. L),b)) . ( term ( Monom (( 0. L),b)))) = ( 0. L) by A6;

      hence thesis by Def5;

    end;

    theorem :: POLYNOM7:9

    

     Th9: for X be set, L be non empty ZeroStr, a be Element of L, b be bag of X holds ( coefficient ( Monom (a,b))) = a

    proof

      let n be set, L be non empty ZeroStr, a be Element of L, b be bag of n;

      set m = (( 0_ (n,L)) +* (b,a));

      reconsider m as Function of ( Bags n), the carrier of L;

      reconsider m as Function of ( Bags n), L;

      reconsider m as Series of n, L;

      

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

      

       A2: b in ( dom (b .--> a)) by TARSKI:def 1;

      ( dom ( 0_ (n,L))) = ( dom (( Bags n) --> ( 0. L))) by POLYNOM1:def 8

      .= ( Bags n);

      

      then

       A3: (m . b) = ((( 0_ (n,L)) +* (b .--> a)) . b) by A1, FUNCT_7:def 3

      .= ((b .--> a) . b) by A2, FUNCT_4: 13

      .= a by FUNCOP_1: 72;

      per cases ;

        suppose (m . b) <> ( 0. L);

        hence thesis by A3, Def5;

      end;

        suppose (m . b) = ( 0. L);

        hence thesis by A3, Th8;

      end;

    end;

    theorem :: POLYNOM7:10

    

     Th10: for X be set, L be non trivial ZeroStr, a be non zero Element of L, b be bag of X holds ( term ( Monom (a,b))) = b

    proof

      let n be set, L be non trivial ZeroStr, a be non zero Element of L, b be bag of n;

      set m = (( 0_ (n,L)) +* (b,a));

      reconsider m as Function of ( Bags n), the carrier of L;

      reconsider m as Function of ( Bags n), L;

      reconsider m as Series of n, L;

      

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

      

       A2: b in ( dom (b .--> a)) by TARSKI:def 1;

      ( dom ( 0_ (n,L))) = ( dom (( Bags n) --> ( 0. L))) by POLYNOM1:def 8

      .= ( Bags n);

      

      then (m . b) = ((( 0_ (n,L)) +* (b .--> a)) . b) by A1, FUNCT_7:def 3

      .= ((b .--> a) . b) by A2, FUNCT_4: 13

      .= a by FUNCOP_1: 72;

      then (m . b) <> ( 0. L);

      hence thesis by Def5;

    end;

    theorem :: POLYNOM7:11

    for X be set, L be non empty ZeroStr, m be Monomial of X, L holds ( Monom (( coefficient m),( term m))) = m

    proof

      let X be set, L be non empty ZeroStr, m be Monomial of X, L;

      per cases by Th6;

        suppose

         A1: ( Support m) = {} ;

         A2:

        now

          

           A3: ( term m) is Element of ( Bags X) by PRE_POLY:def 12;

          assume ( coefficient m) <> ( 0. L);

          hence contradiction by A1, A3, POLYNOM1:def 4;

        end;

        

         A4: m = ( 0_ (X,L)) by A1, Th1;

        set m9 = ( Monom (( coefficient m),( term m)));

        

         A5: ( dom ( 0_ (X,L))) = ( dom (( Bags X) --> ( 0. L))) by POLYNOM1:def 8

        .= ( Bags X);

        

         A6: ( EmptyBag X) in ( dom (( EmptyBag X) .--> ( 0. L))) by TARSKI:def 1;

        

         A7: ( term m) = ( EmptyBag X) by A1, Def5;

        

        then

         A8: (m9 . ( EmptyBag X)) = ((( 0_ (X,L)) +* (( EmptyBag X) .--> ( 0. L))) . ( EmptyBag X)) by A2, A5, FUNCT_7:def 3

        .= ((( EmptyBag X) .--> ( 0. L)) . ( EmptyBag X)) by A6, FUNCT_4: 13

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

        now

          let x be object;

          assume x in ( Bags X);

          then

          reconsider x9 = x as Element of ( Bags X);

          now

            per cases ;

              case x9 = ( EmptyBag X);

              hence (m9 . x9) = ( 0. L) by A8;

            end;

              case x <> ( EmptyBag X);

              then

               A9: not x9 in ( dom (( EmptyBag X) .--> ( 0. L))) by TARSKI:def 1;

              (m9 . x9) = ((( 0_ (X,L)) +* (( EmptyBag X) .--> ( 0. L))) . x9) by A7, A2, A5, FUNCT_7:def 3

              .= (( 0_ (X,L)) . x9) by A9, FUNCT_4: 11;

              hence (m9 . x9) = ( 0. L) by POLYNOM1: 22;

            end;

          end;

          hence (m . x) = (m9 . x) by A4, POLYNOM1: 22;

        end;

        hence thesis;

      end;

        suppose ex b be bag of X st ( Support m) = {b};

        then

        consider b be bag of X such that

         A10: ( Support m) = {b};

        set a = (m . b);

        

         A11: b in ( dom (b .--> a)) by TARSKI:def 1;

        set m9 = ( Monom (( coefficient m),( term m)));

        

         A12: ( dom ( 0_ (X,L))) = ( dom (( Bags X) --> ( 0. L))) by POLYNOM1:def 8

        .= ( Bags X);

        

         A13: b in ( Support m) by A10, TARSKI:def 1;

        then a <> ( 0. L) by POLYNOM1:def 4;

        then

         A14: ( term m) = b by Def5;

         A15:

        now

          let u be object;

          assume

           A16: u in ( Support ( Monom (( coefficient m),( term m))));

          then

          reconsider u9 = u as Element of ( Bags X);

          now

            assume u <> b;

            then

             A17: not u9 in ( dom (b .--> a)) by TARSKI:def 1;

            b in ( dom ( 0_ (X,L))) by A12, PRE_POLY:def 12;

            

            then (m9 . u9) = ((( 0_ (X,L)) +* (b .--> a)) . u9) by A14, FUNCT_7:def 3

            .= (( 0_ (X,L)) . u9) by A17, FUNCT_4: 11;

            hence (m9 . u9) = ( 0. L) by POLYNOM1: 22;

          end;

          hence u in {b} by A16, POLYNOM1:def 4, TARSKI:def 1;

        end;

        b in ( Bags X) by PRE_POLY:def 12;

        

        then

         A18: (m9 . b) = ((( 0_ (X,L)) +* (b .--> a)) . b) by A14, A12, FUNCT_7:def 3

        .= ((b .--> a) . b) by A11, FUNCT_4: 13

        .= a by FUNCOP_1: 72;

        now

          let u be object;

          assume u in {b};

          then

           A19: u = b by TARSKI:def 1;

          (m9 . b) <> ( 0. L) by A13, A18, POLYNOM1:def 4;

          hence u in ( Support ( Monom (( coefficient m),( term m)))) by A13, A19, POLYNOM1:def 4;

        end;

        then

         A20: ( Support ( Monom (( coefficient m),( term m)))) = {b} by A15, TARSKI: 2;

        now

          let x be object;

          assume x in ( Bags X);

          then

          reconsider x9 = x as Element of ( Bags X);

          now

            per cases ;

              case x = b;

              hence (( Monom (( coefficient m),( term m))) . x9) = (m . x9) by A18;

            end;

              case

               A21: x <> b;

              then

               A22: not x in ( Support ( Monom (( coefficient m),( term m)))) by A20, TARSKI:def 1;

               not x in ( Support m) by A10, A21, TARSKI:def 1;

              

              hence (m . x9) = ( 0. L) by POLYNOM1:def 4

              .= (( Monom (( coefficient m),( term m))) . x9) by A22, POLYNOM1:def 4;

            end;

          end;

          hence (m . x) = (( Monom (( coefficient m),( term m))) . x);

        end;

        hence thesis;

      end;

    end;

    theorem :: POLYNOM7:12

    

     Th12: for n be Ordinal, L be right_zeroed add-associative right_complementable well-unital distributive non trivial doubleLoopStr, m be Monomial of n, L, x be Function of n, L holds ( eval (m,x)) = (( coefficient m) * ( eval (( term m),x)))

    proof

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

      consider y be FinSequence of the carrier of L such that

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

       A2: ( eval (m,x)) = ( Sum y) and

       A3: for i be Element of NAT st 1 <= i & i <= ( len y) holds (y /. i) = (((m * ( SgmX (( BagOrder n),( Support m)))) /. i) * ( eval ((( SgmX (( BagOrder n),( Support m))) /. i),x))) by POLYNOM2:def 4;

      consider b be bag of n such that

       A4: for b9 be bag of n st b9 <> b holds (m . b9) = ( 0. L) by Def3;

      now

        per cases ;

          case

           A5: (m . b) <> ( 0. L);

          

           A6: for u be object holds u in ( Support m) implies u in {b}

          proof

            let u be object;

            assume

             A7: u in ( Support m);

            assume

             A8: not u in {b};

            reconsider u as Element of ( Bags n) by A7;

            u <> b by A8, TARSKI:def 1;

            then (m . u) = ( 0. L) by A4;

            hence thesis by A7, POLYNOM1:def 4;

          end;

          

           A9: b in ( Bags n) & ( dom m) = ( Bags n) by FUNCT_2:def 1, PRE_POLY:def 12;

          reconsider sm = ( Support m) as finite Subset of ( Bags n);

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

          

           A10: ( BagOrder n) linearly_orders sm by POLYNOM2: 18;

          for u be object holds u in {b} implies u in ( Support m)

          proof

            let u be object;

            assume

             A11: u in {b};

            then u = b by TARSKI:def 1;

            then

            reconsider u as Element of ( Bags n) by PRE_POLY:def 12;

            (m . u) <> ( 0. L) by A5, A11, TARSKI:def 1;

            hence thesis by POLYNOM1:def 4;

          end;

          then ( Support m) = {b} by A6, TARSKI: 2;

          then

           A12: ( rng sg) = {b} by A10, PRE_POLY:def 2;

          then

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

          then

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

          then

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

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

          then 1 in ( dom (m * sg)) by A14, A9, FUNCT_1: 11;

          

          then

           A16: ((m * sg) /. 1) = ((m * sg) . 1) by PARTFUN1:def 6

          .= (m . (sg . 1)) by A14, FUNCT_1: 13

          .= (m . b) by A12, A15, TARSKI:def 1

          .= ( coefficient m) by A5, Def5;

          

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

          proof

            let u be object;

            assume

             A18: u in ( dom sg);

            assume

             A19: not u in {1};

            reconsider u as Element of NAT by A18;

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

            then

             A20: (sg /. u) in ( rng sg) by A18, FUNCT_1: 3;

            

             A21: u <> 1 by A19, TARSKI:def 1;

            

             A22: 1 < u

            proof

              consider k be Nat such that

               A23: ( 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 A18, A23;

              hence thesis by A21, XXREAL_0: 1;

            end;

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

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

            

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

            .= (sg /. u) by A12, A20, TARSKI:def 1;

            hence thesis by A10, A14, A18, A22, PRE_POLY:def 2;

          end;

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

          then

           A24: ( dom sg) = ( Seg 1) by A17, FINSEQ_1: 2, TARSKI: 2;

          then

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

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

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

          then

           A26: (sg /. 1) = b by A12, TARSKI:def 1;

          

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

          ( dom y) = ( Seg ( len y)) by FINSEQ_1:def 3

          .= ( dom sg) by A1, FINSEQ_1:def 3;

          

          then (y . 1) = (y /. 1) by A25, PARTFUN1:def 6

          .= (((m * sg) /. 1) * ( eval (b,x))) by A26, A1, A3, A27;

          then y = <*(( coefficient m) * ( eval (b,x)))*> by A1, A27, A16, FINSEQ_1: 40;

          

          hence ( eval (m,x)) = (( coefficient m) * ( eval (b,x))) by A2, RLVECT_1: 44

          .= (( coefficient m) * ( eval (( term m),x))) by A5, Def5;

        end;

          case

           A28: (m . b) = ( 0. L);

          

           A29: ( Support m) = {}

          proof

            assume ( Support m) <> {} ;

            then

            reconsider sm = ( Support m) as non empty Subset of ( Bags n);

            set c = the Element of sm;

            (m . c) <> ( 0. L) by POLYNOM1:def 4;

            hence thesis by A4, A28;

          end;

          then ( term m) = ( EmptyBag n) & (m . ( EmptyBag n)) = ( 0. L) by Def5, POLYNOM1:def 4;

          then

           A30: (( coefficient m) * ( eval (( term m),x))) = ( 0. L);

          consider y be FinSequence of the carrier of L such that

           A31: ( len y) = ( len ( SgmX (( BagOrder n),( Support m)))) and

           A32: ( eval (m,x)) = ( Sum y) and for i be Element of NAT st 1 <= i & i <= ( len y) holds (y /. i) = (((m * ( SgmX (( BagOrder n),( Support m)))) /. i) * ( eval ((( SgmX (( BagOrder n),( Support m))) /. i),x))) by POLYNOM2:def 4;

          ( BagOrder n) linearly_orders ( Support m) by POLYNOM2: 18;

          then ( rng ( SgmX (( BagOrder n),( Support m)))) = {} by A29, PRE_POLY:def 2;

          then ( SgmX (( BagOrder n),( Support m))) = {} by RELAT_1: 41;

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

          hence thesis by A30, A32, RLVECT_1: 43;

        end;

      end;

      hence thesis;

    end;

    theorem :: POLYNOM7:13

    for n be Ordinal, L be right_zeroed add-associative right_complementable well-unital distributive non trivial doubleLoopStr, a be Element of L, b be bag of n, x be Function of n, L holds ( eval (( Monom (a,b)),x)) = (a * ( eval (b,x)))

    proof

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

      set m = ( Monom (a,b));

      now

        per cases ;

          case a <> ( 0. L);

          then

           A1: a is non zero;

          

          thus ( eval (m,x)) = (( coefficient m) * ( eval (( term m),x))) by Th12

          .= (a * ( eval (( term m),x))) by Th9

          .= (a * ( eval (b,x))) by A1, Th10;

        end;

          case

           A2: a = ( 0. L);

          for b9 be bag of n holds (m . b9) = ( 0. L)

          proof

            let b9 be bag of n;

            now

              per cases ;

                case

                 A3: b9 = b;

                

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

                

                 A5: b in ( dom (b .--> a)) by TARSKI:def 1;

                ( dom ( 0_ (n,L))) = ( dom (( Bags n) --> ( 0. L))) by POLYNOM1:def 8

                .= ( Bags n);

                then m = (( 0_ (n,L)) +* (b .--> a)) by A4, FUNCT_7:def 3;

                

                hence (m . b9) = ((b .--> a) . b) by A3, A5, FUNCT_4: 13

                .= ( 0. L) by A2, FUNCOP_1: 72;

              end;

                case b9 <> b;

                

                hence (m . b9) = (( 0_ (n,L)) . b9) by FUNCT_7: 32

                .= ( 0. L) by POLYNOM1: 22;

              end;

            end;

            hence thesis;

          end;

          then

           A6: (m . ( term m)) = ( 0. L);

          

          thus ( eval (m,x)) = (( coefficient m) * ( eval (( term m),x))) by Th12

          .= ( 0. L) by A6

          .= (a * ( eval (b,x))) by A2;

        end;

      end;

      hence thesis;

    end;

    begin

    definition

      let X be set, L be non empty ZeroStr, p be Series of X, L;

      :: POLYNOM7:def7

      attr p is Constant means

      : Def7: for b be bag of X st b <> ( EmptyBag X) holds (p . b) = ( 0. L);

    end

    registration

      let X be set, L be non empty ZeroStr;

      cluster Constant for Series of X, L;

      existence

      proof

        set c = ( 0_ (X,L));

        take c;

        for b be bag of X st b <> ( EmptyBag X) holds (c . b) = ( 0. L) by POLYNOM1: 22;

        hence thesis;

      end;

    end

    definition

      let X be set, L be non empty ZeroStr;

      mode ConstPoly of X,L is Constant Series of X, L;

    end

    registration

      let X be set, L be non empty ZeroStr;

      cluster Constant -> monomial-like for Series of X, L;

      coherence ;

    end

    theorem :: POLYNOM7:14

    

     Th14: for X be set, L be non empty ZeroStr, p be Series of X, L holds p is ConstPoly of X, L iff (p = ( 0_ (X,L)) or ( Support p) = {( EmptyBag X)})

    proof

      let n be set, L be non empty ZeroStr, p be Series of n, L;

       A1:

      now

        assume

         A2: p is ConstPoly of n, L;

        

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

        proof

          let u be object;

          assume

           A4: u in ( Support p);

          then

          reconsider u as Element of ( Bags n);

          reconsider u9 = u as bag of n;

          (p . u9) <> ( 0. L) by A4, POLYNOM1:def 4;

          then u9 = ( EmptyBag n) by A2, Def7;

          hence thesis by TARSKI:def 1;

        end;

        thus ( Support p) = {( EmptyBag n)} or p = ( 0_ (n,L))

        proof

          assume

           A5: not ( Support p) = {( EmptyBag n)};

          

           A6: not ( EmptyBag n) in ( Support p)

          proof

            assume ( EmptyBag n) in ( Support p);

            then for u be object holds u in {( EmptyBag n)} implies u in ( Support p) by TARSKI:def 1;

            hence thesis by A3, A5, TARSKI: 2;

          end;

          

           A7: ( Support p) = {}

          proof

            set v = the Element of ( Support p);

            assume ( Support p) <> {} ;

            then v in ( Support p) & v in {( EmptyBag n)} by A3;

            hence thesis by A6, TARSKI:def 1;

          end;

          

           A8: for b be bag of n holds (p . b) = ( 0. L)

          proof

            let b be bag of n;

            

             A9: b is Element of ( Bags n) by PRE_POLY:def 12;

            assume (p . b) <> ( 0. L);

            hence thesis by A7, A9, POLYNOM1:def 4;

          end;

          

           A10: for u be object holds u in ( rng p) implies u in {( 0. L)}

          proof

            let u be object;

            assume u in ( rng p);

            then

            consider x be object such that

             A11: x in ( dom p) and

             A12: (p . x) = u by FUNCT_1:def 3;

            x is bag of n by A11;

            then u = ( 0. L) by A8, A12;

            hence thesis by TARSKI:def 1;

          end;

          

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

          for u be object holds u in {( 0. L)} implies u in ( rng p)

          proof

            set b = the bag of n;

            let u be object;

            assume u in {( 0. L)};

            then u = ( 0. L) by TARSKI:def 1;

            then

             A14: (p . b) = u by A8;

            b in ( dom p) by A13, PRE_POLY:def 12;

            hence thesis by A14, FUNCT_1:def 3;

          end;

          then ( rng p) = {( 0. L)} by A10, TARSKI: 2;

          then p = (( Bags n) --> ( 0. L)) by A13, FUNCOP_1: 9;

          hence thesis by POLYNOM1:def 8;

        end;

      end;

      now

        assume

         A15: p = ( 0_ (n,L)) or ( Support p) = {( EmptyBag n)};

        per cases by A15;

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

          then for b be bag of n st b <> ( EmptyBag n) holds (p . b) = ( 0. L) by POLYNOM1: 22;

          hence p is ConstPoly of n, L by Def7;

        end;

          suppose

           A16: ( Support p) = {( EmptyBag n)};

          for b be bag of n st b <> ( EmptyBag n) holds (p . b) = ( 0. L)

          proof

            let b be bag of n;

            assume

             A17: b <> ( EmptyBag n);

            reconsider b as Element of ( Bags n) by PRE_POLY:def 12;

             not b in ( Support p) by A16, A17, TARSKI:def 1;

            hence thesis by POLYNOM1:def 4;

          end;

          hence p is ConstPoly of n, L by Def7;

        end;

      end;

      hence thesis by A1;

    end;

    registration

      let X be set, L be non empty ZeroStr;

      cluster ( 0_ (X,L)) -> Constant;

      coherence by POLYNOM1: 22;

    end

    registration

      let X be set, L be well-unital non empty doubleLoopStr;

      cluster ( 1_ (X,L)) -> Constant;

      coherence by POLYNOM1: 25;

    end

    

     Lm2: for X be set, L be non empty ZeroStr, c be ConstPoly of X, L holds ( term c) = ( EmptyBag X) & ( coefficient c) = (c . ( EmptyBag X))

    proof

      let n be set, L be non empty ZeroStr, c be ConstPoly of n, L;

      set eb = ( EmptyBag n);

       A1:

      now

        per cases ;

          case (c . eb) <> ( 0. L);

          hence ( term c) = ( EmptyBag n) by Def5;

        end;

          case

           A2: (c . eb) = ( 0. L);

          ( Support c) = {}

          proof

            set u = the Element of ( Support c);

            assume

             A3: ( Support c) <> {} ;

            then u in ( Support c);

            then

            reconsider u as Element of ( Bags n);

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

            hence thesis by A2, Def7;

          end;

          hence ( term c) = ( EmptyBag n) by Def5;

        end;

      end;

      hence ( term c) = ( EmptyBag n);

      thus thesis by A1;

    end;

    theorem :: POLYNOM7:15

    

     Th15: for X be set, L be non empty ZeroStr, c be ConstPoly of X, L holds ( Support c) = {} or ( Support c) = {( EmptyBag X)}

    proof

      let X be set, L be non empty ZeroStr, c be ConstPoly of X, L;

      assume ( Support c) <> {} ;

      

      hence ( Support c) = {( term c)} by Th7

      .= {( EmptyBag X)} by Lm2;

    end;

    theorem :: POLYNOM7:16

    for X be set, L be non empty ZeroStr, c be ConstPoly of X, L holds ( term c) = ( EmptyBag X) & ( coefficient c) = (c . ( EmptyBag X)) by Lm2;

    definition

      let X be set, L be non empty ZeroStr, a be Element of L;

      :: POLYNOM7:def8

      func a | (X,L) -> Series of X, L equals (( 0_ (X,L)) +* (( EmptyBag X),a));

      coherence ;

    end

    registration

      let X be set, L be non empty ZeroStr, a be Element of L;

      cluster (a | (X,L)) -> Constant;

      coherence

      proof

        set Z = ( 0_ (X,L));

        set O = (Z +* (( EmptyBag X),a));

        reconsider O as Function of ( Bags X), the carrier of L;

        reconsider O9 = O as Function of ( Bags X), L;

        reconsider O9 as Series of X, L;

        now

          let b be bag of X;

          ( dom Z) = ( dom (( Bags X) --> ( 0. L))) by POLYNOM1:def 8

          .= ( Bags X);

          then

           A1: O9 = (( 0_ (X,L)) +* (( EmptyBag X) .--> a)) by FUNCT_7:def 3;

          assume b <> ( EmptyBag X);

          then not b in ( dom (( EmptyBag X) .--> a)) by TARSKI:def 1;

          

          hence (O9 . b) = (( 0_ (X,L)) . b) by A1, FUNCT_4: 11

          .= ( 0. L) by POLYNOM1: 22;

        end;

        hence thesis;

      end;

    end

    

     Lm3: for X be set, L be non empty ZeroStr holds (( 0. L) | (X,L)) = ( 0_ (X,L))

    proof

      let X be set, L be non empty ZeroStr;

      set o1 = (( 0. L) | (X,L)), o2 = ( 0_ (X,L));

      now

        set m = (( 0_ (X,L)) +* (( EmptyBag X),( 0. L)));

        let x be object;

        reconsider m as Function of ( Bags X), the carrier of L;

        reconsider m as Function of ( Bags X), L;

        reconsider m as Series of X, L;

        assume x in ( Bags X);

        then

        reconsider x9 = x as bag of X;

        

         A1: ( dom ( 0_ (X,L))) = ( dom (( Bags X) --> ( 0. L))) by POLYNOM1:def 8

        .= ( Bags X);

        then

         A2: m = (( 0_ (X,L)) +* (( EmptyBag X) .--> ( 0. L))) by FUNCT_7:def 3;

        

         A3: ( EmptyBag X) in ( dom (( EmptyBag X) .--> ( 0. L))) by TARSKI:def 1;

        

         A4: (m . ( EmptyBag X)) = ((( 0_ (X,L)) +* (( EmptyBag X) .--> ( 0. L))) . ( EmptyBag X)) by A1, FUNCT_7:def 3

        .= ((( EmptyBag X) .--> ( 0. L)) . ( EmptyBag X)) by A3, FUNCT_4: 13

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

        per cases ;

          suppose x9 = ( EmptyBag X);

          hence (o1 . x) = (o2 . x) by A4, POLYNOM1: 22;

        end;

          suppose x9 <> ( EmptyBag X);

          then not x9 in ( dom (( EmptyBag X) .--> ( 0. L))) by TARSKI:def 1;

          hence (o1 . x) = (o2 . x) by A2, FUNCT_4: 11;

        end;

      end;

      hence thesis;

    end;

    theorem :: POLYNOM7:17

    for X be set, L be non empty ZeroStr, p be Series of X, L holds p is ConstPoly of X, L iff ex a be Element of L st p = (a | (X,L))

    proof

      let X be set, L be non empty ZeroStr, p be Series of X, L;

      now

        assume

         A1: p is ConstPoly of X, L;

        now

          per cases by A1, Th14;

            case p = ( 0_ (X,L));

            then p = (( 0. L) | (X,L)) by Lm3;

            hence ex a be Element of L st p = (a | (X,L));

          end;

            case

             A2: ( Support p) = {( EmptyBag X)};

            set q = (( 0_ (X,L)) +* (( EmptyBag X),(p . ( EmptyBag X))));

             A3:

            now

              let x be object;

              assume x in ( Bags X);

              then

              reconsider x9 = x as bag of X;

              

               A4: ( dom ( 0_ (X,L))) = ( dom (( Bags X) --> ( 0. L))) by POLYNOM1:def 8

              .= ( Bags X);

              then

               A5: q = (( 0_ (X,L)) +* (( EmptyBag X) .--> (p . ( EmptyBag X)))) by FUNCT_7:def 3;

              

               A6: ( EmptyBag X) in ( dom (( EmptyBag X) .--> (p . ( EmptyBag X)))) by TARSKI:def 1;

              

               A7: (q . ( EmptyBag X)) = ((( 0_ (X,L)) +* (( EmptyBag X) .--> (p . ( EmptyBag X)))) . ( EmptyBag X)) by A4, FUNCT_7:def 3

              .= ((( EmptyBag X) .--> (p . ( EmptyBag X))) . ( EmptyBag X)) by A6, FUNCT_4: 13

              .= (p . ( EmptyBag X)) by FUNCOP_1: 72;

              now

                per cases ;

                  case x9 = ( EmptyBag X);

                  hence (p . x) = (q . x) by A7;

                end;

                  case

                   A8: x9 <> ( EmptyBag X);

                  

                   A9: x9 is Element of ( Bags X) by PRE_POLY:def 12;

                   not x9 in ( Support p) by A2, A8, TARSKI:def 1;

                  then

                   A10: (p . x9) = ( 0. L) by A9, POLYNOM1:def 4;

                   not x9 in ( dom (( EmptyBag X) .--> (p . ( EmptyBag X)))) by A8, TARSKI:def 1;

                  then (q . x9) = (( 0_ (X,L)) . x9) by A5, FUNCT_4: 11;

                  hence (p . x) = (q . x) by A10, POLYNOM1: 22;

                end;

              end;

              hence (p . x) = (q . x);

            end;

            

             A11: ( Bags X) = ( dom q) by FUNCT_2:def 1;

            q = ((p . ( EmptyBag X)) | (X,L)) & ( Bags X) = ( dom p) by FUNCT_2:def 1;

            hence ex a be Element of L st p = (a | (X,L)) by A11, A3, FUNCT_1: 2;

          end;

        end;

        hence ex a be Element of L st p = (a | (X,L));

      end;

      hence thesis;

    end;

    theorem :: POLYNOM7:18

    

     Th18: for X be set, L be non empty multLoopStr_0, a be Element of L holds ((a | (X,L)) . ( EmptyBag X)) = a & for b be bag of X st b <> ( EmptyBag X) holds ((a | (X,L)) . b) = ( 0. L)

    proof

      let n be set, L be non empty multLoopStr_0, a be Element of L;

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

      

       A1: Z = (( Bags n) --> ( 0. L)) by POLYNOM1:def 8;

      then ( dom Z) = ( Bags n);

      hence ((a | (n,L)) . ( EmptyBag n)) = a by FUNCT_7: 31;

      let b be bag of n;

      

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

      assume b <> ( EmptyBag n);

      

      hence ((a | (n,L)) . b) = (Z . b) by FUNCT_7: 32

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

    end;

    theorem :: POLYNOM7:19

    for X be set, L be non empty ZeroStr holds (( 0. L) | (X,L)) = ( 0_ (X,L)) by Lm3;

    theorem :: POLYNOM7:20

    for X be set, L be well-unital non empty multLoopStr_0 holds (( 1. L) | (X,L)) = ( 1_ (X,L))

    proof

      let X be set, L be well-unital non empty multLoopStr_0;

      set o1 = (( 1. L) | (X,L)), o2 = ( 1_ (X,L));

      now

        set m = (( 0_ (X,L)) +* (( EmptyBag X),( 1. L)));

        let x be object;

        reconsider m as Function of ( Bags X), the carrier of L;

        reconsider m as Function of ( Bags X), L;

        reconsider m as Series of X, L;

        assume x in ( Bags X);

        then

        reconsider x9 = x as bag of X;

        

         A1: ( dom ( 0_ (X,L))) = ( dom (( Bags X) --> ( 0. L))) by POLYNOM1:def 8

        .= ( Bags X);

        then

         A2: m = (( 0_ (X,L)) +* (( EmptyBag X) .--> ( 1. L))) by FUNCT_7:def 3;

        

         A3: ( EmptyBag X) in ( dom (( EmptyBag X) .--> ( 1. L))) by TARSKI:def 1;

        

         A4: (m . ( EmptyBag X)) = ((( 0_ (X,L)) +* (( EmptyBag X) .--> ( 1. L))) . ( EmptyBag X)) by A1, FUNCT_7:def 3

        .= ((( EmptyBag X) .--> ( 1. L)) . ( EmptyBag X)) by A3, FUNCT_4: 13

        .= ( 1. L) by FUNCOP_1: 72;

        per cases ;

          suppose x9 = ( EmptyBag X);

          hence (o1 . x) = (o2 . x) by A4, POLYNOM1: 25;

        end;

          suppose

           A5: x9 <> ( EmptyBag X);

          then not x9 in ( dom (( EmptyBag X) .--> ( 1. L))) by TARSKI:def 1;

          

          then (m . x9) = (( 0_ (X,L)) . x9) by A2, FUNCT_4: 11

          .= ( 0. L) by POLYNOM1: 22

          .= (o2 . x9) by A5, POLYNOM1: 25;

          hence (o1 . x) = (o2 . x);

        end;

      end;

      hence thesis;

    end;

    theorem :: POLYNOM7:21

    for X be set, L be non empty ZeroStr, a,b be Element of L holds (a | (X,L)) = (b | (X,L)) iff a = b

    proof

      let X be set, L be non empty ZeroStr, a,b be Element of L;

      set m = (( 0_ (X,L)) +* (( EmptyBag X),a));

      reconsider m as Function of ( Bags X), the carrier of L;

      reconsider m as Function of ( Bags X), L;

      reconsider m as Series of X, L;

      set k = (( 0_ (X,L)) +* (( EmptyBag X),b));

      reconsider k as Function of ( Bags X), the carrier of L;

      reconsider k as Function of ( Bags X), L;

      reconsider k as Series of X, L;

      

       A1: ( EmptyBag X) in ( dom (( EmptyBag X) .--> a)) by TARSKI:def 1;

      

       A2: ( EmptyBag X) in ( dom (( EmptyBag X) .--> b)) by TARSKI:def 1;

      ( dom ( 0_ (X,L))) = ( dom (( Bags X) --> ( 0. L))) by POLYNOM1:def 8

      .= ( Bags X);

      

      then

       A3: (k . ( EmptyBag X)) = ((( 0_ (X,L)) +* (( EmptyBag X) .--> b)) . ( EmptyBag X)) by FUNCT_7:def 3

      .= ((( EmptyBag X) .--> b) . ( EmptyBag X)) by A2, FUNCT_4: 13

      .= b by FUNCOP_1: 72;

      ( dom ( 0_ (X,L))) = ( dom (( Bags X) --> ( 0. L))) by POLYNOM1:def 8

      .= ( Bags X);

      

      then (m . ( EmptyBag X)) = ((( 0_ (X,L)) +* (( EmptyBag X) .--> a)) . ( EmptyBag X)) by FUNCT_7:def 3

      .= ((( EmptyBag X) .--> a) . ( EmptyBag X)) by A1, FUNCT_4: 13

      .= a by FUNCOP_1: 72;

      hence thesis by A3;

    end;

    theorem :: POLYNOM7:22

    for X be set, L be non empty ZeroStr, a be Element of L holds ( Support (a | (X,L))) = {} or ( Support (a | (X,L))) = {( EmptyBag X)} by Th15;

    theorem :: POLYNOM7:23

    

     Th23: for X be set, L be non empty ZeroStr, a be Element of L holds ( term (a | (X,L))) = ( EmptyBag X) & ( coefficient (a | (X,L))) = a

    proof

      let X be set, L be non empty ZeroStr, a be Element of L;

      set m = (( 0_ (X,L)) +* (( EmptyBag X),a));

      reconsider m as Function of ( Bags X), the carrier of L;

      reconsider m as Function of ( Bags X), L;

      reconsider m as Series of X, L;

      

       A1: ( EmptyBag X) in ( dom (( EmptyBag X) .--> a)) by TARSKI:def 1;

      ( dom ( 0_ (X,L))) = ( dom (( Bags X) --> ( 0. L))) by POLYNOM1:def 8

      .= ( Bags X);

      

      then (m . ( EmptyBag X)) = ((( 0_ (X,L)) +* (( EmptyBag X) .--> a)) . ( EmptyBag X)) by FUNCT_7:def 3

      .= ((( EmptyBag X) .--> a) . ( EmptyBag X)) by A1, FUNCT_4: 13

      .= a by FUNCOP_1: 72;

      hence thesis by Lm2;

    end;

    theorem :: POLYNOM7:24

    

     Th24: for n be Ordinal, L be right_zeroed add-associative right_complementable well-unital distributive non trivial doubleLoopStr, c be ConstPoly of n, L, x be Function of n, L holds ( eval (c,x)) = ( coefficient c)

    proof

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

      consider y be FinSequence of the carrier of L such that

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

       A2: ( eval (c,x)) = ( Sum y) and

       A3: for i be Element of NAT st 1 <= i & i <= ( len y) holds (y /. i) = (((c * ( SgmX (( BagOrder n),( Support c)))) /. i) * ( eval ((( SgmX (( BagOrder n),( Support c))) /. i),x))) by POLYNOM2:def 4;

      now

        per cases ;

          case

           A4: ( coefficient c) = ( 0. L);

          ( Support c) = {}

          proof

            set u = the Element of ( Support c);

            assume

             A5: ( Support c) <> {} ;

            then u in ( Support c);

            then

            reconsider u as Element of ( Bags n);

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

            then u <> ( EmptyBag n) by A4, Lm2;

            then (c . u) = ( 0. L) by Def7;

            hence thesis by A5, POLYNOM1:def 4;

          end;

          then

          reconsider Sc = ( Support c) as empty Subset of ( Bags n);

          ( SgmX (( BagOrder n),Sc)) = {} by POLYNOM2: 18, PRE_POLY: 76;

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

          hence thesis by A2, A4, RLVECT_1: 43;

        end;

          case

           A6: ( coefficient c) <> ( 0. L);

          reconsider sc = ( Support c) as finite Subset of ( Bags n);

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

          

           A7: ( BagOrder n) linearly_orders sc by POLYNOM2: 18;

          

           A8: for u be object holds u in ( Support c) implies u in {( EmptyBag n)}

          proof

            let u be object;

            assume

             A9: u in ( Support c);

            assume

             A10: not u in {( EmptyBag n)};

            reconsider u as Element of ( Bags n) by A9;

            u <> ( EmptyBag n) by A10, TARSKI:def 1;

            then (c . u) = ( 0. L) by Def7;

            hence thesis by A9, POLYNOM1:def 4;

          end;

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

          proof

            let u be object;

            assume

             A11: u in {( EmptyBag n)};

            then

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

            reconsider u as Element of ( Bags n) by A11;

            (c . u) <> ( 0. L) by A6, A12, Lm2;

            hence thesis by POLYNOM1:def 4;

          end;

          then ( Support c) = {( EmptyBag n)} by A8, TARSKI: 2;

          then

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

          then

           A14: ( EmptyBag n) in ( rng sg) by TARSKI:def 1;

          then

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

          then

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

          

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

          proof

            let u be object;

            assume

             A18: u in ( dom sg);

            assume

             A19: not u in {1};

            reconsider u as Element of NAT by A18;

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

            then

             A20: (sg /. u) in ( rng sg) by A18, FUNCT_1: 3;

            

             A21: u <> 1 by A19, TARSKI:def 1;

            

             A22: 1 < u

            proof

              consider k be Nat such that

               A23: ( dom sg) = ( 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 A18, A23;

              hence thesis by A21, XXREAL_0: 1;

            end;

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

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

            

            then (sg /. 1) = ( EmptyBag n) by A13, TARSKI:def 1

            .= (sg /. u) by A13, A20, TARSKI:def 1;

            hence thesis by A7, A15, A18, A22, PRE_POLY:def 2;

          end;

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

          then

           A24: ( dom sg) = ( Seg 1) by A17, FINSEQ_1: 2, TARSKI: 2;

          then

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

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

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

          then

           A26: (sg /. 1) = ( EmptyBag n) by A13, TARSKI:def 1;

          

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

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

          then 1 in ( dom (c * sg)) by A13, A15, A16, FUNCT_1: 11;

          

          then

           A28: ((c * sg) /. 1) = ((c * sg) . 1) by PARTFUN1:def 6

          .= (c . (sg . 1)) by A15, FUNCT_1: 13

          .= (c . ( EmptyBag n)) by A13, A16, TARSKI:def 1

          .= ( coefficient c) by Lm2;

          ( dom y) = ( Seg ( len y)) by FINSEQ_1:def 3

          .= ( dom sg) by A1, FINSEQ_1:def 3;

          

          then (y . 1) = (y /. 1) by A25, PARTFUN1:def 6

          .= (( coefficient c) * ( eval (( EmptyBag n),x))) by A1, A3, A27, A26, A28

          .= (( coefficient c) * ( 1. L)) by POLYNOM2: 14

          .= ( coefficient c);

          then y = <*( coefficient c)*> by A1, A27, FINSEQ_1: 40;

          hence thesis by A2, RLVECT_1: 44;

        end;

      end;

      hence thesis;

    end;

    theorem :: POLYNOM7:25

    

     Th25: for n be Ordinal, L be right_zeroed add-associative right_complementable well-unital distributive non trivial doubleLoopStr, a be Element of L, x be Function of n, L holds ( eval ((a | (n,L)),x)) = a

    proof

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

      

      thus ( eval ((a | (n,L)),x)) = ( coefficient (a | (n,L))) by Th24

      .= a by Th23;

    end;

    begin

    definition

      let X be set, L be non empty multLoopStr_0, p be Series of X, L, a be Element of L;

      :: POLYNOM7:def9

      func a * p -> Series of X, L means

      : Def9: for b be bag of X holds (it . b) = (a * (p . b));

      existence

      proof

        deffunc F( Element of ( Bags X)) = (a * (p . $1));

        consider f be Function of ( Bags X), the carrier of L such that

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

        reconsider f as Function of ( Bags X), L;

        reconsider f as Series of X, L;

        reconsider f as Series of X, L;

        take f;

        let x be bag of X;

        x in ( Bags X) by PRE_POLY:def 12;

        hence thesis by A1;

      end;

      uniqueness

      proof

        let p1,p2 be Series of X, L such that

         A2: for b be bag of X holds (p1 . b) = (a * (p . b)) and

         A3: for b be bag of X holds (p2 . b) = (a * (p . b));

        now

          let b be Element of ( Bags X);

          reconsider b9 = b as bag of X;

          

          thus (p1 . b) = (a * (p . b9)) by A2

          .= (p2 . b) by A3;

        end;

        hence p1 = p2;

      end;

      :: POLYNOM7:def10

      func p * a -> Series of X, L means

      : Def10: for b be bag of X holds (it . b) = ((p . b) * a);

      existence

      proof

        deffunc F( Element of ( Bags X)) = ((p . $1) * a);

        consider f be Function of ( Bags X), the carrier of L such that

         A4: for x be Element of ( Bags X) holds (f . x) = F(x) from FUNCT_2:sch 4;

        reconsider f as Function of ( Bags X), L;

        reconsider f as Series of X, L;

        reconsider f as Series of X, L;

        take f;

        let x be bag of X;

        x in ( Bags X) by PRE_POLY:def 12;

        hence thesis by A4;

      end;

      uniqueness

      proof

        let p1,p2 be Series of X, L such that

         A5: for b be bag of X holds (p1 . b) = ((p . b) * a) and

         A6: for b be bag of X holds (p2 . b) = ((p . b) * a);

        now

          let b be Element of ( Bags X);

          reconsider b9 = b as bag of X;

          

          thus (p1 . b) = ((p . b9) * a) by A5

          .= (p2 . b) by A6;

        end;

        hence p1 = p2;

      end;

    end

    registration

      let X be set, L be left_zeroed right_zeroed add-cancelable distributive non empty doubleLoopStr, p be finite-Support Series of X, L, a be Element of L;

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

      coherence

      proof

        set ap = (a * p);

        now

          let u be object;

          assume

           A1: u in ( Support ap);

          then

          reconsider u9 = u as Element of ( Bags X);

          (ap . u) <> ( 0. L) by A1, POLYNOM1:def 4;

          then (a * (p . u9)) <> ( 0. L) by Def9;

          then (p . u9) <> ( 0. L) by BINOM: 2;

          hence u in ( Support p) by POLYNOM1:def 4;

        end;

        then ( Support p) is finite & ( Support ap) c= ( Support p) by POLYNOM1:def 5, TARSKI:def 3;

        hence thesis by POLYNOM1:def 5;

      end;

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

      coherence

      proof

        set ap = (p * a);

        now

          let u be object;

          assume

           A2: u in ( Support ap);

          then

          reconsider u9 = u as Element of ( Bags X);

          (ap . u) <> ( 0. L) by A2, POLYNOM1:def 4;

          then ((p . u9) * a) <> ( 0. L) by Def10;

          then (p . u9) <> ( 0. L) by BINOM: 1;

          hence u in ( Support p) by POLYNOM1:def 4;

        end;

        then ( Support p) is finite & ( Support ap) c= ( Support p) by POLYNOM1:def 5, TARSKI:def 3;

        hence thesis by POLYNOM1:def 5;

      end;

    end

    theorem :: POLYNOM7:26

    for X be set, L be commutative non empty multLoopStr_0, p be Series of X, L, a be Element of L holds (a * p) = (p * a)

    proof

      let n be set, L be commutative non empty multLoopStr_0, p be Series of n, L, a be Element of L;

      now

        let b be Element of ( Bags n);

        reconsider b9 = b as bag of n;

        

        thus ((a * p) . b) = (a * (p . b9)) by Def9

        .= ((p * a) . b) by Def10;

      end;

      hence thesis;

    end;

    theorem :: POLYNOM7:27

    

     Th27: for n be Ordinal, L be add-associative right_complementable right_zeroed left-distributive non empty doubleLoopStr, p be Series of n, L, a be Element of L holds (a * p) = ((a | (n,L)) *' p)

    proof

      let n be Ordinal, L be add-associative right_complementable left-distributive right_zeroed non empty doubleLoopStr, p be Series of n, L, a be Element of L;

      for x be object st x in ( Bags n) holds ((a * p) . x) = (((a | (n,L)) *' p) . x)

      proof

        set O = (a | (n,L)), cL = the carrier of L;

        let x be object;

        assume x in ( Bags n);

        then

        reconsider b = x as bag of n;

        

         A1: for b be Element of ( Bags n) holds (((a | (n,L)) *' p) . b) = (a * (p . b))

        proof

          let b be Element of ( Bags n);

          consider s be FinSequence of cL such that

           A2: ((O *' p) . b) = ( Sum s) and

           A3: ( len s) = ( len ( decomp b)) and

           A4: for k be Element of NAT st k in ( dom s) holds ex b1,b2 be bag of n st (( decomp b) /. k) = <*b1, b2*> & (s /. k) = ((O . b1) * (p . b2)) by POLYNOM1:def 10;

          s is non empty by A3;

          then

          consider s1 be Element of cL, t be FinSequence of cL such that

           A5: s1 = (s . 1) and

           A6: s = ( <*s1*> ^ t) by FINSEQ_3: 102;

          

           A7: ( Sum s) = (( Sum <*s1*>) + ( Sum t)) by A6, RLVECT_1: 41;

           A8:

          now

            per cases ;

              suppose t = ( <*> cL);

              hence ( Sum t) = ( 0. L) by RLVECT_1: 43;

            end;

              suppose

               A9: t <> ( <*> cL);

              now

                let k be Nat;

                

                 A10: ( len s) = (( len t) + ( len <*s1*>)) by A6, FINSEQ_1: 22

                .= (( len t) + 1) by FINSEQ_1: 39;

                assume

                 A11: k in ( dom t);

                

                then

                 A12: (t /. k) = (t . k) by PARTFUN1:def 6

                .= (s . (k + 1)) by A6, A11, FINSEQ_3: 103;

                1 <= k by A11, FINSEQ_3: 25;

                then

                 A13: 1 < (k + 1) by NAT_1: 13;

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

                then

                 A14: (k + 1) <= ( len s) by A10, XREAL_1: 6;

                then

                 A15: (k + 1) in ( dom ( decomp b)) by A3, A13, FINSEQ_3: 25;

                

                 A16: ( dom s) = ( dom ( decomp b)) by A3, FINSEQ_3: 29;

                then

                 A17: (s /. (k + 1)) = (s . (k + 1)) by A15, PARTFUN1:def 6;

                per cases by A14, XXREAL_0: 1;

                  suppose

                   A18: (k + 1) < ( len s);

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

                  consider b1,b2 be bag of n such that

                   A19: (( decomp b) /. (k1 + 1)) = <*b1, b2*> and

                   A20: (s /. (k1 + 1)) = ((O . b1) * (p . b2)) by A4, A16, A15;

                  b1 <> ( EmptyBag n) by A3, A13, A18, A19, PRE_POLY: 72;

                  

                  hence (t /. k) = (( 0. L) * (p . b2)) by A12, A17, A20, Th18

                  .= ( 0. L);

                end;

                  suppose

                   A21: (k + 1) = ( len s);

                   A22:

                  now

                    assume b = ( EmptyBag n);

                    then ( decomp b) = <* <*( EmptyBag n), ( EmptyBag n)*>*> by PRE_POLY: 73;

                    then (( len t) + 1) = ( 0 + 1) by A3, A10, FINSEQ_1: 39;

                    hence contradiction by A9;

                  end;

                  consider b1,b2 be bag of n such that

                   A23: (( decomp b) /. (k + 1)) = <*b1, b2*> and

                   A24: (s /. (k + 1)) = ((O . b1) * (p . b2)) by A4, A16, A15;

                  (( decomp b) /. ( len s)) = <*b, ( EmptyBag n)*> by A3, PRE_POLY: 71;

                  then b2 = ( EmptyBag n) & b1 = b by A21, A23, FINSEQ_1: 77;

                  

                  then (s . (k + 1)) = (( 0. L) * (p . ( EmptyBag n))) by A17, A24, A22, Th18

                  .= ( 0. L);

                  hence (t /. k) = ( 0. L) by A12;

                end;

              end;

              hence ( Sum t) = ( 0. L) by MATRLIN: 11;

            end;

          end;

          

           A25: s is non empty by A3;

          then

          consider b1,b2 be bag of n such that

           A26: (( decomp b) /. 1) = <*b1, b2*> and

           A27: (s /. 1) = ((O . b1) * (p . b2)) by A4, FINSEQ_5: 6;

          1 in ( dom s) by A25, FINSEQ_5: 6;

          then

           A28: (s /. 1) = (s . 1) by PARTFUN1:def 6;

          (( decomp b) /. 1) = <*( EmptyBag n), b*> by PRE_POLY: 71;

          then

           A29: b2 = b & b1 = ( EmptyBag n) by A26, FINSEQ_1: 77;

          ( Sum <*s1*>) = s1 by RLVECT_1: 44

          .= (a * (p . b)) by A5, A27, A29, A28, Th18;

          hence thesis by A2, A7, A8, RLVECT_1: 4;

        end;

        b is Element of ( Bags n) by PRE_POLY:def 12;

        

        then ((O *' p) . b) = (a * (p . b)) by A1

        .= ((a * p) . b) by Def9;

        hence thesis;

      end;

      hence thesis;

    end;

    theorem :: POLYNOM7:28

    

     Th28: for n be Ordinal, L be add-associative right_complementable right_zeroed right-distributive non empty doubleLoopStr, p be Series of n, L, a be Element of L holds (p * a) = (p *' (a | (n,L)))

    proof

      let n be Ordinal, L be add-associative right_complementable right-distributive right_zeroed non empty doubleLoopStr, p be Series of n, L, a be Element of L;

      for x be object st x in ( Bags n) holds ((p * a) . x) = ((p *' (a | (n,L))) . x)

      proof

        set O = (a | (n,L)), cL = the carrier of L;

        let x be object;

        assume x in ( Bags n);

        then

        reconsider b = x as bag of n;

        

         A1: for b be Element of ( Bags n) holds ((p *' (a | (n,L))) . b) = ((p . b) * a)

        proof

          let b be Element of ( Bags n);

          consider s be FinSequence of cL such that

           A2: ((p *' O) . b) = ( Sum s) and

           A3: ( len s) = ( len ( decomp b)) and

           A4: for k be Element of NAT st k in ( dom s) holds ex b1,b2 be bag of n st (( decomp b) /. k) = <*b1, b2*> & (s /. k) = ((p . b1) * (O . b2)) by POLYNOM1:def 10;

          consider t be FinSequence of cL, s1 be Element of cL such that

           A5: s = (t ^ <*s1*>) by A3, FINSEQ_2: 19;

           A6:

          now

            per cases ;

              suppose t = ( <*> cL);

              hence ( Sum t) = ( 0. L) by RLVECT_1: 43;

            end;

              suppose

               A7: t <> ( <*> cL);

              now

                let k be Nat;

                

                 A8: ( len s) = (( len t) + ( len <*s1*>)) by A5, FINSEQ_1: 22

                .= (( len t) + 1) by FINSEQ_1: 39;

                assume

                 A9: k in ( dom t);

                

                then

                 A10: (t /. k) = (t . k) by PARTFUN1:def 6

                .= (s . k) by A5, A9, FINSEQ_1:def 7;

                k <= ( len t) by A9, FINSEQ_3: 25;

                then

                 A11: k < ( len s) by A8, NAT_1: 13;

                

                 A12: 1 <= k by A9, FINSEQ_3: 25;

                then

                 A13: k in ( dom ( decomp b)) by A3, A11, FINSEQ_3: 25;

                

                 A14: ( dom s) = ( dom ( decomp b)) by A3, FINSEQ_3: 29;

                then

                 A15: (s /. k) = (s . k) by A13, PARTFUN1:def 6;

                per cases by A12, XXREAL_0: 1;

                  suppose

                   A16: 1 < k;

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

                  consider b1,b2 be bag of n such that

                   A17: (( decomp b) /. k1) = <*b1, b2*> and

                   A18: (s /. k1) = ((p . b1) * (O . b2)) by A4, A14, A13;

                  b2 <> ( EmptyBag n) by A3, A11, A16, A17, PRE_POLY: 72;

                  

                  hence (t /. k) = ((p . b1) * ( 0. L)) by A10, A15, A18, Th18

                  .= ( 0. L);

                end;

                  suppose

                   A19: k = 1;

                   A20:

                  now

                    assume b = ( EmptyBag n);

                    then ( decomp b) = <* <*( EmptyBag n), ( EmptyBag n)*>*> by PRE_POLY: 73;

                    then (( len t) + 1) = ( 0 + 1) by A3, A8, FINSEQ_1: 39;

                    hence contradiction by A7;

                  end;

                  consider b1,b2 be bag of n such that

                   A21: (( decomp b) /. k) = <*b1, b2*> and

                   A22: (s /. k) = ((p . b1) * (O . b2)) by A4, A14, A13;

                  (( decomp b) /. 1) = <*( EmptyBag n), b*> by PRE_POLY: 71;

                  then b1 = ( EmptyBag n) & b2 = b by A19, A21, FINSEQ_1: 77;

                  

                  then (s . k) = ((p . ( EmptyBag n)) * ( 0. L)) by A15, A22, A20, Th18

                  .= ( 0. L);

                  hence (t /. k) = ( 0. L) by A10;

                end;

              end;

              hence ( Sum t) = ( 0. L) by MATRLIN: 11;

            end;

          end;

          

           A23: (s . ( len s)) = ((t ^ <*s1*>) . (( len t) + 1)) by A5, FINSEQ_2: 16

          .= s1 by FINSEQ_1: 42;

          

           A24: ( Sum s) = (( Sum t) + ( Sum <*s1*>)) by A5, RLVECT_1: 41;

          s is non empty by A3;

          then

           A25: ( len s) in ( dom s) by FINSEQ_5: 6;

          then

          consider b1,b2 be bag of n such that

           A26: (( decomp b) /. ( len s)) = <*b1, b2*> and

           A27: (s /. ( len s)) = ((p . b1) * (O . b2)) by A4;

          

           A28: (s /. ( len s)) = (s . ( len s)) by A25, PARTFUN1:def 6;

          (( decomp b) /. ( len s)) = <*b, ( EmptyBag n)*> by A3, PRE_POLY: 71;

          then

           A29: b1 = b & b2 = ( EmptyBag n) by A26, FINSEQ_1: 77;

          ( Sum <*s1*>) = s1 by RLVECT_1: 44

          .= ((p . b) * a) by A27, A29, A28, A23, Th18;

          hence thesis by A2, A24, A6, RLVECT_1: 4;

        end;

        b is Element of ( Bags n) by PRE_POLY:def 12;

        

        then ((p *' O) . b) = ((p . b) * a) by A1

        .= ((p * a) . b) by Def10;

        hence thesis;

      end;

      hence thesis;

    end;

    

     Lm4: for n be Ordinal, L be Abelian left_zeroed right_zeroed add-associative right_complementable well-unital associative commutative distributive non trivial doubleLoopStr, p be Polynomial of n, L, a be Element of L, x be Function of n, L holds ( eval (((a | (n,L)) *' p),x)) = (a * ( eval (p,x)))

    proof

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

      

      thus ( eval (((a | (n,L)) *' p),x)) = (( eval ((a | (n,L)),x)) * ( eval (p,x))) by POLYNOM2: 25

      .= (a * ( eval (p,x))) by Th25;

    end;

    

     Lm5: for n be Ordinal, L be Abelian left_zeroed right_zeroed add-associative right_complementable well-unital associative commutative distributive non trivial doubleLoopStr, p be Polynomial of n, L, a be Element of L, x be Function of n, L holds ( eval ((p *' (a | (n,L))),x)) = (( eval (p,x)) * a)

    proof

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

      

      thus ( eval ((p *' (a | (n,L))),x)) = (( eval (p,x)) * ( eval ((a | (n,L)),x))) by POLYNOM2: 25

      .= (( eval (p,x)) * a) by Th25;

    end;

    theorem :: POLYNOM7:29

    for n be Ordinal, L be Abelian left_zeroed right_zeroed add-associative right_complementable well-unital associative commutative distributive non trivial doubleLoopStr, p be Polynomial of n, L, a be Element of L, x be Function of n, L holds ( eval ((a * p),x)) = (a * ( eval (p,x)))

    proof

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

      

      thus ( eval ((a * p),x)) = ( eval (((a | (n,L)) *' p),x)) by Th27

      .= (a * ( eval (p,x))) by Lm4;

    end;

    theorem :: POLYNOM7:30

    for n be Ordinal, L be left_zeroed right_zeroed left_add-cancelable add-associative right_complementable well-unital associative domRing-like distributive non trivial doubleLoopStr, p be Polynomial of n, L, a be Element of L, x be Function of n, L holds ( eval ((a * p),x)) = (a * ( eval (p,x)))

    proof

      let n be Ordinal, L be left_zeroed right_zeroed left_add-cancelable add-associative right_complementable well-unital associative domRing-like distributive non trivial doubleLoopStr, p be Polynomial of n, L, a be Element of L, x be Function of n, L;

      consider y be FinSequence of the carrier of L such that

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

       A2: ( eval ((a * p),x)) = ( Sum y) and

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

      

       A4: ( BagOrder n) linearly_orders ( Support (a * p)) by POLYNOM2: 18;

      consider z be FinSequence of the carrier of L such that

       A5: ( len z) = ( len ( SgmX (( BagOrder n),( Support p)))) and

       A6: ( eval (p,x)) = ( Sum z) and

       A7: for i be Element of NAT st 1 <= i & i <= ( len z) holds (z /. i) = (((p * ( SgmX (( BagOrder n),( Support p)))) /. i) * ( eval ((( SgmX (( BagOrder n),( Support p))) /. i),x))) by POLYNOM2:def 4;

      per cases ;

        suppose

         A8: a = ( 0. L);

         A9:

        now

          let b be bag of n;

          

          thus ((a * p) . b) = (a * (p . b)) by Def9

          .= ( 0. L) by A8;

        end;

        now

          assume ( Support (a * p)) <> {} ;

          then

          reconsider sp = ( Support (a * p)) as non empty Subset of ( Bags n);

          set c = the Element of sp;

          ((a * p) . c) <> ( 0. L) by POLYNOM1:def 4;

          hence contradiction by A9;

        end;

        then ( rng ( SgmX (( BagOrder n),( Support (a * p))))) = {} by A4, PRE_POLY:def 2;

        then ( SgmX (( BagOrder n),( Support (a * p)))) = {} by RELAT_1: 41;

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

        

        then ( Sum y) = ( 0. L) by RLVECT_1: 43

        .= (a * ( Sum z)) by A8;

        hence thesis by A2, A6;

      end;

        suppose

         A10: a <> ( 0. L);

        

         A11: for u be object holds u in ( Support (a * p)) implies u in ( Support p)

        proof

          let u be object;

          assume

           A12: u in ( Support (a * p));

          then

          reconsider u9 = u as Element of ( Bags n);

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

          then (a * (p . u9)) <> ( 0. L) by Def9;

          then (p . u9) <> ( 0. L);

          hence thesis by POLYNOM1:def 4;

        end;

        

         A13: for u be object holds u in ( Support p) implies u in ( Support (a * p))

        proof

          let u be object;

          assume

           A14: u in ( Support p);

          then

          reconsider u9 = u as Element of ( Bags n);

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

          then (a * (p . u9)) <> ( 0. L) by A10, VECTSP_2:def 1;

          then ((a * p) . u9) <> ( 0. L) by Def9;

          hence thesis by POLYNOM1:def 4;

        end;

        then

         A15: ( len z) = ( len y) by A1, A5, A11, TARSKI: 2;

        

        then

         A16: ( dom z) = ( Seg ( len y)) by FINSEQ_1:def 3

        .= ( dom y) by FINSEQ_1:def 3;

        

         A17: ( Support (a * p)) = ( Support p) by A13, A11, TARSKI: 2;

        now

          

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

          now

            let u be object;

            assume u in ( rng ( SgmX (( BagOrder n),( Support (a * p)))));

            then u in ( Support (a * p)) by A4, PRE_POLY:def 2;

            hence u in ( dom (a * p)) by A18;

          end;

          then ( rng ( SgmX (( BagOrder n),( Support (a * p))))) c= ( dom (a * p)) by TARSKI:def 3;

          then

          reconsider r = ((a * p) * ( SgmX (( BagOrder n),( Support (a * p))))) as FinSequence by FINSEQ_1: 16;

          for u be object holds u in ( rng r) implies u in the carrier of L

          proof

            let u be object;

            assume u in ( rng r);

            then

             A19: u in ( rng (a * p)) by FUNCT_1: 14;

            ( rng (a * p)) c= the carrier of L by RELAT_1:def 19;

            hence thesis by A19;

          end;

          then

           A20: ( rng r) c= the carrier of L by TARSKI:def 3;

          

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

          now

            let u be object;

            assume u in ( rng ( SgmX (( BagOrder n),( Support (a * p)))));

            then u in ( Support (a * p)) by A4, PRE_POLY:def 2;

            hence u in ( dom p) by A21;

          end;

          then ( rng ( SgmX (( BagOrder n),( Support (a * p))))) c= ( dom p) by TARSKI:def 3;

          then

          reconsider q = (p * ( SgmX (( BagOrder n),( Support (a * p))))) as FinSequence by FINSEQ_1: 16;

          for u be object holds u in ( rng q) implies u in the carrier of L

          proof

            let u be object;

            assume u in ( rng q);

            then

             A22: u in ( rng p) by FUNCT_1: 14;

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

            hence thesis by A22;

          end;

          then

           A23: ( rng q) c= the carrier of L by TARSKI:def 3;

          reconsider r as FinSequence of the carrier of L by A20, FINSEQ_1:def 4;

          reconsider q as FinSequence of the carrier of L by A23, FINSEQ_1:def 4;

          let i be object;

          assume

           A24: i in ( dom z);

          then i in ( Seg ( len z)) by FINSEQ_1:def 3;

          then i in { k where k be Nat : 1 <= k & k <= ( len z) } by FINSEQ_1:def 1;

          then

          consider k be Nat such that

           A25: i = k and

           A26: 1 <= k & k <= ( len z);

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

          

           A27: ( dom z) = ( Seg ( len ( SgmX (( BagOrder n),( Support (a * p)))))) by A1, A16, FINSEQ_1:def 3

          .= ( dom ( SgmX (( BagOrder n),( Support (a * p))))) by FINSEQ_1:def 3;

          then (( SgmX (( BagOrder n),( Support (a * p)))) . k) = (( SgmX (( BagOrder n),( Support (a * p)))) /. k) by A24, A25, PARTFUN1:def 6;

          then k in ( dom q) by A24, A25, A27, A21, FUNCT_1: 11;

          

          then

           A28: ((p * ( SgmX (( BagOrder n),( Support (a * p))))) /. k) = (q . k) by PARTFUN1:def 6

          .= (p . (( SgmX (( BagOrder n),( Support (a * p)))) . k)) by A24, A25, A27, FUNCT_1: 13

          .= (p . (( SgmX (( BagOrder n),( Support (a * p)))) /. k)) by A24, A25, A27, PARTFUN1:def 6;

          reconsider c = (( SgmX (( BagOrder n),( Support (a * p)))) /. k) as Element of ( Bags n);

          reconsider c as bag of n;

          

           A29: (a * (z /. k)) = (a * (((p * ( SgmX (( BagOrder n),( Support p)))) /. k) * ( eval ((( SgmX (( BagOrder n),( Support p))) /. k),x)))) by A7, A26

          .= ((a * ((p * ( SgmX (( BagOrder n),( Support (a * p))))) /. k)) * ( eval ((( SgmX (( BagOrder n),( Support (a * p)))) /. k),x))) by A17, GROUP_1:def 3;

          

           A30: ((a * p) . (( SgmX (( BagOrder n),( Support (a * p)))) /. k)) = (a * ((p * ( SgmX (( BagOrder n),( Support (a * p))))) /. k)) by A28, Def9;

          (( SgmX (( BagOrder n),( Support (a * p)))) . k) = (( SgmX (( BagOrder n),( Support (a * p)))) /. k) by A24, A25, A27, PARTFUN1:def 6;

          then k in ( dom r) by A24, A25, A27, A18, FUNCT_1: 11;

          

          then (((a * p) * ( SgmX (( BagOrder n),( Support (a * p))))) /. k) = (r . k) by PARTFUN1:def 6

          .= ((a * p) . (( SgmX (( BagOrder n),( Support (a * p)))) . k)) by A24, A25, A27, FUNCT_1: 13

          .= (a * ((p * ( SgmX (( BagOrder n),( Support (a * p))))) /. k)) by A24, A25, A27, A30, PARTFUN1:def 6;

          hence (y /. i) = (a * (z /. i)) by A3, A15, A25, A26, A29;

        end;

        then y = (a * z) by A16, POLYNOM1:def 1;

        hence thesis by A2, A6, BINOM: 4;

      end;

    end;

    theorem :: POLYNOM7:31

    for n be Ordinal, L be Abelian left_zeroed right_zeroed add-associative right_complementable well-unital associative commutative distributive non trivial doubleLoopStr, p be Polynomial of n, L, a be Element of L, x be Function of n, L holds ( eval ((p * a),x)) = (( eval (p,x)) * a)

    proof

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

      

      thus ( eval ((p * a),x)) = ( eval ((p *' (a | (n,L))),x)) by Th28

      .= (( eval (p,x)) * a) by Lm5;

    end;

    theorem :: POLYNOM7:32

    for n be Ordinal, L be left_zeroed right_zeroed left_add-cancelable add-associative right_complementable well-unital associative commutative distributive domRing-like non trivial doubleLoopStr, p be Polynomial of n, L, a be Element of L, x be Function of n, L holds ( eval ((p * a),x)) = (( eval (p,x)) * a)

    proof

      let n be Ordinal, L be left_zeroed right_zeroed left_add-cancelable add-associative right_complementable well-unital associative commutative distributive domRing-like non trivial doubleLoopStr, p be Polynomial of n, L, a be Element of L, x be Function of n, L;

      consider y be FinSequence of the carrier of L such that

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

       A2: ( eval ((p * a),x)) = ( Sum y) and

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

      consider z be FinSequence of the carrier of L such that

       A4: ( len z) = ( len ( SgmX (( BagOrder n),( Support p)))) and

       A5: ( eval (p,x)) = ( Sum z) and

       A6: for i be Element of NAT st 1 <= i & i <= ( len z) holds (z /. i) = (((p * ( SgmX (( BagOrder n),( Support p)))) /. i) * ( eval ((( SgmX (( BagOrder n),( Support p))) /. i),x))) by POLYNOM2:def 4;

      now

        per cases ;

          case

           A7: a = ( 0. L);

           A8:

          now

            let b be bag of n;

            

            thus ((p * a) . b) = ((p . b) * a) by Def10

            .= ( 0. L) by A7;

          end;

           A9:

          now

            assume ( Support (p * a)) <> {} ;

            then

            reconsider sp = ( Support (p * a)) as non empty Subset of ( Bags n);

            set c = the Element of sp;

            ((p * a) . c) <> ( 0. L) by POLYNOM1:def 4;

            hence contradiction by A8;

          end;

          ( BagOrder n) linearly_orders ( Support (p * a)) by POLYNOM2: 18;

          then ( rng ( SgmX (( BagOrder n),( Support (p * a))))) = {} by A9, PRE_POLY:def 2;

          then ( SgmX (( BagOrder n),( Support (p * a)))) = {} by RELAT_1: 41;

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

          

          then ( Sum y) = ( 0. L) by RLVECT_1: 43

          .= (( Sum z) * a) by A7;

          hence thesis by A2, A5;

        end;

          case

           A10: a <> ( 0. L);

          

           A11: for u be object holds u in ( Support (p * a)) implies u in ( Support p)

          proof

            let u be object;

            assume

             A12: u in ( Support (p * a));

            then

            reconsider u9 = u as Element of ( Bags n);

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

            then ((p . u9) * a) <> ( 0. L) by Def10;

            then (p . u9) <> ( 0. L);

            hence thesis by POLYNOM1:def 4;

          end;

          

           A13: for u be object holds u in ( Support p) implies u in ( Support (p * a))

          proof

            let u be object;

            assume

             A14: u in ( Support p);

            then

            reconsider u9 = u as Element of ( Bags n);

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

            then ((p . u9) * a) <> ( 0. L) by A10, VECTSP_2:def 1;

            then ((p * a) . u9) <> ( 0. L) by Def10;

            hence thesis by POLYNOM1:def 4;

          end;

          then

           A15: ( len z) = ( len y) by A1, A4, A11, TARSKI: 2;

          

          then

           A16: ( dom z) = ( Seg ( len y)) by FINSEQ_1:def 3

          .= ( dom y) by FINSEQ_1:def 3;

          

           A17: ( BagOrder n) linearly_orders ( Support (p * a)) by POLYNOM2: 18;

          

           A18: ( Support (p * a)) = ( Support p) by A13, A11, TARSKI: 2;

          now

            

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

            now

              let u be object;

              assume u in ( rng ( SgmX (( BagOrder n),( Support (p * a)))));

              then u in ( Support (p * a)) by A17, PRE_POLY:def 2;

              hence u in ( dom (p * a)) by A19;

            end;

            then ( rng ( SgmX (( BagOrder n),( Support (p * a))))) c= ( dom (p * a)) by TARSKI:def 3;

            then

            reconsider r = ((p * a) * ( SgmX (( BagOrder n),( Support (p * a))))) as FinSequence by FINSEQ_1: 16;

            for u be object holds u in ( rng r) implies u in the carrier of L

            proof

              let u be object;

              assume u in ( rng r);

              then

               A20: u in ( rng (p * a)) by FUNCT_1: 14;

              ( rng (p * a)) c= the carrier of L by RELAT_1:def 19;

              hence thesis by A20;

            end;

            then

             A21: ( rng r) c= the carrier of L by TARSKI:def 3;

            

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

            now

              let u be object;

              assume u in ( rng ( SgmX (( BagOrder n),( Support (p * a)))));

              then u in ( Support (p * a)) by A17, PRE_POLY:def 2;

              hence u in ( dom p) by A22;

            end;

            then ( rng ( SgmX (( BagOrder n),( Support (p * a))))) c= ( dom p) by TARSKI:def 3;

            then

            reconsider q = (p * ( SgmX (( BagOrder n),( Support (p * a))))) as FinSequence by FINSEQ_1: 16;

            for u be object holds u in ( rng q) implies u in the carrier of L

            proof

              let u be object;

              assume u in ( rng q);

              then

               A23: u in ( rng p) by FUNCT_1: 14;

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

              hence thesis by A23;

            end;

            then

             A24: ( rng q) c= the carrier of L by TARSKI:def 3;

            reconsider r as FinSequence of the carrier of L by A21, FINSEQ_1:def 4;

            reconsider q as FinSequence of the carrier of L by A24, FINSEQ_1:def 4;

            let i be object;

            assume

             A25: i in ( dom z);

            then i in ( Seg ( len z)) by FINSEQ_1:def 3;

            then i in { k where k be Nat : 1 <= k & k <= ( len z) } by FINSEQ_1:def 1;

            then

            consider k be Nat such that

             A26: i = k and

             A27: 1 <= k & k <= ( len z);

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

            

             A28: ( dom z) = ( Seg ( len ( SgmX (( BagOrder n),( Support (p * a)))))) by A1, A16, FINSEQ_1:def 3

            .= ( dom ( SgmX (( BagOrder n),( Support (p * a))))) by FINSEQ_1:def 3;

            then (( SgmX (( BagOrder n),( Support (p * a)))) . k) = (( SgmX (( BagOrder n),( Support (p * a)))) /. k) by A25, A26, PARTFUN1:def 6;

            then k in ( dom q) by A25, A26, A28, A22, FUNCT_1: 11;

            

            then

             A29: ((p * ( SgmX (( BagOrder n),( Support (p * a))))) /. k) = (q . k) by PARTFUN1:def 6

            .= (p . (( SgmX (( BagOrder n),( Support (p * a)))) . k)) by A25, A26, A28, FUNCT_1: 13

            .= (p . (( SgmX (( BagOrder n),( Support (p * a)))) /. k)) by A25, A26, A28, PARTFUN1:def 6;

            reconsider c = (( SgmX (( BagOrder n),( Support (p * a)))) /. k) as Element of ( Bags n);

            reconsider c as bag of n;

            

             A30: ((z /. k) * a) = ((((p * ( SgmX (( BagOrder n),( Support (p * a))))) /. k) * ( eval ((( SgmX (( BagOrder n),( Support (p * a)))) /. k),x))) * a) by A6, A18, A27

            .= ((((p * ( SgmX (( BagOrder n),( Support (p * a))))) /. k) * a) * ( eval ((( SgmX (( BagOrder n),( Support (p * a)))) /. k),x))) by GROUP_1:def 3;

            

             A31: ((p * a) . (( SgmX (( BagOrder n),( Support (p * a)))) /. k)) = (((p * ( SgmX (( BagOrder n),( Support (p * a))))) /. k) * a) by A29, Def10;

            (( SgmX (( BagOrder n),( Support (p * a)))) . k) = (( SgmX (( BagOrder n),( Support (p * a)))) /. k) by A25, A26, A28, PARTFUN1:def 6;

            then k in ( dom r) by A25, A26, A28, A19, FUNCT_1: 11;

            

            then (((p * a) * ( SgmX (( BagOrder n),( Support (p * a))))) /. k) = (r . k) by PARTFUN1:def 6

            .= ((p * a) . (( SgmX (( BagOrder n),( Support (p * a)))) . k)) by A25, A26, A28, FUNCT_1: 13

            .= (((p * ( SgmX (( BagOrder n),( Support (p * a))))) /. k) * a) by A25, A26, A28, A31, PARTFUN1:def 6;

            hence (y /. i) = ((z /. i) * a) by A3, A15, A26, A27, A30;

          end;

          then y = (z * a) by A16, POLYNOM1:def 2;

          hence thesis by A2, A5, BINOM: 5;

        end;

      end;

      hence thesis;

    end;

    theorem :: POLYNOM7:33

    for n be Ordinal, L be Abelian left_zeroed right_zeroed add-associative right_complementable well-unital associative commutative distributive non trivial doubleLoopStr, p be Polynomial of n, L, a be Element of L, x be Function of n, L holds ( eval (((a | (n,L)) *' p),x)) = (a * ( eval (p,x))) by Lm4;

    theorem :: POLYNOM7:34

    for n be Ordinal, L be Abelian left_zeroed right_zeroed add-associative right_complementable well-unital associative commutative distributive non trivial doubleLoopStr, p be Polynomial of n, L, a be Element of L, x be Function of n, L holds ( eval ((p *' (a | (n,L))),x)) = (( eval (p,x)) * a)

    proof

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

      

      thus ( eval ((p *' (a | (n,L))),x)) = (( eval (p,x)) * ( eval ((a | (n,L)),x))) by POLYNOM2: 25

      .= (( eval (p,x)) * a) by Th25;

    end;