polynom1.miz



    begin

    registration

      cluster degenerated -> trivial for add-associative right_zeroed right_complementable right_unital right-distributive non empty doubleLoopStr;

      coherence

      proof

        let L be add-associative right_zeroed right_complementable right_unital right-distributive non empty doubleLoopStr such that

         A1: ( 0. L) = ( 1. L);

        let u be Element of L;

        

        thus u = (u * ( 1. L))

        .= ( 0. L) by A1;

      end;

    end

    registration

      cluster non trivial -> non degenerated for add-associative right_zeroed right_complementable right_unital right-distributive non empty doubleLoopStr;

      coherence ;

    end

    theorem :: POLYNOM1:1

    

     Th1: for K be non empty addLoopStr, p1,p2 be FinSequence of the carrier of K st ( dom p1) = ( dom p2) holds ( dom (p1 + p2)) = ( dom p1)

    proof

      let K be non empty addLoopStr, p1,p2 be FinSequence of the carrier of K;

      assume

       A1: ( dom p1) = ( dom p2);

      

       A2: ( rng <:p1, p2:>) c= [:( rng p1), ( rng p2):] & [:( rng p1), ( rng p2):] c= [:the carrier of K, the carrier of K:] by FUNCT_3: 51, ZFMISC_1: 96;

      

       A3: [:the carrier of K, the carrier of K:] = ( dom the addF of K) by FUNCT_2:def 1;

      

      thus ( dom (p1 + p2)) = ( dom (the addF of K .: (p1,p2))) by FVSUM_1:def 3

      .= ( dom <:p1, p2:>) by A2, A3, RELAT_1: 27, XBOOLE_1: 1

      .= (( dom p1) /\ ( dom p2)) by FUNCT_3:def 7

      .= ( dom p1) by A1;

    end;

    theorem :: POLYNOM1:2

    

     Th2: for L be non empty addLoopStr, F be FinSequence of (the carrier of L * ) holds ( dom ( Sum F)) = ( dom F)

    proof

      let L be non empty addLoopStr, F be FinSequence of (the carrier of L * );

      ( len ( Sum F)) = ( len F) by MATRLIN:def 6;

      hence thesis by FINSEQ_3: 29;

    end;

    theorem :: POLYNOM1:3

    

     Th3: for L be non empty addLoopStr, F be FinSequence of (the carrier of L * ) holds ( Sum ( <*> (the carrier of L * ))) = ( <*> the carrier of L)

    proof

      let L be non empty addLoopStr, F be FinSequence of (the carrier of L * );

      ( dom ( Sum ( <*> (the carrier of L * )))) = ( dom ( <*> (the carrier of L * ))) by Th2;

      hence thesis;

    end;

    theorem :: POLYNOM1:4

    

     Th4: for L be non empty addLoopStr, p be Element of (the carrier of L * ) holds <*( Sum p)*> = ( Sum <*p*>)

    proof

      let L be non empty addLoopStr, p be Element of (the carrier of L * );

       A1:

      now

        let i be Nat;

        assume i in ( dom <*p*>);

        then i in {1} by FINSEQ_1: 2, FINSEQ_1: 38;

        then

         A2: i = 1 by TARSKI:def 1;

        

        hence ( <*( Sum p)*> /. i) = ( Sum p) by FINSEQ_4: 16

        .= ( Sum ( <*p*> /. i)) by A2, FINSEQ_4: 16;

      end;

      

       A3: ( dom <*( Sum p)*>) = ( Seg 1) by FINSEQ_1: 38

      .= ( dom <*p*>) by FINSEQ_1: 38;

      then ( len <*( Sum p)*>) = ( len <*p*>) by FINSEQ_3: 29;

      hence thesis by A3, A1, MATRLIN:def 6;

    end;

    theorem :: POLYNOM1:5

    

     Th5: for L be non empty addLoopStr, F,G be FinSequence of (the carrier of L * ) holds ( Sum (F ^ G)) = (( Sum F) ^ ( Sum G))

    proof

      let L be non empty addLoopStr, F,G be FinSequence of (the carrier of L * );

      

       A1: ( dom ( Sum F)) = ( dom F) by Th2;

      

       A2: ( dom ( Sum G)) = ( dom G) by Th2;

      

       A3: ( len (( Sum F) ^ ( Sum G))) = (( len ( Sum F)) + ( len ( Sum G))) by FINSEQ_1: 22

      .= (( len F) + ( len ( Sum G))) by A1, FINSEQ_3: 29

      .= (( len F) + ( len G)) by A2, FINSEQ_3: 29

      .= ( len (F ^ G)) by FINSEQ_1: 22;

      then

       A4: ( dom (( Sum F) ^ ( Sum G))) = ( dom (F ^ G)) by FINSEQ_3: 29;

      

       A5: ( len ( Sum F)) = ( len F) by A1, FINSEQ_3: 29;

      now

        let i be Nat such that

         A6: i in ( dom (F ^ G));

        per cases by A6, FINSEQ_1: 25;

          suppose

           A7: i in ( dom F);

          

          thus ((( Sum F) ^ ( Sum G)) /. i) = ((( Sum F) ^ ( Sum G)) . i) by A4, A6, PARTFUN1:def 6

          .= (( Sum F) . i) by A1, A7, FINSEQ_1:def 7

          .= (( Sum F) /. i) by A1, A7, PARTFUN1:def 6

          .= ( Sum (F /. i)) by A1, A7, MATRLIN:def 6

          .= ( Sum ((F ^ G) /. i)) by A7, FINSEQ_4: 68;

        end;

          suppose ex n be Nat st n in ( dom G) & i = (( len F) + n);

          then

          consider n be Nat such that

           A8: n in ( dom G) and

           A9: i = (( len F) + n);

          

          thus ((( Sum F) ^ ( Sum G)) /. i) = ((( Sum F) ^ ( Sum G)) . i) by A4, A6, PARTFUN1:def 6

          .= (( Sum G) . n) by A2, A5, A8, A9, FINSEQ_1:def 7

          .= (( Sum G) /. n) by A2, A8, PARTFUN1:def 6

          .= ( Sum (G /. n)) by A2, A8, MATRLIN:def 6

          .= ( Sum ((F ^ G) /. i)) by A8, A9, FINSEQ_4: 69;

        end;

      end;

      hence thesis by A3, A4, MATRLIN:def 6;

    end;

    definition

      let L be non empty multMagma, p be FinSequence of the carrier of L, a be Element of L;

      :: original: *

      redefine

      :: POLYNOM1:def1

      func a * p means

      : Def1: ( dom it ) = ( dom p) & for i be object st i in ( dom p) holds (it /. i) = (a * (p /. i));

      compatibility

      proof

         A1:

        now

          set R = ((a multfield ) * p);

          let G be FinSequence of the carrier of L;

          assume that

           A2: ( dom G) = ( dom p) and

           A3: for i be object st i in ( dom p) holds (G /. i) = (a * (p /. i));

          

           A4: for k be object st k in ( dom G) holds (G . k) = (R . k)

          proof

            let k be object;

            assume

             A5: k in ( dom G);

            

            then (G . k) = (G /. k) by PARTFUN1:def 6

            .= (a * (p /. k)) by A2, A3, A5

            .= ((a multfield ) . (p /. k)) by FVSUM_1: 49

            .= ((a multfield ) . (p . k)) by A2, A5, PARTFUN1:def 6

            .= (R . k) by A2, A5, FUNCT_1: 13;

            hence thesis;

          end;

          ( rng p) c= the carrier of L & ( dom (a multfield )) = the carrier of L by FUNCT_2:def 1;

          then ( dom G) = ( dom R) by A2, RELAT_1: 27;

          then G = R by A4;

          hence G = (a * p) by FVSUM_1:def 6;

        end;

        set F = (a * p);

        

         A6: ( rng p) c= ( dom (a multfield ))

        proof

          let x be object;

          ( dom (a multfield )) = the carrier of L by FUNCT_2:def 1;

          hence thesis;

        end;

        

         A7: F = ((a multfield ) * p) by FVSUM_1:def 6;

        then

         A8: ( dom F) = ( dom p) by A6, RELAT_1: 27;

        for i be object st i in ( dom p) holds (F /. i) = (a * (p /. i))

        proof

          let i be object;

          assume

           A9: i in ( dom p);

          (F . i) = (((a multfield ) * p) . i) by FVSUM_1:def 6

          .= ((a multfield ) . (p . i)) by A9, FUNCT_1: 13

          .= ((a multfield ) . (p /. i)) by A9, PARTFUN1:def 6

          .= (a * (p /. i)) by FVSUM_1: 49;

          hence thesis by A8, A9, PARTFUN1:def 6;

        end;

        hence thesis by A7, A6, A1, RELAT_1: 27;

      end;

    end

    definition

      let L be non empty multMagma, p be FinSequence of the carrier of L, a be Element of L;

      :: POLYNOM1:def2

      func p * a -> FinSequence of the carrier of L means

      : Def2: ( dom it ) = ( dom p) & for i be object st i in ( dom p) holds (it /. i) = ((p /. i) * a);

      existence

      proof

        deffunc F( set) = ((p /. $1) * a);

        consider f be FinSequence of the carrier of L such that

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

         A2: for j be Nat st j in ( dom f) holds (f /. j) = F(j) from FINSEQ_4:sch 2;

        take f;

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

        hence thesis by A2;

      end;

      uniqueness

      proof

        let it1,it2 be FinSequence of the carrier of L such that

         A4: ( dom it1) = ( dom p) and

         A5: for i be object st i in ( dom p) holds (it1 /. i) = ((p /. i) * a) and

         A6: ( dom it2) = ( dom p) and

         A7: for i be object st i in ( dom p) holds (it2 /. i) = ((p /. i) * a);

        now

          let j be Nat;

          assume

           A8: j in ( dom p);

          

          hence (it1 /. j) = ((p /. j) * a) by A5

          .= (it2 /. j) by A7, A8;

        end;

        hence thesis by A4, A6, FINSEQ_5: 12;

      end;

    end

    theorem :: POLYNOM1:6

    

     Th6: for L be non empty multMagma, a be Element of L holds (a * ( <*> the carrier of L)) = ( <*> the carrier of L)

    proof

      let L be non empty multMagma, a be Element of L;

      ( dom (a * ( <*> the carrier of L))) = ( dom ( <*> the carrier of L)) by Def1;

      hence thesis;

    end;

    theorem :: POLYNOM1:7

    

     Th7: for L be non empty multMagma, a be Element of L holds (( <*> the carrier of L) * a) = ( <*> the carrier of L)

    proof

      let L be non empty multMagma, a be Element of L;

      ( dom (( <*> the carrier of L) * a)) = ( dom ( <*> the carrier of L)) by Def2;

      hence thesis;

    end;

    theorem :: POLYNOM1:8

    

     Th8: for L be non empty multMagma, a,b be Element of L holds (a * <*b*>) = <*(a * b)*>

    proof

      let L be non empty multMagma, a,b be Element of L;

      

       A1: for i be object st i in ( dom <*b*>) holds ( <*(a * b)*> /. i) = (a * ( <*b*> /. i))

      proof

        let i be object;

        assume i in ( dom <*b*>);

        then i in {1} by FINSEQ_1: 2, FINSEQ_1: 38;

        then

         A2: i = 1 by TARSKI:def 1;

        

        hence ( <*(a * b)*> /. i) = (a * b) by FINSEQ_4: 16

        .= (a * ( <*b*> /. i)) by A2, FINSEQ_4: 16;

      end;

      ( dom <*(a * b)*>) = ( Seg 1) by FINSEQ_1: 38

      .= ( dom <*b*>) by FINSEQ_1: 38;

      hence thesis by A1, Def1;

    end;

    theorem :: POLYNOM1:9

    

     Th9: for L be non empty multMagma, a,b be Element of L holds ( <*b*> * a) = <*(b * a)*>

    proof

      let L be non empty multMagma, a,b be Element of L;

      

       A1: for i be object st i in ( dom <*b*>) holds ( <*(b * a)*> /. i) = (( <*b*> /. i) * a)

      proof

        let i be object;

        assume i in ( dom <*b*>);

        then i in {1} by FINSEQ_1: 2, FINSEQ_1: 38;

        then

         A2: i = 1 by TARSKI:def 1;

        

        hence ( <*(b * a)*> /. i) = (b * a) by FINSEQ_4: 16

        .= (( <*b*> /. i) * a) by A2, FINSEQ_4: 16;

      end;

      ( dom <*(b * a)*>) = ( Seg 1) by FINSEQ_1: 38

      .= ( dom <*b*>) by FINSEQ_1: 38;

      hence thesis by A1, Def2;

    end;

    theorem :: POLYNOM1:10

    

     Th10: for L be non empty multMagma, a be Element of L, p,q be FinSequence of the carrier of L holds (a * (p ^ q)) = ((a * p) ^ (a * q))

    proof

      let L be non empty multMagma, a be Element of L, p,q be FinSequence of the carrier of L;

      

       A1: ( dom (a * (p ^ q))) = ( dom (p ^ q)) by Def1;

      

       A2: ( dom (a * q)) = ( dom q) by Def1;

      then

       A3: ( len (a * q)) = ( len q) by FINSEQ_3: 29;

      

       A4: ( dom (a * p)) = ( dom p) by Def1;

      then

       A5: ( len (a * p)) = ( len p) by FINSEQ_3: 29;

       A6:

      now

        let i be Nat;

        assume

         A7: i in ( dom (a * (p ^ q)));

        per cases by A1, A7, FINSEQ_1: 25;

          suppose

           A8: i in ( dom p);

          

          thus ((a * (p ^ q)) /. i) = (a * ((p ^ q) /. i)) by A1, A7, Def1

          .= (a * (p /. i)) by A8, FINSEQ_4: 68

          .= ((a * p) /. i) by A8, Def1

          .= (((a * p) ^ (a * q)) /. i) by A4, A8, FINSEQ_4: 68;

        end;

          suppose ex n be Nat st n in ( dom q) & i = (( len p) + n);

          then

          consider n be Nat such that

           A9: n in ( dom q) and

           A10: i = (( len p) + n);

          

          thus ((a * (p ^ q)) /. i) = (a * ((p ^ q) /. i)) by A1, A7, Def1

          .= (a * (q /. n)) by A9, A10, FINSEQ_4: 69

          .= ((a * q) /. n) by A9, Def1

          .= (((a * p) ^ (a * q)) /. i) by A5, A2, A9, A10, FINSEQ_4: 69;

        end;

      end;

      ( len ((a * p) ^ (a * q))) = (( len (a * p)) + ( len (a * q))) by FINSEQ_1: 22

      .= ( len (p ^ q)) by A5, A3, FINSEQ_1: 22;

      then ( dom (a * (p ^ q))) = ( dom ((a * p) ^ (a * q))) by A1, FINSEQ_3: 29;

      hence thesis by A6, FINSEQ_5: 12;

    end;

    theorem :: POLYNOM1:11

    

     Th11: for L be non empty multMagma, a be Element of L, p,q be FinSequence of the carrier of L holds ((p ^ q) * a) = ((p * a) ^ (q * a))

    proof

      let L be non empty multMagma, a be Element of L, p,q be FinSequence of the carrier of L;

      

       A1: ( dom ((p ^ q) * a)) = ( dom (p ^ q)) by Def2;

      

       A2: ( dom (q * a)) = ( dom q) by Def2;

      then

       A3: ( len (q * a)) = ( len q) by FINSEQ_3: 29;

      

       A4: ( dom (p * a)) = ( dom p) by Def2;

      then

       A5: ( len (p * a)) = ( len p) by FINSEQ_3: 29;

       A6:

      now

        let i be Nat;

        assume

         A7: i in ( dom ((p ^ q) * a));

        per cases by A1, A7, FINSEQ_1: 25;

          suppose

           A8: i in ( dom p);

          

          thus (((p ^ q) * a) /. i) = (((p ^ q) /. i) * a) by A1, A7, Def2

          .= ((p /. i) * a) by A8, FINSEQ_4: 68

          .= ((p * a) /. i) by A8, Def2

          .= (((p * a) ^ (q * a)) /. i) by A4, A8, FINSEQ_4: 68;

        end;

          suppose ex n be Nat st n in ( dom q) & i = (( len p) + n);

          then

          consider n be Nat such that

           A9: n in ( dom q) and

           A10: i = (( len p) + n);

          

          thus (((p ^ q) * a) /. i) = (((p ^ q) /. i) * a) by A1, A7, Def2

          .= ((q /. n) * a) by A9, A10, FINSEQ_4: 69

          .= ((q * a) /. n) by A9, Def2

          .= (((p * a) ^ (q * a)) /. i) by A5, A2, A9, A10, FINSEQ_4: 69;

        end;

      end;

      ( len ((p * a) ^ (q * a))) = (( len (p * a)) + ( len (q * a))) by FINSEQ_1: 22

      .= ( len (p ^ q)) by A5, A3, FINSEQ_1: 22;

      then ( dom ((p ^ q) * a)) = ( dom ((p * a) ^ (q * a))) by A1, FINSEQ_3: 29;

      hence thesis by A6, FINSEQ_5: 12;

    end;

    registration

      cluster right_unital for non empty strict multLoopStr_0;

      existence

      proof

        take multEX_0 ;

        thus thesis;

      end;

    end

    registration

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

      existence

      proof

        take F_Real ;

        thus thesis;

      end;

    end

    theorem :: POLYNOM1:12

    

     Th12: for L be add-associative right_zeroed right_complementable right_unital distributive non empty doubleLoopStr, a be Element of L, p be FinSequence of the carrier of L holds ( Sum (a * p)) = (a * ( Sum p))

    proof

      let L be add-associative right_zeroed right_complementable right_unital distributive non empty doubleLoopStr, a be Element of L;

      set p = ( <*> the carrier of L);

      defpred P[ FinSequence of the carrier of L] means ( Sum (a * $1)) = (a * ( Sum $1));

       A1:

      now

        let p be FinSequence of the carrier of L, r be Element of L such that

         A2: P[p];

        ( Sum (a * (p ^ <*r*>))) = ( Sum ((a * p) ^ (a * <*r*>))) by Th10

        .= (( Sum (a * p)) + ( Sum (a * <*r*>))) by RLVECT_1: 41

        .= (( Sum (a * p)) + ( Sum <*(a * r)*>)) by Th8

        .= (( Sum (a * p)) + (a * r)) by RLVECT_1: 44

        .= ((a * ( Sum p)) + (a * ( Sum <*r*>))) by A2, RLVECT_1: 44

        .= (a * (( Sum p) + ( Sum <*r*>))) by VECTSP_1:def 7

        .= (a * ( Sum (p ^ <*r*>))) by RLVECT_1: 41;

        hence P[(p ^ <*r*>)];

      end;

      ( Sum p) = ( 0. L) & ( Sum (a * p)) = ( Sum p) by Th6, RLVECT_1: 43;

      then

       A3: P[p];

      thus for p be FinSequence of the carrier of L holds P[p] from FINSEQ_2:sch 2( A3, A1);

    end;

    theorem :: POLYNOM1:13

    

     Th13: for L be add-associative right_zeroed right_complementable right_unital distributive non empty doubleLoopStr, a be Element of L, p be FinSequence of the carrier of L holds ( Sum (p * a)) = (( Sum p) * a)

    proof

      let L be add-associative right_zeroed right_complementable right_unital distributive non empty doubleLoopStr, a be Element of L;

      set p = ( <*> the carrier of L);

      defpred P[ FinSequence of the carrier of L] means ( Sum ($1 * a)) = (( Sum $1) * a);

       A1:

      now

        let p be FinSequence of the carrier of L, r be Element of L such that

         A2: P[p];

        ( Sum ((p ^ <*r*>) * a)) = ( Sum ((p * a) ^ ( <*r*> * a))) by Th11

        .= (( Sum (p * a)) + ( Sum ( <*r*> * a))) by RLVECT_1: 41

        .= (( Sum (p * a)) + ( Sum <*(r * a)*>)) by Th9

        .= (( Sum (p * a)) + (r * a)) by RLVECT_1: 44

        .= ((( Sum p) * a) + (( Sum <*r*>) * a)) by A2, RLVECT_1: 44

        .= ((( Sum p) + ( Sum <*r*>)) * a) by VECTSP_1:def 7

        .= (( Sum (p ^ <*r*>)) * a) by RLVECT_1: 41;

        hence P[(p ^ <*r*>)];

      end;

      ( Sum p) = ( 0. L) & ( Sum (p * a)) = ( Sum p) by Th7, RLVECT_1: 43;

      then

       A3: P[p];

      thus for p be FinSequence of the carrier of L holds P[p] from FINSEQ_2:sch 2( A3, A1);

    end;

    begin

    theorem :: POLYNOM1:14

    

     Th14: for L be add-associative right_zeroed right_complementable non empty addLoopStr, F be FinSequence of (the carrier of L * ) holds ( Sum ( FlattenSeq F)) = ( Sum ( Sum F))

    proof

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

      defpred P[ FinSequence of (the carrier of L * )] means ( Sum ( FlattenSeq $1)) = ( Sum ( Sum $1));

      

       A1: for f be FinSequence of (the carrier of L * ), p be Element of (the carrier of L * ) st P[f] holds P[(f ^ <*p*>)]

      proof

        let f be FinSequence of (the carrier of L * ), p be Element of (the carrier of L * ) such that

         A2: ( Sum ( FlattenSeq f)) = ( Sum ( Sum f));

        

        thus ( Sum ( FlattenSeq (f ^ <*p*>))) = ( Sum (( FlattenSeq f) ^ ( FlattenSeq <*p*>))) by PRE_POLY: 3

        .= ( Sum (( FlattenSeq f) ^ p)) by PRE_POLY: 1

        .= (( Sum ( Sum f)) + ( Sum p)) by A2, RLVECT_1: 41

        .= (( Sum ( Sum f)) + ( Sum <*( Sum p)*>)) by RLVECT_1: 44

        .= ( Sum (( Sum f) ^ <*( Sum p)*>)) by RLVECT_1: 41

        .= ( Sum (( Sum f) ^ ( Sum <*p*>))) by Th4

        .= ( Sum ( Sum (f ^ <*p*>))) by Th5;

      end;

      ( Sum ( FlattenSeq ( <*> (the carrier of L * )))) = ( Sum ( <*> the carrier of L));

      then

       A3: P[( <*> (the carrier of L * ))] by Th3;

      thus for f be FinSequence of (the carrier of L * ) holds P[f] from FINSEQ_2:sch 2( A3, A1);

    end;

    definition

      let S be ZeroStr, f be the carrier of S -valued Function;

      :: POLYNOM1:def3

      func Support f -> set means

      : Def3: for x be object holds x in it iff x in ( dom f) & (f . x) <> ( 0. S);

      existence

      proof

        defpred P[ object] means (f . $1) <> ( 0. S);

        consider X be set such that

         A1: for x be object holds x in X iff x in ( dom f) & P[x] from XBOOLE_0:sch 1;

        take X;

        thus thesis by A1;

      end;

      uniqueness

      proof

        let A,B be set such that

         A2: for x be object holds x in A iff x in ( dom f) & (f . x) <> ( 0. S) and

         A3: for x be object holds x in B iff x in ( dom f) & (f . x) <> ( 0. S);

        now

          let x be object;

          x in A iff x in ( dom f) & (f . x) <> ( 0. S) by A2;

          hence x in A iff x in B by A3;

        end;

        hence thesis by TARSKI: 2;

      end;

    end

    definition

      let X be non empty set, S be non empty ZeroStr, f be Function of X, S;

      :: original: Support

      redefine

      :: POLYNOM1:def4

      func Support f -> Subset of X means

      : Def4: for x be Element of X holds x in it iff (f . x) <> ( 0. S);

      coherence

      proof

        ( Support f) c= ( dom f) by Def3;

        hence ( Support f) is Subset of X by XBOOLE_1: 1;

      end;

      compatibility

      proof

        let A be Subset of X;

        

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

        hence A = ( Support f) implies for x be Element of X holds x in A iff (f . x) <> ( 0. S) by Def3;

        assume

         A2: for x be Element of X holds x in A iff (f . x) <> ( 0. S);

        

         A3: ( Support f) c= ( dom f) by Def3;

        thus A c= ( Support f)

        proof

          let e be object;

          assume

           A4: e in A;

          then (f . e) <> ( 0. S) by A2;

          hence e in ( Support f) by A4, A1, Def3;

        end;

        let e be object;

        assume

         A5: e in ( Support f);

        then

         A6: (f . e) <> ( 0. S) by Def3;

        ( Support f) c= X by A3, XBOOLE_1: 1;

        hence e in A by A2, A6, A5;

      end;

    end

    definition

      let S be ZeroStr, p be the carrier of S -valued Function;

      :: POLYNOM1:def5

      attr p is finite-Support means

      : Def5: ( Support p) is finite;

    end

    definition

      let n be set, L be non empty 1-sorted, p be Function of ( Bags n), L, x be bag of n;

      :: original: .

      redefine

      func p . x -> Element of L ;

      coherence

      proof

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

        reconsider f = p as Function of ( Bags n), the carrier of L;

        (f . b) is Element of L;

        hence thesis;

      end;

    end

    begin

    definition

      let X be set, S be 1-sorted;

      mode Series of X,S is Function of ( Bags X), S;

    end

    definition

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

      :: POLYNOM1:def6

      func p + q -> Series of n, L equals (p + q);

      coherence ;

    end

    theorem :: POLYNOM1:15

    

     Th15: for n be set, L be non empty addLoopStr, p,q be Series of n, L holds for x be bag of n holds ((p + q) . x) = ((p . x) + (q . x))

    proof

      let n be set;

      let L be non empty addLoopStr;

      let p,q be Series of n, L;

      let x be bag of n;

      

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

      

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

      then

       A3: (p /. x) = (p . x) & (q /. x) = (q . x) by A1, PARTFUN1:def 6;

      

       A4: ( dom (p + q)) = (( dom p) /\ ( dom q)) by VFUNCT_1:def 1;

      

      hence ((p + q) . x) = ((p + q) /. x) by A1, A2, PARTFUN1:def 6

      .= ((p . x) + (q . x)) by A1, A2, A3, A4, VFUNCT_1:def 1;

    end;

    theorem :: POLYNOM1:16

    for n be set, L be non empty addLoopStr, p,q,r be Series of n, L st for x be bag of n holds (r . x) = ((p . x) + (q . x)) holds r = (p + q)

    proof

      let n be set;

      let L be non empty addLoopStr;

      let p,q,r be Series of n, L;

      assume

       A1: for x be bag of n holds (r . x) = ((p . x) + (q . x));

      let x be Element of ( Bags n);

      

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

      

       A3: ((p + q) /. x) = ((p + q) . x);

      

       A4: (p /. x) = (p . x) & (q /. x) = (q . x);

      

      thus (r . x) = ((p . x) + (q . x)) by A1

      .= ((p + q) . x) by A2, A3, A4, VFUNCT_1:def 1;

    end;

    theorem :: POLYNOM1:17

    

     Th17: for n be set, L be add-associative right_zeroed right_complementable non empty addLoopStr, p be Series of n, L holds for x be bag of n holds (( - p) . x) = ( - (p . x))

    proof

      let n be set;

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

      let p be Series of n, L;

      let x be bag of n;

      

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

      

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

      then

       A3: (p /. x) = (p . x) by A1, PARTFUN1:def 6;

      

       A4: ( dom ( - p)) = ( dom p) by VFUNCT_1:def 5;

      

      hence (( - p) . x) = (( - p) /. x) by A1, A2, PARTFUN1:def 6

      .= ( - (p . x)) by A1, A2, A3, A4, VFUNCT_1:def 5;

    end;

    theorem :: POLYNOM1:18

    for n be set, L be add-associative right_zeroed right_complementable non empty addLoopStr, p,r be Series of n, L st for x be bag of n holds (r . x) = ( - (p . x)) holds r = ( - p)

    proof

      let n be set;

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

      let p,r be Series of n, L;

      assume

       A1: for x be bag of n holds (r . x) = ( - (p . x));

      let x be Element of ( Bags n);

      

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

      

       A3: (( - p) /. x) = (( - p) . x);

      

       A4: (p /. x) = (p . x);

      

      thus (r . x) = ( - (p . x)) by A1

      .= (( - p) . x) by A2, A3, A4, VFUNCT_1:def 5;

    end;

    theorem :: POLYNOM1:19

    for n be set, L be add-associative right_zeroed right_complementable non empty addLoopStr, p be Series of n, L holds p = ( - ( - p))

    proof

      let n be set, L be add-associative right_zeroed right_complementable non empty addLoopStr, p be Series of n, L;

      set r = ( - p);

      

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

      

       A2: ( dom ( - p)) = ( dom p) by VFUNCT_1:def 5;

      

       A3: ( dom ( - ( - p))) = ( dom ( - p)) by VFUNCT_1:def 5;

      now

        let x be Element of ( Bags n);

        assume x in ( dom p);

        

         A4: (p . x) = (p /. x);

        

        thus (p . x) = ( - ( - (p . x))) by RLVECT_1: 17

        .= ( - (( - p) /. x)) by A1, A2, A4, VFUNCT_1:def 5

        .= (( - ( - p)) /. x) by A1, A2, A3, VFUNCT_1:def 5

        .= (( - r) . x);

      end;

      hence thesis by A1;

    end;

    theorem :: POLYNOM1:20

    

     Th20: for n be set, L be right_zeroed non empty addLoopStr, p,q be Series of n, L holds ( Support (p + q)) c= (( Support p) \/ ( Support q))

    proof

      let n be set, L be right_zeroed non empty addLoopStr, p,q be Series of n, L;

      set f = (p + q), Sp = ( Support p), Sq = ( Support q);

      let x be object;

      assume

       A1: x in ( Support f);

      then

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

      (f . x9) <> ( 0. L) by A1, Def4;

      then ((p . x9) + (q . x9)) <> ( 0. L) by Th15;

      then not ((p . x9) = ( 0. L) & (q . x9) = ( 0. L)) by RLVECT_1:def 4;

      then x9 in Sp or x9 in Sq by Def4;

      hence thesis by XBOOLE_0:def 3;

    end;

    definition

      let n be set, L be Abelian right_zeroed non empty addLoopStr, p,q be Series of n, L;

      :: original: +

      redefine

      func p + q;

      commutativity

      proof

        let p,q be Series of n, L;

        now

          let b be Element of ( Bags n);

          

          thus ((p + q) . b) = ((q . b) + (p . b)) by Th15

          .= ((q + p) . b) by Th15;

        end;

        hence (p + q) = (q + p);

      end;

    end

    theorem :: POLYNOM1:21

    

     Th21: for n be set, L be add-associative right_zeroed non empty doubleLoopStr, p,q,r be Series of n, L holds ((p + q) + r) = (p + (q + r))

    proof

      let n be set, L be add-associative right_zeroed non empty doubleLoopStr, p,q,r be Series of n, L;

      now

        let b be Element of ( Bags n);

        

        thus (((p + q) + r) . b) = (((p + q) . b) + (r . b)) by Th15

        .= (((p . b) + (q . b)) + (r . b)) by Th15

        .= ((p . b) + ((q . b) + (r . b))) by RLVECT_1:def 3

        .= ((p . b) + ((q + r) . b)) by Th15

        .= ((p + (q + r)) . b) by Th15;

      end;

      hence thesis;

    end;

    definition

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

      :: POLYNOM1:def7

      func p - q -> Series of n, L equals (p + ( - q));

      coherence ;

    end

    definition

      let n be set, S be non empty ZeroStr;

      :: POLYNOM1:def8

      func 0_ (n,S) -> Series of n, S equals (( Bags n) --> ( 0. S));

      coherence ;

    end

    theorem :: POLYNOM1:22

    

     Th22: for n be set, S be non empty ZeroStr, b be bag of n holds (( 0_ (n,S)) . b) = ( 0. S)

    proof

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

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

      hence thesis by FUNCOP_1: 7;

    end;

    theorem :: POLYNOM1:23

    

     Th23: for n be set, L be right_zeroed non empty addLoopStr, p be Series of n, L holds (p + ( 0_ (n,L))) = p

    proof

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

      reconsider ls = (p + ( 0_ (n,L))), p9 = p as Function of ( Bags n), the carrier of L;

      now

        let b be Element of ( Bags n);

        

        thus (ls . b) = ((p . b) + (( 0_ (n,L)) . b)) by Th15

        .= ((p9 . b) + ( 0. L))

        .= (p9 . b) by RLVECT_1:def 4;

      end;

      hence thesis;

    end;

    definition

      let n be set, L be right_unital non empty multLoopStr_0;

      :: POLYNOM1:def9

      func 1_ (n,L) -> Series of n, L equals (( 0_ (n,L)) +* (( EmptyBag n),( 1. L)));

      coherence ;

    end

    theorem :: POLYNOM1:24

    

     Th24: for n be set, L be add-associative right_zeroed right_complementable non empty addLoopStr, p be Series of n, L holds (p - p) = ( 0_ (n,L))

    proof

      let n be set, L be add-associative right_zeroed right_complementable non empty addLoopStr, p be Series of n, L;

      reconsider pp = (p - p), Z = ( 0_ (n,L)) as Function of ( Bags n), the carrier of L;

      now

        let b be Element of ( Bags n);

        

        thus (pp . b) = ((p . b) + (( - p) . b)) by Th15

        .= ((p . b) + ( - (p . b))) by Th17

        .= ( 0. L) by RLVECT_1:def 10

        .= (Z . b);

      end;

      hence thesis;

    end;

    theorem :: POLYNOM1:25

    

     Th25: for n be set, L be right_unital non empty multLoopStr_0 holds (( 1_ (n,L)) . ( EmptyBag n)) = ( 1. L) & for b be bag of n st b <> ( EmptyBag n) holds (( 1_ (n,L)) . b) = ( 0. L)

    proof

      let n be set, L be right_unital non empty multLoopStr_0;

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

      ( dom Z) = ( Bags n);

      hence (( 1_ (n,L)) . ( EmptyBag n)) = ( 1. L) by FUNCT_7: 31;

      let b be bag of n;

      

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

      assume b <> ( EmptyBag n);

      

      hence (( 1_ (n,L)) . b) = (Z . b) by FUNCT_7: 32

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

    end;

    definition

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

      :: POLYNOM1:def10

      func p *' q -> Series of n, L means

      : Def10: for b be bag of n holds ex s be FinSequence of the carrier of L st (it . b) = ( Sum s) & ( len s) = ( len ( decomp b)) & 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) * (q . b2));

      existence

      proof

        defpred P[ Element of ( Bags n), Element of L] means ex b be bag of n st b = $1 & ex s be FinSequence of the carrier of L st $2 = ( Sum s) & ( len s) = ( len ( decomp b)) & 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) * (q . b2));

         A1:

        now

          let bb be Element of ( Bags n);

          reconsider b = bb as bag of n;

          defpred Q[ Nat, set] means ex b1,b2 be bag of n st (( decomp b) /. $1) = <*b1, b2*> & $2 = ((p . b1) * (q . b2));

           A2:

          now

            let k be Nat;

            assume k in ( Seg ( len ( decomp b)));

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

            then

            consider b1,b2 be bag of n such that

             A3: (( decomp b) /. k) = <*b1, b2*> and b = (b1 + b2) by PRE_POLY: 68;

            reconsider x = ((p . b1) * (q . b2)) as Element of L;

            take x;

            thus Q[k, x] by A3;

          end;

          consider s be FinSequence of the carrier of L such that

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

           A5: for k be Nat st k in ( Seg ( len ( decomp b))) holds Q[k, (s /. k)] from FINSEQ_4:sch 1( A2);

          reconsider y = ( Sum s) as Element of L;

          take y;

          thus P[bb, y]

          proof

            take b;

            thus b = bb;

            take s;

            thus y = ( Sum s);

            thus ( len s) = ( len ( decomp b)) by A4;

            let k be Element of NAT ;

            assume k in ( dom s);

            then k in ( Seg ( len ( decomp b))) by A4, FINSEQ_1:def 3;

            hence thesis by A5;

          end;

        end;

        consider P be Function of ( Bags n), the carrier of L such that

         A6: for b be Element of ( Bags n) holds P[b, (P . b)] from FUNCT_2:sch 3( A1);

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

        reconsider P as Series of n, L;

        take P;

        let b be bag of n;

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

         P[bb, (P . bb)] by A6;

        hence thesis;

      end;

      uniqueness

      proof

        let it1,it2 be Series of n, L such that

         A7: for b be bag of n holds ex s be FinSequence of the carrier of L st (it1 . b) = ( Sum s) & ( len s) = ( len ( decomp b)) & 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) * (q . b2)) and

         A8: for b be bag of n holds ex s be FinSequence of the carrier of L st (it2 . b) = ( Sum s) & ( len s) = ( len ( decomp b)) & 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) * (q . b2));

        reconsider ita = it1, itb = it2 as Function of ( Bags n), the carrier of L;

        now

          let b be Element of ( Bags n);

          consider sa be FinSequence of the carrier of L such that

           A9: (ita . b) = ( Sum sa) and

           A10: ( len sa) = ( len ( decomp b)) and

           A11: for k be Element of NAT st k in ( dom sa) holds ex b1,b2 be bag of n st (( decomp b) /. k) = <*b1, b2*> & (sa /. k) = ((p . b1) * (q . b2)) by A7;

          consider sb be FinSequence of the carrier of L such that

           A12: (itb . b) = ( Sum sb) and

           A13: ( len sb) = ( len ( decomp b)) and

           A14: for k be Element of NAT st k in ( dom sb) holds ex b1,b2 be bag of n st (( decomp b) /. k) = <*b1, b2*> & (sb /. k) = ((p . b1) * (q . b2)) by A8;

          now

            let k be Nat;

            assume

             A15: 1 <= k & k <= ( len sa);

            then

             A16: k in ( dom sa) by FINSEQ_3: 25;

            then

             A17: (sa /. k) = (sa . k) by PARTFUN1:def 6;

            

             A18: k in ( dom sb) by A10, A13, A15, FINSEQ_3: 25;

            then

             A19: (sb /. k) = (sb . k) by PARTFUN1:def 6;

            consider ab1,ab2 be bag of n such that

             A20: (( decomp b) /. k) = <*ab1, ab2*> and

             A21: (sa /. k) = ((p . ab1) * (q . ab2)) by A11, A16;

            consider bb1,bb2 be bag of n such that

             A22: (( decomp b) /. k) = <*bb1, bb2*> and

             A23: (sb /. k) = ((p . bb1) * (q . bb2)) by A14, A18;

            ab1 = bb1 by A20, A22, FINSEQ_1: 77;

            hence (sa . k) = (sb . k) by A20, A21, A22, A23, A17, A19, FINSEQ_1: 77;

          end;

          hence (ita . b) = (itb . b) by A9, A10, A12, A13, FINSEQ_1: 14;

        end;

        hence it1 = it2;

      end;

    end

    theorem :: POLYNOM1:26

    

     Th26: for n be Ordinal, L be Abelian add-associative right_zeroed right_complementable distributive associative non empty doubleLoopStr, p,q,r be Series of n, L holds (p *' (q + r)) = ((p *' q) + (p *' r))

    proof

      let n be Ordinal, L be Abelian add-associative right_zeroed right_complementable distributive associative non empty doubleLoopStr, p,q,r be Series of n, L;

      set cL = the carrier of L;

      now

        let b be Element of ( Bags n);

        consider s be FinSequence of cL such that

         A1: ((p *' (q + r)) . b) = ( Sum s) and

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

         A3: 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) * ((q + r) . b2)) by Def10;

        consider u be FinSequence of cL such that

         A4: ((p *' r) . b) = ( Sum u) and

         A5: ( len u) = ( len ( decomp b)) and

         A6: for k be Element of NAT st k in ( dom u) holds ex b1,b2 be bag of n st (( decomp b) /. k) = <*b1, b2*> & (u /. k) = ((p . b1) * (r . b2)) by Def10;

        consider t be FinSequence of cL such that

         A7: ((p *' q) . b) = ( Sum t) and

         A8: ( len t) = ( len ( decomp b)) and

         A9: for k be Element of NAT st k in ( dom t) holds ex b1,b2 be bag of n st (( decomp b) /. k) = <*b1, b2*> & (t /. k) = ((p . b1) * (q . b2)) by Def10;

        reconsider t, u as Element of (( len s) -tuples_on cL) by A2, A8, A5, FINSEQ_2: 92;

        

         A10: ( dom u) = ( dom s) by A2, A5, FINSEQ_3: 29;

        

         A11: ( dom t) = ( dom s) by A2, A8, FINSEQ_3: 29;

        then

         A12: ( dom (t + u)) = ( dom s) by A10, Th1;

         A13:

        now

          let i be Nat;

          assume

           A14: i in ( dom s);

          then

          consider sb1,sb2 be bag of n such that

           A15: (( decomp b) /. i) = <*sb1, sb2*> and

           A16: (s /. i) = ((p . sb1) * ((q + r) . sb2)) by A3;

          

           A17: (t /. i) = (t . i) & (u /. i) = (u . i) by A11, A10, A14, PARTFUN1:def 6;

          consider ub1,ub2 be bag of n such that

           A18: (( decomp b) /. i) = <*ub1, ub2*> and

           A19: (u /. i) = ((p . ub1) * (r . ub2)) by A6, A10, A14;

          

           A20: sb1 = ub1 & sb2 = ub2 by A15, A18, FINSEQ_1: 77;

          consider tb1,tb2 be bag of n such that

           A21: (( decomp b) /. i) = <*tb1, tb2*> and

           A22: (t /. i) = ((p . tb1) * (q . tb2)) by A9, A11, A14;

          

           A23: sb1 = tb1 & sb2 = tb2 by A15, A21, FINSEQ_1: 77;

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

          

          hence (s . i) = ((p . sb1) * ((q . sb2) + (r . sb2))) by A16, Th15

          .= (((p . sb1) * (q . sb2)) + ((p . sb1) * (r . sb2))) by VECTSP_1:def 7

          .= ((t + u) . i) by A12, A14, A22, A19, A23, A20, A17, FVSUM_1: 17;

        end;

        ( len (t + u)) = ( len s) by A12, FINSEQ_3: 29;

        then s = (t + u) by A13, FINSEQ_2: 9;

        

        hence ((p *' (q + r)) . b) = (( Sum t) + ( Sum u)) by A1, FVSUM_1: 76

        .= (((p *' q) + (p *' r)) . b) by A7, A4, Th15;

      end;

      hence thesis;

    end;

    theorem :: POLYNOM1:27

    

     Th27: for n be Ordinal, L be Abelian add-associative right_zeroed right_complementable right_unital distributive associative non empty doubleLoopStr, p,q,r be Series of n, L holds ((p *' q) *' r) = (p *' (q *' r))

    proof

      let n be Ordinal, L be Abelian add-associative right_zeroed right_complementable right_unital distributive associative non empty doubleLoopStr, p,q,r be Series of n, L;

      set cL = the carrier of L;

      reconsider pqra = ((p *' q) *' r), pqrb = (p *' (q *' r)) as Function of ( Bags n), cL;

      set pq = (p *' q), qr = (q *' r);

      now

        let b be Element of ( Bags n);

        set db = ( decomp b);

        deffunc F( Nat) = (( decomp ((db /. $1) /. 1) qua Element of ( Bags n)) ^^ (( len ( decomp ((db /. $1) /. 1) qua Element of ( Bags n))) |-> <*((db /. $1) /. 2)*>));

        consider dbl be FinSequence such that

         A1: ( len dbl) = ( len db) and

         A2: for k be Nat st k in ( dom dbl) holds (dbl . k) = F(k) from FINSEQ_1:sch 2;

        

         A3: ( rng dbl) c= ((3 -tuples_on ( Bags n)) * )

        proof

          let y be object;

          assume y in ( rng dbl);

          then

          consider k be object such that

           A4: k in ( dom dbl) and

           A5: y = (dbl . k) by FUNCT_1:def 3;

          reconsider k as set by TARSKI: 1;

          set dbk2 = ((db /. k) /. 2);

          set ddbk1 = ( decomp ((db /. k) /. 1) qua Element of ( Bags n));

          reconsider k as Nat by A4;

          set dblk = (ddbk1 ^^ (( len ddbk1) |-> <*dbk2*>));

          

           A6: ( dom dblk) = (( dom ddbk1) /\ ( dom (( len ddbk1) |-> <*dbk2*>))) by PRE_POLY:def 4

          .= (( dom ddbk1) /\ ( Seg ( len ddbk1)))

          .= (( dom ddbk1) /\ ( dom ddbk1)) by FINSEQ_1:def 3

          .= ( dom ddbk1);

          

           A7: ( dom ddbk1) = ( Seg ( len ddbk1)) by FINSEQ_1:def 3;

          ( rng dblk) c= (3 -tuples_on ( Bags n))

          proof

            reconsider Gi = <*dbk2*> as Element of (1 -tuples_on ( Bags n)) by FINSEQ_2: 98;

            let y be object;

            assume y in ( rng dblk);

            then

            consider i be object such that

             A8: i in ( dom dblk) and

             A9: (dblk . i) = y by FUNCT_1:def 3;

            (ddbk1 . i) in ( rng ddbk1) by A6, A8, FUNCT_1:def 3;

            then

            reconsider Fi = (ddbk1 . i) as Element of (2 -tuples_on ( Bags n));

            reconsider i9 = i as Element of NAT by A8;

            ((( len ddbk1) |-> <*dbk2*>) . i9) = <*dbk2*> by A6, A7, A8, FUNCOP_1: 7;

            then y = (Fi ^ Gi) by A8, A9, PRE_POLY:def 4;

            hence thesis by FINSEQ_2: 131;

          end;

          then

           A10: dblk is FinSequence of (3 -tuples_on ( Bags n)) by FINSEQ_1:def 4;

          (dbl . k) = (ddbk1 ^^ (( len ddbk1) |-> <*dbk2*>)) by A2, A4;

          hence thesis by A5, A10, FINSEQ_1:def 11;

        end;

        deffunc F( Element of (3 -tuples_on ( Bags n))) = (((p . ($1 /. 1)) * (q . ($1 /. 2))) * (r . ($1 /. 3)));

        consider v be Function of (3 -tuples_on ( Bags n)), cL such that

         A11: for b be Element of (3 -tuples_on ( Bags n)) holds (v . b) = F(b) from FUNCT_2:sch 4;

        deffunc G( Nat) = ((( len ( decomp ((db /. $1) /. 2) qua Element of ( Bags n))) |-> <*((db /. $1) /. 1)*>) ^^ ( decomp ((db /. $1) /. 2) qua Element of ( Bags n)));

        consider dbr be FinSequence such that

         A12: ( len dbr) = ( len db) and

         A13: for k be Nat st k in ( dom dbr) holds (dbr . k) = G(k) from FINSEQ_1:sch 2;

        ( rng dbr) c= ((3 -tuples_on ( Bags n)) * )

        proof

          let y be object;

          assume y in ( rng dbr);

          then

          consider k be object such that

           A14: k in ( dom dbr) and

           A15: y = (dbr . k) by FUNCT_1:def 3;

          reconsider k as Nat by A14;

          set ddbk1 = ( decomp ((db /. k) /. 2) qua Element of ( Bags n));

          set dbk2 = ((db /. k) /. 1);

          set dbrk = ((( len ddbk1) |-> <*dbk2*>) ^^ ddbk1);

          

           A16: ( dom dbrk) = (( dom ddbk1) /\ ( dom (( len ddbk1) |-> <*dbk2*>))) by PRE_POLY:def 4

          .= (( dom ddbk1) /\ ( Seg ( len ddbk1)))

          .= (( dom ddbk1) /\ ( dom ddbk1)) by FINSEQ_1:def 3

          .= ( dom ddbk1);

          

           A17: ( dom ddbk1) = ( Seg ( len ddbk1)) by FINSEQ_1:def 3;

          ( rng dbrk) c= (3 -tuples_on ( Bags n))

          proof

            reconsider Gi = <*dbk2*> as Element of (1 -tuples_on ( Bags n)) by FINSEQ_2: 98;

            let y be object;

            assume y in ( rng dbrk);

            then

            consider i be object such that

             A18: i in ( dom dbrk) and

             A19: (dbrk . i) = y by FUNCT_1:def 3;

            (ddbk1 . i) in ( rng ddbk1) by A16, A18, FUNCT_1:def 3;

            then

            reconsider Fi = (ddbk1 . i) as Element of (2 -tuples_on ( Bags n));

            reconsider i9 = i as Element of NAT by A18;

            ((( len ddbk1) |-> <*dbk2*>) . i9) = <*dbk2*> by A16, A17, A18, FUNCOP_1: 7;

            then y = (Gi ^ Fi) by A18, A19, PRE_POLY:def 4;

            hence thesis by FINSEQ_2: 131;

          end;

          then

           A20: dbrk is FinSequence of (3 -tuples_on ( Bags n)) by FINSEQ_1:def 4;

          (dbr . k) = ((( len ddbk1) |-> <*dbk2*>) ^^ ddbk1) by A13, A14;

          hence thesis by A15, A20, FINSEQ_1:def 11;

        end;

        then

        reconsider dbl, dbr as FinSequence of ((3 -tuples_on ( Bags n)) * ) by A3, FINSEQ_1:def 4;

        set fdbl = ( FlattenSeq dbl), fdbr = ( FlattenSeq dbr);

        consider ls be FinSequence of cL such that

         A21: (pqra . b) = ( Sum ls) and

         A22: ( len ls) = ( len ( decomp b)) and

         A23: for k be Element of NAT st k in ( dom ls) holds ex b1,b2 be bag of n st (db /. k) = <*b1, b2*> & (ls /. k) = ((pq . b1) * (r . b2)) by Def10;

        

         A24: ( dom dbr) = ( dom db) by A12, FINSEQ_3: 29;

        reconsider vfdbl = (v * fdbl), vfdbr = (v * fdbr) as FinSequence of cL by FINSEQ_2: 32;

        consider vdbl be FinSequence of (cL * ) such that

         A25: vdbl = ((( dom dbl) --> v) ** dbl) and

         A26: vfdbl = ( FlattenSeq vdbl) by PRE_POLY: 32;

        

         A27: ( dom v) = (3 -tuples_on ( Bags n)) by FUNCT_2:def 1;

        now

          set f = ( Sum vdbl);

          

           A28: ( dom vdbl) = (( dom (( dom dbl) --> v)) /\ ( dom dbl)) by A25, PBOOLE:def 19

          .= (( dom dbl) /\ ( dom dbl))

          .= ( dom dbl);

          

           A29: ( dom f) = ( dom vdbl) by Th2;

          hence ( len ( Sum vdbl)) = ( len ls) by A22, A1, A28, FINSEQ_3: 29;

          let k be Nat such that

           A30: 1 <= k & k <= ( len ls);

          

           A31: k in ( dom f) by A22, A1, A29, A28, A30, FINSEQ_3: 25;

          

           A32: (f /. k) = (f . k) by A22, A1, A29, A28, A30, FINSEQ_3: 25, PARTFUN1:def 6;

          

           A33: ( dom ls) = ( dom f) by A22, A1, A29, A28, FINSEQ_3: 29;

          then

           A34: (ls /. k) = (ls . k) by A30, FINSEQ_3: 25, PARTFUN1:def 6;

          consider b1,b2 be bag of n such that

           A35: (db /. k) = <*b1, b2*> and

           A36: (ls /. k) = ((pq . b1) * (r . b2)) by A23, A33, A31;

          

           A37: ( len <*b1, b2*>) = 2 by FINSEQ_1: 44;

          then 1 in ( dom <*b1, b2*>) by FINSEQ_3: 25;

          

          then

           A38: ((db /. k) /. 1) = ( <*b1, b2*> . 1) by A35, PARTFUN1:def 6

          .= b1 by FINSEQ_1: 44;

          set dblk = (dbl . k);

          set dbk2 = ((db /. k) /. 2);

          set ddbk1 = ( decomp ((db /. k) /. 1) qua Element of ( Bags n));

          

           A39: k in ( dom vdbl) by A22, A1, A28, A30, FINSEQ_3: 25;

          then

           A40: (dbl . k) = (ddbk1 ^^ (( len ddbk1) |-> <*dbk2*>)) by A2, A28;

          

          then

           A41: ( dom dblk) = (( dom ddbk1) /\ ( dom (( len ddbk1) |-> <*dbk2*>))) by PRE_POLY:def 4

          .= (( dom ddbk1) /\ ( Seg ( len ddbk1)))

          .= (( dom ddbk1) /\ ( dom ddbk1)) by FINSEQ_1:def 3

          .= ( dom ddbk1);

          set vdblk = (v * (dbl . k));

          k in ( dom dbl) by A22, A1, A30, FINSEQ_3: 25;

          then dblk in ( rng dbl) by FUNCT_1:def 3;

          then dblk is Element of ((3 -tuples_on ( Bags n)) * );

          then

          reconsider dblk as FinSequence of (3 -tuples_on ( Bags n));

          ( rng dblk) c= (3 -tuples_on ( Bags n));

          then

           A42: ( dom vdblk) = ( dom dblk) by A27, RELAT_1: 27;

          then

           A43: ( dom vdblk) = ( Seg ( len ddbk1)) by A41, FINSEQ_1:def 3;

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

          consider pqs be FinSequence of the carrier of L such that

           A44: (pq . b1) = ( Sum pqs) and

           A45: ( len pqs) = ( len ( decomp b1)) and

           A46: for i be Element of NAT st i in ( dom pqs) holds ex b11,b12 be bag of n st (( decomp b1) /. i) = <*b11, b12*> & (pqs /. i) = ((p . b11) * (q . b12)) by Def10;

          

           A47: ( dom pqs) = ( dom (pqs * (r . b2))) by Def2;

          2 in ( dom <*b1, b2*>) by A37, FINSEQ_3: 25;

          

          then

           A48: dbk2 = ( <*b1, b2*> . 2) by A35, PARTFUN1:def 6

          .= b2 by FINSEQ_1: 44;

          reconsider vdblk as FinSequence by A43, FINSEQ_1:def 2;

          

           A49: ( Sum (pqs * (r . b2))) = (( Sum pqs) * (r . b2)) by Th13;

          

           A50: ( dom ddbk1) = ( Seg ( len ddbk1)) by FINSEQ_1:def 3;

          now

            

             A51: ( dom pqs) = ( dom (pqs * (r . b2))) by Def2;

            

            thus ( len vdblk) = ( len pqs) by A45, A38, A41, A42, FINSEQ_3: 29

            .= ( len (pqs * (r . b2))) by A47, FINSEQ_3: 29;

            then

             A52: ( dom vdblk) = ( dom (pqs * (r . b2))) by FINSEQ_3: 29;

            let i be Nat;

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

            assume

             A53: 1 <= i & i <= ( len (pqs * (r . b2)));

            then

             A54: i in ( dom (pqs * (r . b2))) by FINSEQ_3: 25;

            then

            consider b11,b12 be bag of n such that

             A55: (( decomp b1) /. i) = <*b11, b12*> and

             A56: (pqs /. i) = ((p . b11) * (q . b12)) by A46, A47;

            ((( len ddbk1) |-> <*dbk2*>) . i9) = <*dbk2*> & (( decomp b1) /. i) = (( decomp b1) . i) by A38, A41, A50, A42, A52, A54, FUNCOP_1: 7, PARTFUN1:def 6;

            

            then

             A57: (dblk . i) = ( <*b11, b12*> ^ <*b2*>) by A48, A38, A40, A42, A52, A54, A55, PRE_POLY:def 4

            .= <*b11, b12, b2*> by FINSEQ_1: 43;

            reconsider b119 = b11, b129 = b12 as Element of ( Bags n) by PRE_POLY:def 12;

            reconsider B = <*b119, b129, b29*> as Element of (3 -tuples_on ( Bags n)) by FINSEQ_2: 104;

            

             A58: i in ( dom pqs) by A47, A53, FINSEQ_3: 25;

            

            thus ((v * (dbl . k)) . i) = (v . (dblk . i)) by A52, A54, FUNCT_1: 12

            .= (((p . (B /. 1)) * (q . (B /. 2))) * (r . (B /. 3))) by A11, A57

            .= (((p . b119) * (q . (B /. 2))) * (r . (B /. 3))) by FINSEQ_4: 18

            .= (((p . b11) * (q . b12)) * (r . (B /. 3))) by FINSEQ_4: 18

            .= ((pqs /. i) * (r . b2)) by A56, FINSEQ_4: 18

            .= ((pqs * (r . b2)) /. i) by A58, Def2

            .= ((pqs * (r . b2)) . i) by A58, A51, PARTFUN1:def 6;

          end;

          then

           A59: vdblk = (pqs * (r . b2)) by FINSEQ_1: 14;

          (vdbl /. k) = (vdbl . k) by A39, PARTFUN1:def 6

          .= (((( dom dbl) --> v) . k) * (dbl . k)) by A25, A39, PBOOLE:def 19

          .= (pqs * (r . b2)) by A28, A39, A59, FUNCOP_1: 7;

          hence (( Sum vdbl) . k) = (ls . k) by A31, A36, A44, A49, A34, A32, MATRLIN:def 6;

        end;

        then

         A60: ( Sum vdbl) = ls by FINSEQ_1: 14;

        consider vdbr be FinSequence of (cL * ) such that

         A61: vdbr = ((( dom dbr) --> v) ** dbr) and

         A62: vfdbr = ( FlattenSeq vdbr) by PRE_POLY: 32;

        

         A63: ( Sum vfdbr) = ( Sum ( Sum vdbr)) by A62, Th14;

        consider rs be FinSequence of cL such that

         A64: (pqrb . b) = ( Sum rs) and

         A65: ( len rs) = ( len ( decomp b)) and

         A66: for k be Element of NAT st k in ( dom rs) holds ex b1,b2 be bag of n st (db /. k) = <*b1, b2*> & (rs /. k) = ((p . b1) * (qr . b2)) by Def10;

        now

          set f = ( Sum vdbr);

          

           A67: ( dom vdbr) = (( dom (( dom dbr) --> v)) /\ ( dom dbr)) by A61, PBOOLE:def 19

          .= (( dom dbr) /\ ( dom dbr))

          .= ( dom dbr);

          

           A68: ( dom f) = ( dom vdbr) by Th2;

          hence ( len ( Sum vdbr)) = ( len rs) by A65, A12, A67, FINSEQ_3: 29;

          let k be Nat such that

           A69: 1 <= k & k <= ( len rs);

          

           A70: k in ( dom f) by A65, A12, A68, A67, A69, FINSEQ_3: 25;

          then

           A71: (f /. k) = (f . k) by PARTFUN1:def 6;

          set dbrk = (dbr . k);

          set dbk2 = ((db /. k) /. 1);

          set ddbk1 = ( decomp ((db /. k) /. 2) qua Element of ( Bags n));

          

           A72: k in ( dom vdbr) by A65, A12, A67, A69, FINSEQ_3: 25;

          then

           A73: (dbr . k) = ((( len ddbk1) |-> <*dbk2*>) ^^ ddbk1) by A13, A67;

          

          then

           A74: ( dom dbrk) = (( dom ddbk1) /\ ( dom (( len ddbk1) |-> <*dbk2*>))) by PRE_POLY:def 4

          .= (( dom ddbk1) /\ ( Seg ( len ddbk1)))

          .= (( dom ddbk1) /\ ( dom ddbk1)) by FINSEQ_1:def 3

          .= ( dom ddbk1);

          k in ( dom dbr) by A65, A12, A69, FINSEQ_3: 25;

          then dbrk in ( rng dbr) by FUNCT_1:def 3;

          then

           A75: dbrk is Element of ((3 -tuples_on ( Bags n)) * );

          set vdbrk = (v * (dbr . k));

          

           A76: ( dom ddbk1) = ( Seg ( len ddbk1)) by FINSEQ_1:def 3;

          reconsider dbrk as FinSequence of (3 -tuples_on ( Bags n)) by A75;

          ( rng dbrk) c= (3 -tuples_on ( Bags n));

          then

           A77: ( dom vdbrk) = ( dom dbrk) by A27, RELAT_1: 27;

          then

           A78: ( dom vdbrk) = ( Seg ( len ddbk1)) by A74, FINSEQ_1:def 3;

          

           A79: ( dom rs) = ( dom f) by A65, A12, A68, A67, FINSEQ_3: 29;

          then

           A80: (rs /. k) = (rs . k) by A70, PARTFUN1:def 6;

          consider b1,b2 be bag of n such that

           A81: (db /. k) = <*b1, b2*> and

           A82: (rs /. k) = ((p . b1) * (qr . b2)) by A66, A79, A70;

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

          consider qrs be FinSequence of the carrier of L such that

           A83: (qr . b2) = ( Sum qrs) and

           A84: ( len qrs) = ( len ( decomp b2)) and

           A85: for i be Element of NAT st i in ( dom qrs) holds ex b11,b12 be bag of n st (( decomp b2) /. i) = <*b11, b12*> & (qrs /. i) = ((q . b11) * (r . b12)) by Def10;

          

           A86: ( dom qrs) = ( dom ((p . b1) * qrs)) by Def1;

          then

           A87: ( len qrs) = ( len ((p . b1) * qrs)) by FINSEQ_3: 29;

          

           A88: ( len <*b1, b2*>) = 2 by FINSEQ_1: 44;

          then 1 in ( dom <*b1, b2*>) by FINSEQ_3: 25;

          

          then

           A89: dbk2 = ( <*b1, b2*> . 1) by A81, PARTFUN1:def 6

          .= b1 by FINSEQ_1: 44;

          reconsider vdbrk as FinSequence by A78, FINSEQ_1:def 2;

          

           A90: ( Sum ((p . b1) * qrs)) = ((p . b1) * ( Sum qrs)) by Th12;

          2 in ( dom <*b1, b2*>) by A88, FINSEQ_3: 25;

          

          then

           A91: ((db /. k) /. 2) = ( <*b1, b2*> . 2) by A81, PARTFUN1:def 6

          .= b2 by FINSEQ_1: 44;

          then

           A92: ( dom vdbrk) = ( dom ((p . b1) * qrs)) by A84, A74, A77, A86, FINSEQ_3: 29;

           A93:

          now

            let i be Nat;

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

            assume

             A94: 1 <= i & i <= ( len ((p . b1) * qrs));

            then

             A95: i in ( dom qrs) by A86, FINSEQ_3: 25;

            

             A96: i in ( dom dbrk) by A84, A91, A74, A87, A94, FINSEQ_3: 25;

            then

            consider b11,b12 be bag of n such that

             A97: (( decomp b2) /. i) = <*b11, b12*> and

             A98: (qrs /. i) = ((q . b11) * (r . b12)) by A85, A77, A86, A92;

            ((( len ddbk1) |-> <*dbk2*>) . i9) = <*dbk2*> & (( decomp b2) /. i) = (( decomp b2) . i) by A91, A74, A76, A96, FUNCOP_1: 7, PARTFUN1:def 6;

            

            then

             A99: (dbrk . i) = ( <*b1*> ^ <*b11, b12*>) by A89, A91, A73, A96, A97, PRE_POLY:def 4

            .= <*b1, b11, b12*> by FINSEQ_1: 43;

            reconsider b119 = b11, b129 = b12 as Element of ( Bags n) by PRE_POLY:def 12;

            reconsider B = <*b19, b119, b129*> as Element of (3 -tuples_on ( Bags n)) by FINSEQ_2: 104;

            

            thus ((v * (dbr . k)) . i) = (v . (dbrk . i)) by A77, A96, FUNCT_1: 12

            .= (((p . (B /. 1)) * (q . (B /. 2))) * (r . (B /. 3))) by A11, A99

            .= (((p . b1) * (q . (B /. 2))) * (r . (B /. 3))) by FINSEQ_4: 18

            .= (((p . b1) * (q . b11)) * (r . (B /. 3))) by FINSEQ_4: 18

            .= (((p . b1) * (q . b11)) * (r . b12)) by FINSEQ_4: 18

            .= ((p . b1) * (qrs /. i)) by A98, GROUP_1:def 3

            .= (((p . b1) * qrs) /. i) by A95, Def1

            .= (((p . b1) * qrs) . i) by A86, A95, PARTFUN1:def 6;

          end;

          ( len vdbrk) = ( len ((p . b1) * qrs)) by A84, A91, A74, A77, A87, FINSEQ_3: 29;

          then

           A100: vdbrk = ((p . b1) * qrs) by A93, FINSEQ_1: 14;

          (vdbr /. k) = (vdbr . k) by A72, PARTFUN1:def 6

          .= (((( dom dbr) --> v) . k) * (dbr . k)) by A61, A72, PBOOLE:def 19

          .= ((p . b1) * qrs) by A67, A72, A100, FUNCOP_1: 7;

          hence (( Sum vdbr) . k) = (rs . k) by A70, A82, A83, A90, A80, A71, MATRLIN:def 6;

        end;

        then

         A101: ( Sum vdbr) = rs by FINSEQ_1: 14;

        ( dom dbl) = ( dom db) by A1, FINSEQ_3: 29;

        then

        consider P be Permutation of ( dom fdbl) such that

         A102: fdbr = (fdbl * P) by A2, A13, A24, PRE_POLY: 74;

        ( rng fdbl) c= (3 -tuples_on ( Bags n));

        then ( dom vfdbl) = ( dom fdbl) by A27, RELAT_1: 27;

        then

        reconsider P as Permutation of ( dom vfdbl);

        

         A103: vfdbr = (vfdbl * P) by A102, RELAT_1: 36;

        ( Sum vfdbl) = ( Sum ( Sum vdbl)) by A26, Th14;

        hence (pqra . b) = (pqrb . b) by A21, A64, A60, A63, A101, A103, RLVECT_2: 7;

      end;

      hence thesis;

    end;

    definition

      let n be Ordinal, L be Abelian add-associative right_zeroed right_complementable commutative non empty doubleLoopStr, p,q be Series of n, L;

      :: original: *'

      redefine

      func p *' q;

      commutativity

      proof

        let p,q be Series of n, L;

        reconsider pq = (p *' q), qp = (q *' p) as Function of ( Bags n), the carrier of L;

        now

          let b be Element of ( Bags n);

          defpred P[ object, object] means ex b1,b2 be bag of n st (( decomp b) . $1) = <*b1, b2*> & (( decomp b) . $2) = <*b2, b1*>;

          consider s be FinSequence of the carrier of L such that

           A1: (pq . b) = ( Sum s) and

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

           A3: 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) * (q . b2)) by Def10;

          

           A4: ( dom s) = ( dom ( decomp b)) by A2, FINSEQ_3: 29;

          then

          reconsider ds = ( dom s) as non empty set;

           A5:

          now

            let e be object;

            assume

             A6: e in ds;

            then

            consider b1,b2 be bag of n such that

             A7: (( decomp b) /. e) = <*b1, b2*> and

             A8: b = (b1 + b2) by A4, PRE_POLY: 68;

            consider d be Element of NAT such that

             A9: d in ( dom ( decomp b)) and

             A10: (( decomp b) /. d) = <*b2, b1*> by A8, PRE_POLY: 69;

            reconsider d as object;

            take d;

            thus d in ds by A2, A9, FINSEQ_3: 29;

            thus P[e, d]

            proof

              take b1, b2;

              thus thesis by A4, A6, A7, A9, A10, PARTFUN1:def 6;

            end;

          end;

          consider f be Function of ds, ds such that

           A11: for e be object st e in ds holds P[e, (f . e)] from FUNCT_2:sch 1( A5);

          

           A12: ( dom f) = ds by FUNCT_2:def 1;

          ds c= ( rng f)

          proof

            let x be object;

            assume

             A13: x in ds;

            then

            consider b1,b2 be bag of n such that

             A14: (( decomp b) . x) = <*b1, b2*> and

             A15: (( decomp b) . (f . x)) = <*b2, b1*> by A11;

            

             A16: (f . x) in ( rng f) by A12, A13, FUNCT_1:def 3;

            then

             A17: (f . (f . x)) in ( rng f) by A12, FUNCT_1:def 3;

            consider b3,b4 be bag of n such that

             A18: (( decomp b) . (f . x)) = <*b3, b4*> and

             A19: (( decomp b) . (f . (f . x))) = <*b4, b3*> by A11, A16;

            b3 = b2 & b4 = b1 by A15, A18, FINSEQ_1: 77;

            hence thesis by A4, A13, A17, A14, A19, FUNCT_1:def 4;

          end;

          then

           A20: ( rng f) = ds;

          f is one-to-one

          proof

            let x1,x2 be object such that

             A21: x1 in ( dom f) and

             A22: x2 in ( dom f) and

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

            consider b3,b4 be bag of n such that

             A24: (( decomp b) . x2) = <*b3, b4*> and

             A25: (( decomp b) . (f . x2)) = <*b4, b3*> by A11, A22;

            consider b1,b2 be bag of n such that

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

             A27: (( decomp b) . (f . x1)) = <*b2, b1*> by A11, A21;

            b2 = b4 & b1 = b3 by A23, A27, A25, FINSEQ_1: 77;

            hence thesis by A4, A21, A22, A26, A24, FUNCT_1:def 4;

          end;

          then

          reconsider f as Permutation of ( dom s) by A20, FUNCT_2: 57;

          consider t be FinSequence of the carrier of L such that

           A28: (qp . b) = ( Sum t) and

           A29: ( len t) = ( len ( decomp b)) and

           A30: for k be Element of NAT st k in ( dom t) holds ex b1,b2 be bag of n st (( decomp b) /. k) = <*b1, b2*> & (t /. k) = ((q . b1) * (p . b2)) by Def10;

          

           A31: ( dom t) = ( dom ( decomp b)) by A29, FINSEQ_3: 29;

          now

            let i be Nat;

            reconsider fi = (f . i) as Element of NAT ;

            

             A32: ( dom s) = ( dom ( decomp b)) by A2, FINSEQ_3: 29;

            assume

             A33: i in ( dom t);

            then

            consider b1,b2 be bag of n such that

             A34: (( decomp b) /. i) = <*b1, b2*> and

             A35: (t /. i) = ((q . b1) * (p . b2)) by A30;

            

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

            consider b5,b6 be bag of n such that

             A37: (( decomp b) . i) = <*b5, b6*> and

             A38: (( decomp b) . (f . i)) = <*b6, b5*> by A4, A31, A11, A33;

            ( dom s) = ( dom t) by A2, A29, FINSEQ_3: 29;

            then (( decomp b) /. i) = (( decomp b) . i) by A33, A32, PARTFUN1:def 6;

            then

             A39: b1 = b5 & b2 = b6 by A34, A37, FINSEQ_1: 77;

            

             A40: (f . i) in ( rng f) by A4, A31, A12, A33, FUNCT_1:def 3;

            then

             A41: (s /. fi) = (s . fi) by PARTFUN1:def 6;

            consider b3,b4 be bag of n such that

             A42: (( decomp b) /. fi) = <*b3, b4*> and

             A43: (s /. fi) = ((p . b3) * (q . b4)) by A3, A40;

            

             A44: (( decomp b) /. fi) = (( decomp b) . fi) by A40, A32, PARTFUN1:def 6;

            then b3 = b6 by A42, A38, FINSEQ_1: 77;

            hence (t . i) = (s . (f . i)) by A35, A42, A43, A38, A36, A41, A44, A39, FINSEQ_1: 77;

          end;

          hence (pq . b) = (qp . b) by A1, A2, A28, A29, RLVECT_2: 6;

        end;

        hence (p *' q) = (q *' p);

      end;

    end

    theorem :: POLYNOM1:28

    for n be Ordinal, L be add-associative right_complementable right_zeroed right_unital distributive non empty doubleLoopStr, p be Series of n, L holds (p *' ( 0_ (n,L))) = ( 0_ (n,L))

    proof

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

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

      now

        let b be Element of ( Bags n);

        consider s be FinSequence of the carrier of L such that

         A1: ((p *' Z) . b) = ( Sum s) and ( len s) = ( len ( decomp b)) and

         A2: 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) * (Z . b2)) by Def10;

        now

          let k be Nat;

          assume k in ( dom s);

          then

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

           A3: (s /. k) = ((p . b1) * (Z . b2)) by A2;

          

          thus (s /. k) = ((p . b1) * ( 0. L)) by A3, Th22

          .= ( 0. L);

        end;

        then ( Sum s) = ( 0. L) by MATRLIN: 11;

        hence ((p *' Z) . b) = (Z . b) by A1;

      end;

      hence thesis;

    end;

    theorem :: POLYNOM1:29

    

     Th29: for n be Ordinal, L be add-associative right_complementable right_zeroed distributive right_unital non trivial non empty doubleLoopStr, p be Series of n, L holds (p *' ( 1_ (n,L))) = p

    proof

      let n be Ordinal, L be add-associative right_complementable right_zeroed distributive right_unital non trivial doubleLoopStr, p be Series of n, L;

      set O = ( 1_ (n,L)), cL = the carrier of L;

      now

        let b be Element of ( Bags n);

        consider s be FinSequence of cL such that

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

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

         A3: 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 Def10;

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

         A4: s = (t ^ <*s1*>) by A2, FINSEQ_2: 19;

         A5:

        now

          per cases ;

            suppose t = ( <*> cL);

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

          end;

            suppose

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

            now

              let k be Nat;

              

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

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

              assume

               A8: k in ( dom t);

              

              then

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

              .= (s . k) by A4, A8, FINSEQ_1:def 7;

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

              then

               A10: k < ( len s) by A7, NAT_1: 13;

              

               A11: 1 <= k by A8, FINSEQ_3: 25;

              then

               A12: k in ( dom ( decomp b)) by A2, A10, FINSEQ_3: 25;

              

               A13: ( dom s) = ( dom ( decomp b)) by A2, FINSEQ_3: 29;

              then

               A14: (s /. k) = (s . k) by A12, PARTFUN1:def 6;

              per cases by A11, XXREAL_0: 1;

                suppose

                 A15: 1 < k;

                consider b1,b2 be bag of n such that

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

                 A17: (s /. k) = ((p . b1) * (O . b2)) by A3, A13, A12;

                b2 <> ( EmptyBag n) by A2, A10, A15, A16, PRE_POLY: 72;

                

                hence (t /. k) = ((p . b1) * ( 0. L)) by A9, A14, A17, Th25

                .= ( 0. L);

              end;

                suppose

                 A18: k = 1;

                 A19:

                now

                  assume b = ( EmptyBag n);

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

                  then (( len t) + 1) = ( 0 qua Nat + 1) by A2, A7, FINSEQ_1: 39;

                  hence contradiction by A6;

                end;

                consider b1,b2 be bag of n such that

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

                 A21: (s /. k) = ((p . b1) * (O . b2)) by A3, A13, A12;

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

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

                

                then (s . k) = ((p . ( EmptyBag n)) * ( 0. L)) by A14, A21, A19, Th25

                .= ( 0. L);

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

              end;

            end;

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

          end;

        end;

        

         A22: (s . ( len s)) = ((t ^ <*s1*>) . (( len t) + 1)) by A4, FINSEQ_2: 16

        .= s1 by FINSEQ_1: 42;

        

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

        s is non empty by A2;

        then

         A24: ( len s) in ( dom s) by FINSEQ_5: 6;

        then

        consider b1,b2 be bag of n such that

         A25: (( decomp b) /. ( len s)) = <*b1, b2*> and

         A26: (s /. ( len s)) = ((p . b1) * (O . b2)) by A3;

        

         A27: (s /. ( len s)) = (s . ( len s)) by A24, PARTFUN1:def 6;

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

        then

         A28: b1 = b & b2 = ( EmptyBag n) by A25, FINSEQ_1: 77;

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

        .= ((p . b) * ( 1. L)) by A26, A28, A22, A27, Th25

        .= (p . b);

        hence ((p *' O) . b) = (p . b) by A1, A23, A5, RLVECT_1: 4;

      end;

      hence thesis;

    end;

    theorem :: POLYNOM1:30

    

     Th30: for n be Ordinal, L be add-associative right_complementable right_zeroed distributive well-unital non trivial non empty doubleLoopStr, p be Series of n, L holds (( 1_ (n,L)) *' p) = p

    proof

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

      set O = ( 1_ (n,L)), cL = the carrier of L;

      now

        let b be Element of ( Bags n);

        consider s be FinSequence of cL such that

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

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

         A3: 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 Def10;

        s is non empty by A2;

        then

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

         A4: s1 = (s . 1) and

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

        

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

         A7:

        now

          per cases ;

            suppose t = ( <*> cL);

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

          end;

            suppose

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

            now

              let k be Nat;

              

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

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

              assume

               A10: k in ( dom t);

              

              then

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

              .= (s . (k + 1)) by A5, A10, FINSEQ_3: 103;

              1 <= k by A10, FINSEQ_3: 25;

              then

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

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

              then

               A13: (k + 1) <= ( len s) by A9, XREAL_1: 6;

              then

               A14: (k + 1) in ( dom ( decomp b)) by A2, A12, FINSEQ_3: 25;

              

               A15: ( dom s) = ( dom ( decomp b)) by A2, FINSEQ_3: 29;

              then

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

              per cases by A13, XXREAL_0: 1;

                suppose

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

                consider b1,b2 be bag of n such that

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

                 A19: (s /. (k + 1)) = ((O . b1) * (p . b2)) by A3, A15, A14;

                b1 <> ( EmptyBag n) by A2, A12, A17, A18, PRE_POLY: 72;

                

                hence (t /. k) = (( 0. L) * (p . b2)) by A11, A16, A19, Th25

                .= ( 0. L);

              end;

                suppose

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

                 A21:

                now

                  assume b = ( EmptyBag n);

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

                  then (( len t) + 1) = ( 0 qua Nat + 1) by A2, A9, FINSEQ_1: 39;

                  hence contradiction by A8;

                end;

                consider b1,b2 be bag of n such that

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

                 A23: (s /. (k + 1)) = ((O . b1) * (p . b2)) by A3, A15, A14;

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

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

                

                then (s . (k + 1)) = (( 0. L) * (p . ( EmptyBag n))) by A16, A23, A21, Th25

                .= ( 0. L);

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

              end;

            end;

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

          end;

        end;

        

         A24: s is non empty by A2;

        then

        consider b1,b2 be bag of n such that

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

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

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

        then

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

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

        then

         A28: b2 = b & b1 = ( EmptyBag n) by A25, FINSEQ_1: 77;

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

        .= (( 1. L) * (p . b)) by A4, A26, A28, A27, Th25

        .= (p . b);

        hence ((O *' p) . b) = (p . b) by A1, A6, A7, RLVECT_1: 4;

      end;

      hence thesis;

    end;

    begin

    registration

      let n be set, S be non empty ZeroStr;

      cluster finite-Support for Series of n, S;

      existence

      proof

        reconsider P = (( Bags n) --> ( 0. S)) as Function of ( Bags n), the carrier of S;

        reconsider P as Function of ( Bags n), S;

        reconsider P as Series of n, S;

        take P;

        for x be Element of ( Bags n) holds x in {} iff (P . x) <> ( 0. S);

        then ( Support P) = ( {} ( Bags n)) by Def4;

        hence ( Support P) is finite;

      end;

    end

    definition

      let n be Ordinal, S be non empty ZeroStr;

      mode Polynomial of n,S is finite-Support Series of n, S;

    end

    registration

      let n be Ordinal, L be right_zeroed non empty addLoopStr, p,q be Polynomial of n, L;

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

      coherence

      proof

        set Sp = ( Support p), Sq = ( Support q);

        ( Support p) is finite & ( Support q) is finite by Def5;

        then (Sp \/ Sq) is finite;

        then ( Support (p + q)) is finite by Th20, FINSET_1: 1;

        hence thesis;

      end;

    end

    registration

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

      cluster ( - p) -> finite-Support;

      coherence

      proof

        set f = ( - p);

        

         A1: ( Support f) c= ( Support p)

        proof

          let x be object;

          assume

           A2: x in ( Support f);

          then

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

          (f . x9) <> ( 0. L) by A2, Def4;

          then ( - (p . x9)) <> ( 0. L) by Th17;

          then (p . x9) <> ( 0. L) by RLVECT_1: 12;

          hence thesis by Def4;

        end;

        ( Support p) is finite by Def5;

        hence thesis by A1;

      end;

    end

    registration

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

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

      coherence ;

    end

    registration

      let n be Ordinal, S be non empty ZeroStr;

      cluster ( 0_ (n,S)) -> finite-Support;

      coherence

      proof

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

        now

          given x be object such that

           A1: x in ( Support Z);

          reconsider x as Element of ( Bags n) by A1;

          (Z . x) = ( 0. S);

          hence contradiction by A1, Def4;

        end;

        then ( Support Z) = {} by XBOOLE_0:def 1;

        hence thesis;

      end;

    end

    registration

      let n be Ordinal, L be add-associative right_zeroed right_complementable right_unital right-distributive non trivial doubleLoopStr;

      cluster ( 1_ (n,L)) -> finite-Support;

      coherence

      proof

        reconsider O = (( 0_ (n,L)) +* (( EmptyBag n),( 1. L))) as Function of ( Bags n), the carrier of L;

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

        reconsider O9 as Series of n, L;

        now

          let x be object;

          hereby

            assume

             A1: x in ( Support O9);

            then

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

            assume x <> ( EmptyBag n);

            

            then (O9 . x) = (( 0_ (n,L)) . x9) by FUNCT_7: 32

            .= ( 0. L);

            hence contradiction by A1, Def4;

          end;

          assume

           A2: x = ( EmptyBag n);

          ( dom ( 0_ (n,L))) = ( Bags n);

          then (O9 . x) <> ( 0. L) by A2, FUNCT_7: 31;

          hence x in ( Support O9) by A2, Def4;

        end;

        then ( Support O9) = {( EmptyBag n)} by TARSKI:def 1;

        hence thesis;

      end;

    end

    registration

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

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

      coherence

      proof

        deffunc F( Element of ( Bags n), Element of ( Bags n)) = ($1 + $2);

        set D = { F(b1,b2) where b1,b2 be Element of ( Bags n) : b1 in ( Support p) & b2 in ( Support q) };

        

         A1: ( Support q) is finite by Def5;

        

         A2: ( Support (p *' q)) c= D

        proof

          let x9 be object;

          assume

           A3: x9 in ( Support (p *' q));

          then

          reconsider b = x9 as Element of ( Bags n);

          consider s be FinSequence of the carrier of L such that

           A4: ((p *' q) . b) = ( Sum s) and

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

           A6: 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) * (q . b2)) by Def10;

          ((p *' q) . b) <> ( 0. L) by A3, Def4;

          then

          consider k be Nat such that

           A7: k in ( dom s) and

           A8: (s /. k) <> ( 0. L) by A4, MATRLIN: 11;

          consider b1,b2 be bag of n such that

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

           A10: (s /. k) = ((p . b1) * (q . b2)) by A6, A7;

          

           A11: b1 in ( Bags n) by PRE_POLY:def 12;

          

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

          (q . b2) <> ( 0. L) by A8, A10;

          then

           A13: b2 in ( Support q) by A12, Def4;

          (p . b1) <> ( 0. L) by A8, A10;

          then

           A14: b1 in ( Support p) by A11, Def4;

          k in ( dom ( decomp b)) by A5, A7, FINSEQ_3: 29;

          then

          consider b19,b29 be bag of n such that

           A15: (( decomp b) /. k) = <*b19, b29*> and

           A16: b = (b19 + b29) by PRE_POLY: 68;

          b19 = b1 & b29 = b2 by A9, A15, FINSEQ_1: 77;

          hence thesis by A14, A13, A16;

        end;

        

         A17: ( Support p) is finite by Def5;

        D is finite from FRAENKEL:sch 22( A17, A1);

        hence thesis by A2;

      end;

    end

    begin

    definition

      let n be Ordinal, L be right_zeroed add-associative right_complementable right_unital distributive non trivial doubleLoopStr;

      :: POLYNOM1:def11

      func Polynom-Ring (n,L) -> strict non empty doubleLoopStr means

      : Def11: (for x be set holds x in the carrier of it iff x is Polynomial of n, L) & (for x,y be Element of it , p,q be Polynomial of n, L st x = p & y = q holds (x + y) = (p + q)) & (for x,y be Element of it , p,q be Polynomial of n, L st x = p & y = q holds (x * y) = (p *' q)) & ( 0. it ) = ( 0_ (n,L)) & ( 1. it ) = ( 1_ (n,L));

      existence

      proof

        reconsider Z = (( Bags n) --> ( 0. L)) as Function of ( Bags n), the carrier of L;

        defpred M[ set, set, set] means ex p,q,r be Polynomial of n, L st p = $1 & q = $2 & r = $3 & (p *' q) = r;

        defpred A[ set, set, set] means ex p,q,r be Polynomial of n, L st p = $1 & q = $2 & r = $3 & (p + q) = r;

        set x9 = the finite-Support Series of n, L;

        defpred Q[ set] means ex x9 be Series of n, L st x9 = $1 & x9 is finite-Support;

        consider P be Subset of ( Funcs (( Bags n),the carrier of L)) such that

         A1: for x be Element of ( Funcs (( Bags n),the carrier of L)) holds x in P iff Q[x] from SUBSET_1:sch 3;

        x9 in ( Funcs (( Bags n),the carrier of L)) by FUNCT_2: 8;

        then

        reconsider P as non empty Subset of ( Funcs (( Bags n),the carrier of L)) by A1;

         A2:

        now

          let x be Element of P, y be Element of P;

          reconsider p = x, q = y as Element of ( Funcs (( Bags n),the carrier of L));

          consider p9 be Series of n, L such that

           A3: p9 = p and

           A4: p9 is finite-Support by A1;

          consider q9 be Series of n, L such that

           A5: q9 = q and

           A6: q9 is finite-Support by A1;

          reconsider p9, q9 as Polynomial of n, L by A4, A6;

          set r = (p9 + q9);

          r in ( Funcs (( Bags n),the carrier of L)) by FUNCT_2: 8;

          then

          reconsider u = r as Element of P by A1;

          take u;

          thus A[x, y, u] by A3, A5;

        end;

        consider fadd be Function of [:P, P:], P such that

         A7: for x be Element of P, y be Element of P holds A[x, y, (fadd . (x,y))] from BINOP_1:sch 3( A2);

         A8:

        now

          let x be Element of P, y be Element of P;

          reconsider p = x, q = y as Element of ( Funcs (( Bags n),the carrier of L));

          consider p9 be Series of n, L such that

           A9: p9 = p and

           A10: p9 is finite-Support by A1;

          consider q9 be Series of n, L such that

           A11: q9 = q and

           A12: q9 is finite-Support by A1;

          reconsider p9, q9 as Polynomial of n, L by A10, A12;

          set r = (p9 *' q9);

          r in ( Funcs (( Bags n),the carrier of L)) by FUNCT_2: 8;

          then

          reconsider u = r as Element of P by A1;

          take u;

          thus M[x, y, u] by A9, A11;

        end;

        consider fmult be Function of [:P, P:], P such that

         A13: for x be Element of P, y be Element of P holds M[x, y, (fmult . (x,y))] from BINOP_1:sch 3( A8);

        reconsider ZZ = Z as Element of ( Funcs (( Bags n),the carrier of L)) by FUNCT_2: 8;

        reconsider Z9 = Z as Function of ( Bags n), L;

        reconsider Z9 as Series of n, L;

        now

          given x be object such that

           A14: x in ( Support Z9);

          reconsider x as Element of ( Bags n) by A14;

          (Z9 . x) = ( 0. L);

          hence contradiction by A14, Def4;

        end;

        then ( Support Z9) = {} by XBOOLE_0:def 1;

        then Z9 is finite-Support;

        then ZZ in P by A1;

        then

        reconsider Ze = Z as Element of P;

        reconsider O = (Z +* (( EmptyBag n),( 1. L))) as Function of ( Bags n), the carrier of L;

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

        reconsider O9 as Series of n, L;

        reconsider O as Element of ( Funcs (( Bags n),the carrier of L)) by FUNCT_2: 8;

        now

          let x be object;

          hereby

            assume

             A15: x in ( Support O9);

            then

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

            assume x <> ( EmptyBag n);

            

            then (O9 . x) = (Z . x9) by FUNCT_7: 32

            .= ( 0. L);

            hence contradiction by A15, Def4;

          end;

          assume

           A16: x = ( EmptyBag n);

          ( dom Z) = ( Bags n);

          then (O9 . x) <> ( 0. L) by A16, FUNCT_7: 31;

          hence x in ( Support O9) by A16, Def4;

        end;

        then ( Support O9) = {( EmptyBag n)} by TARSKI:def 1;

        then O9 is finite-Support;

        then

        reconsider O as Element of P by A1;

        reconsider R = doubleLoopStr (# P, fadd, fmult, O, Ze #) as strict non empty doubleLoopStr;

        take R;

        thus for x be set holds x in the carrier of R iff x is Polynomial of n, L

        proof

          let x be set;

          hereby

            assume

             A17: x in the carrier of R;

            then

            reconsider xx = x as Element of ( Funcs (( Bags n),the carrier of L));

            ex x9 be Series of n, L st x9 = xx & x9 is finite-Support by A1, A17;

            hence x is Polynomial of n, L;

          end;

          assume

           A18: x is Polynomial of n, L;

          then x is Element of ( Funcs (( Bags n),the carrier of L)) by FUNCT_2: 8;

          hence thesis by A1, A18;

        end;

        hereby

          let x,y be Element of R, p,q be Polynomial of n, L such that

           A19: x = p & y = q;

          ex p9,q9,r9 be Polynomial of n, L st p9 = x & q9 = y & r9 = (fadd . (x,y)) & (p9 + q9) = r9 by A7;

          hence (x + y) = (p + q) by A19;

        end;

        hereby

          let x,y be Element of R, p,q be Polynomial of n, L such that

           A20: x = p & y = q;

          ex p9,q9,r9 be Polynomial of n, L st p9 = x & q9 = y & r9 = (fmult . (x,y)) & (p9 *' q9) = r9 by A13;

          hence (x * y) = (p *' q) by A20;

        end;

        thus ( 0. R) = ( 0_ (n,L));

        thus thesis;

      end;

      uniqueness

      proof

        let it1,it2 be strict non empty doubleLoopStr such that

         A21: for x be set holds x in the carrier of it1 iff x is Polynomial of n, L and

         A22: for x,y be Element of it1, p,q be Polynomial of n, L st x = p & y = q holds (x + y) = (p + q) and

         A23: for x,y be Element of it1, p,q be Polynomial of n, L st x = p & y = q holds (x * y) = (p *' q) and

         A24: ( 0. it1) = ( 0_ (n,L)) & ( 1. it1) = ( 1_ (n,L)) and

         A25: for x be set holds x in the carrier of it2 iff x is Polynomial of n, L and

         A26: for x,y be Element of it2, p,q be Polynomial of n, L st x = p & y = q holds (x + y) = (p + q) and

         A27: for x,y be Element of it2, p,q be Polynomial of n, L st x = p & y = q holds (x * y) = (p *' q) and

         A28: ( 0. it2) = ( 0_ (n,L)) & ( 1. it2) = ( 1_ (n,L));

         A29:

        now

          let x be object;

          hereby

            assume x in the carrier of it1;

            then x is Polynomial of n, L by A21;

            hence x in the carrier of it2 by A25;

          end;

          assume x in the carrier of it2;

          then x is Polynomial of n, L by A25;

          hence x in the carrier of it1 by A21;

        end;

        then

         A30: the carrier of it1 = the carrier of it2 by TARSKI: 2;

         A31:

        now

          let a,b be Element of it1;

          reconsider a9 = a, b9 = b as Element of it2 by A29;

          reconsider a19 = a9, b19 = b9 as Element of it2;

          reconsider p = a, q = b as Polynomial of n, L by A21;

          reconsider a1 = a, b1 = b as Element of it1;

          

          thus (the multF of it1 . (a,b)) = (a1 * b1)

          .= (p *' q) by A23

          .= (a19 * b19) by A27

          .= (the multF of it2 . (a,b));

        end;

        now

          let a,b be Element of it1;

          reconsider a9 = a, b9 = b as Element of it2 by A29;

          reconsider a19 = a9, b19 = b9 as Element of it2;

          reconsider p = a, q = b as Polynomial of n, L by A21;

          reconsider a1 = a, b1 = b as Element of it1;

          

          thus (the addF of it1 . (a,b)) = (a1 + b1)

          .= (p + q) by A22

          .= (a19 + b19) by A26

          .= (the addF of it2 . (a,b));

        end;

        then the addF of it1 = the addF of it2 by A30, BINOP_1: 2;

        hence thesis by A24, A28, A30, A31, BINOP_1: 2;

      end;

    end

    registration

      let n be Ordinal, L be Abelian right_zeroed add-associative right_complementable right_unital distributive non trivial doubleLoopStr;

      cluster ( Polynom-Ring (n,L)) -> Abelian;

      coherence

      proof

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

        let v,w be Element of Pm;

        reconsider p = v, q = w as Polynomial of n, L by Def11;

        

        thus (v + w) = (q + p) by Def11

        .= (w + v) by Def11;

      end;

    end

    registration

      let n be Ordinal, L be add-associative right_zeroed right_complementable right_unital distributive non trivial doubleLoopStr;

      cluster ( Polynom-Ring (n,L)) -> add-associative;

      coherence

      proof

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

        let u,v,w be Element of Pm;

        reconsider o = u, p = v, q = w as Polynomial of n, L by Def11;

        

         A1: (v + w) = (p + q) by Def11;

        (u + v) = (o + p) by Def11;

        

        hence ((u + v) + w) = ((o + p) + q) by Def11

        .= (o + (p + q)) by Th21

        .= (u + (v + w)) by A1, Def11;

      end;

    end

    registration

      let n be Ordinal, L be right_zeroed add-associative right_complementable right_unital distributive non trivial doubleLoopStr;

      cluster ( Polynom-Ring (n,L)) -> right_zeroed;

      coherence

      proof

        let v be Element of ( Polynom-Ring (n,L));

        reconsider p = v as Polynomial of n, L by Def11;

        ( 0. ( Polynom-Ring (n,L))) = ( 0_ (n,L)) by Def11;

        

        hence (v + ( 0. ( Polynom-Ring (n,L)))) = (p + ( 0_ (n,L))) by Def11

        .= v by Th23;

      end;

    end

    registration

      let n be Ordinal, L be right_complementable right_zeroed add-associative right_unital distributive non trivial doubleLoopStr;

      cluster ( Polynom-Ring (n,L)) -> right_complementable;

      coherence

      proof

        let v be Element of ( Polynom-Ring (n,L));

        reconsider p = v as Polynomial of n, L by Def11;

        reconsider w = ( - p) as Element of ( Polynom-Ring (n,L)) by Def11;

        take w;

        

        thus (v + w) = (p - p) by Def11

        .= ( 0_ (n,L)) by Th24

        .= ( 0. ( Polynom-Ring (n,L))) by Def11;

      end;

    end

    registration

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

      cluster ( Polynom-Ring (n,L)) -> commutative;

      coherence

      proof

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

        let v,w be Element of Pm;

        reconsider p = v, q = w as Polynomial of n, L by Def11;

        

        thus (v * w) = (q *' p) by Def11

        .= (w * v) by Def11;

      end;

    end

    registration

      let n be Ordinal, L be Abelian add-associative right_zeroed right_complementable right_unital distributive associative non trivial non empty doubleLoopStr;

      cluster ( Polynom-Ring (n,L)) -> associative;

      coherence

      proof

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

        let x,y,z be Element of Pm;

        reconsider p = x, q = y, r = z as Polynomial of n, L by Def11;

        

         A1: (y * z) = (q *' r) by Def11;

        (x * y) = (p *' q) by Def11;

        

        hence ((x * y) * z) = ((p *' q) *' r) by Def11

        .= (p *' (q *' r)) by Th27

        .= (x * (y * z)) by A1, Def11;

      end;

    end

     Lm1:

    now

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

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

      let x,e be Element of Pm;

      reconsider p = x as Polynomial of n, L by Def11;

      assume

       A1: e = ( 1. Pm);

      

       A2: ( 1. Pm) = ( 1_ (n,L)) by Def11;

      

      hence (x * e) = (p *' ( 1_ (n,L))) by A1, Def11

      .= x by Th29;

      

      thus (e * x) = (( 1_ (n,L)) *' p) by A1, A2, Def11

      .= x by Th30;

    end;

    registration

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

      cluster ( Polynom-Ring (n,L)) -> well-unital right-distributive;

      coherence

      proof

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

        thus Pm is well-unital by Lm1;

        let x,y,z be Element of Pm;

        reconsider p = x, q = y, r = z as Polynomial of n, L by Def11;

        

         A1: (x * y) = (p *' q) & (x * z) = (p *' r) by Def11;

        (y + z) = (q + r) by Def11;

        

        hence (x * (y + z)) = (p *' (q + r)) by Def11

        .= ((p *' q) + (p *' r)) by Th26

        .= ((x * y) + (x * z)) by A1, Def11;

      end;

    end

    theorem :: POLYNOM1:31

    for n be Ordinal, L be right_zeroed Abelian add-associative right_complementable right_unital distributive associative non trivial non empty doubleLoopStr holds ( 1. ( Polynom-Ring (n,L))) = ( 1_ (n,L)) by Def11;