polyalg1.miz



    begin

    definition

      let F be 1-sorted;

      struct ( doubleLoopStr, ModuleStr over F) AlgebraStr over F (# the carrier -> set,

the addF, multF -> BinOp of the carrier,

the ZeroF, OneF -> Element of the carrier,

the lmult -> Function of [:the carrier of F, the carrier:], the carrier #)

       attr strict strict;

    end

    registration

      let L be non empty doubleLoopStr;

      cluster strict non empty for AlgebraStr over L;

      existence

      proof

         0 in { 0 } by TARSKI:def 1;

        then

        reconsider lm = ( [:the carrier of L, { 0 }:] --> 0 ) as Function of [:the carrier of L, { 0 }:], { 0 } by FUNCOP_1: 45;

        reconsider z = 0 as Element of { 0 } by TARSKI:def 1;

        set a = the BinOp of { 0 };

        take AlgebraStr (# { 0 }, a, a, z, z, lm #);

        thus thesis;

      end;

    end

    definition

      let L be non empty doubleLoopStr, A be non empty AlgebraStr over L;

      :: POLYALG1:def1

      attr A is mix-associative means for a be Element of L, x,y be Element of A holds (a * (x * y)) = ((a * x) * y);

    end

    registration

      let L be non empty doubleLoopStr;

      cluster unital distributive vector-distributive scalar-distributive scalar-associative scalar-unital mix-associative for non empty AlgebraStr over L;

      existence

      proof

         0 in { 0 } by TARSKI:def 1;

        then

        reconsider lm = ( [:the carrier of L, { 0 }:] --> 0 ) as Function of [:the carrier of L, { 0 }:], { 0 } by FUNCOP_1: 45;

        reconsider z = 0 as Element of { 0 } by TARSKI:def 1;

        set a = the BinOp of { 0 };

        reconsider A = AlgebraStr (# { 0 }, a, a, z, z, lm #) as non empty AlgebraStr over L;

        take A;

        

         A1: for x,y be Element of A holds x = y

        proof

          let x,y be Element of A;

          x = 0 by TARSKI:def 1;

          hence thesis by TARSKI:def 1;

        end;

        thus A is unital

        proof

          take ( 1. A);

          thus thesis by A1;

        end;

        thus A is distributive by A1;

        thus A is vector-distributive by A1;

        thus A is scalar-distributive by A1;

        thus A is scalar-associative by A1;

        thus A is scalar-unital by A1;

        thus A is mix-associative by A1;

      end;

    end

    definition

      let L be non empty doubleLoopStr;

      mode Algebra of L is unital distributive vector-distributive scalar-distributive scalar-associative scalar-unital mix-associative non empty AlgebraStr over L;

    end

    theorem :: POLYALG1:1

    

     Th1: for X,Y be set holds for f be Function of [:X, Y:], X holds ( dom f) = [:X, Y:]

    proof

      let X,Y be set;

      let f be Function of [:X, Y:], X;

      X is empty implies [:X, Y:] is empty by ZFMISC_1: 90;

      hence thesis by FUNCT_2:def 1;

    end;

    theorem :: POLYALG1:2

    

     Th2: for X,Y be set holds for f be Function of [:X, Y:], Y holds ( dom f) = [:X, Y:]

    proof

      let X,Y be set;

      let f be Function of [:X, Y:], Y;

      Y is empty implies [:X, Y:] is empty by ZFMISC_1: 90;

      hence thesis by FUNCT_2:def 1;

    end;

    begin

    definition

      let L be non empty doubleLoopStr;

      :: POLYALG1:def2

      func Formal-Series L -> strict non empty AlgebraStr over L means

      : Def2: (for x be set holds x in the carrier of it iff x is sequence of L) & (for x,y be Element of it , p,q be sequence of L st x = p & y = q holds (x + y) = (p + q)) & (for x,y be Element of it , p,q be sequence of L st x = p & y = q holds (x * y) = (p *' q)) & (for a be Element of L, x be Element of it , p be sequence of L st x = p holds (a * x) = (a * p)) & ( 0. it ) = ( 0_. L) & ( 1. it ) = ( 1_. L);

      existence

      proof

        

         A1: ( 0_. L) in the set of all x where x be sequence of L;

        then

        reconsider Ca = the set of all x where x be sequence of L as non empty set;

        reconsider Ze = ( 0_. L) as Element of Ca by A1;

        defpred P[ set, set, set] means ex p,q be sequence of L st p = $1 & q = $2 & $3 = (p + q);

        

         A2: for x,y be Element of Ca holds ex u be Element of Ca st P[x, y, u]

        proof

          let x,y be Element of Ca;

          x in Ca;

          then

          consider p be sequence of L such that

           A3: x = p;

          y in Ca;

          then

          consider q be sequence of L such that

           A4: y = q;

          (p + q) in Ca;

          then

          reconsider u = (p + q) as Element of Ca;

          take u, p, q;

          thus thesis by A3, A4;

        end;

        consider Ad be Function of [:Ca, Ca:], Ca such that

         A5: for x,y be Element of Ca holds P[x, y, (Ad . (x,y))] from BINOP_1:sch 3( A2);

        ( 1_. L) in the set of all x where x be sequence of L;

        then

        reconsider Un = ( 1_. L) as Element of Ca;

        defpred P[ set, set, set] means ex p,q be sequence of L st p = $1 & q = $2 & $3 = (p *' q);

        

         A6: for x,y be Element of Ca holds ex u be Element of Ca st P[x, y, u]

        proof

          let x,y be Element of Ca;

          x in Ca;

          then

          consider p be sequence of L such that

           A7: x = p;

          y in Ca;

          then

          consider q be sequence of L such that

           A8: y = q;

          (p *' q) in Ca;

          then

          reconsider u = (p *' q) as Element of Ca;

          take u, p, q;

          thus thesis by A7, A8;

        end;

        consider Mu be Function of [:Ca, Ca:], Ca such that

         A9: for x,y be Element of Ca holds P[x, y, (Mu . (x,y))] from BINOP_1:sch 3( A6);

        defpred P[ Element of L, set, set] means ex p be sequence of L st p = $2 & $3 = ($1 * p);

        

         A10: for a be Element of L, x be Element of Ca holds ex u be Element of Ca st P[a, x, u]

        proof

          let a be Element of L, x be Element of Ca;

          x in Ca;

          then

          consider q be sequence of L such that

           A11: x = q;

          (a * q) in Ca;

          then

          reconsider u = (a * q) as Element of Ca;

          take u, q;

          thus thesis by A11;

        end;

        consider lm be Function of [:the carrier of L, Ca:], Ca such that

         A12: for a be Element of L, x be Element of Ca holds P[a, x, (lm . (a,x))] from BINOP_1:sch 3( A10);

        reconsider P = AlgebraStr (# Ca, Ad, Mu, Ze, Un, lm #) as strict non empty AlgebraStr over L;

        take P;

        thus for x be set holds x in the carrier of P iff x is sequence of L

        proof

          let x be set;

          thus x in the carrier of P implies x is sequence of L

          proof

            assume x in the carrier of P;

            then ex p be sequence of L st x = p;

            hence thesis;

          end;

          thus thesis;

        end;

        thus for x,y be Element of P, p,q be sequence of L st x = p & y = q holds (x + y) = (p + q)

        proof

          let x,y be Element of P;

          let p,q be sequence of L;

          assume

           A13: x = p & y = q;

          ex p1,q1 be sequence of L st p1 = x & q1 = y & (Ad . (x,y)) = (p1 + q1) by A5;

          hence thesis by A13;

        end;

        thus for x,y be Element of P, p,q be sequence of L st x = p & y = q holds (x * y) = (p *' q)

        proof

          let x,y be Element of P;

          let p,q be sequence of L;

          assume

           A14: x = p & y = q;

          ex p1,q1 be sequence of L st p1 = x & q1 = y & (Mu . (x,y)) = (p1 *' q1) by A9;

          hence thesis by A14;

        end;

        thus for a be Element of L, x be Element of P, p be sequence of L st x = p holds (a * x) = (a * p)

        proof

          let a be Element of L, x be Element of P, p be sequence of L such that

           A15: x = p;

          ex p1 be sequence of L st x = p1 & (lm . (a,x)) = (a * p1) by A12;

          hence thesis by A15;

        end;

        thus ( 0. P) = ( 0_. L);

        thus thesis;

      end;

      uniqueness

      proof

        let P1,P2 be strict non empty AlgebraStr over L such that

         A16: for x be set holds x in the carrier of P1 iff x is sequence of L and

         A17: for x,y be Element of P1, p,q be sequence of L st x = p & y = q holds (x + y) = (p + q) and

         A18: for x,y be Element of P1, p,q be sequence of L st x = p & y = q holds (x * y) = (p *' q) and

         A19: for a be Element of L, x be Element of P1, p be sequence of L st x = p holds (a * x) = (a * p) and

         A20: ( 0. P1) = ( 0_. L) & ( 1. P1) = ( 1_. L) and

         A21: for x be set holds x in the carrier of P2 iff x is sequence of L and

         A22: for x,y be Element of P2, p,q be sequence of L st x = p & y = q holds (x + y) = (p + q) and

         A23: for x,y be Element of P2, p,q be sequence of L st x = p & y = q holds (x * y) = (p *' q) and

         A24: for a be Element of L, x be Element of P2, p be sequence of L st x = p holds (a * x) = (a * p) and

         A25: ( 0. P2) = ( 0_. L) & ( 1. P2) = ( 1_. L);

         A26:

        now

          let x be object;

          x in the carrier of P1 iff x is sequence of L by A16;

          hence x in the carrier of P1 iff x in the carrier of P2 by A21;

        end;

        then

         A27: the carrier of P1 = the carrier of P2 by TARSKI: 2;

        now

          let a be Element of L, x be Element of P1;

          reconsider p = x as sequence of L by A16;

          reconsider x1 = x as Element of P2 by A26;

          reconsider a1 = a as Element of L;

          

          thus (the lmult of P1 . (a,x)) = (a * x)

          .= (a1 * p) by A19

          .= (a1 * x1) by A24

          .= (the lmult of P2 . (a,x));

        end;

        then

         A28: the lmult of P1 = the lmult of P2 by A27, BINOP_1: 2;

         A29:

        now

          let x be Element of P1, y be Element of P2;

          reconsider y1 = y as Element of P1 by A26;

          reconsider x1 = x as Element of P2 by A26;

          reconsider p = x as sequence of L by A16;

          reconsider q = y as sequence of L by A21;

          

          thus (the multF of P1 . (x,y)) = (x * y1)

          .= (p *' q) by A18

          .= (x1 * y) by A23

          .= (the multF of P2 . (x,y));

        end;

        now

          let x be Element of P1, y be Element of P2;

          reconsider y1 = y as Element of P1 by A26;

          reconsider x1 = x as Element of P2 by A26;

          reconsider p = x as sequence of L by A16;

          reconsider q = y as sequence of L by A21;

          

          thus (the addF of P1 . (x,y)) = (x + y1)

          .= (p + q) by A17

          .= (x1 + y) by A22

          .= (the addF of P2 . (x,y));

        end;

        then the addF of P1 = the addF of P2 by A27, BINOP_1: 2;

        hence thesis by A20, A25, A27, A29, A28, BINOP_1: 2;

      end;

    end

    registration

      let L be Abelian non empty doubleLoopStr;

      cluster ( Formal-Series L) -> Abelian;

      coherence

      proof

        let p,q be Element of ( Formal-Series L);

        reconsider p1 = p, q1 = q as sequence of L by Def2;

        

        thus (p + q) = (p1 + q1) by Def2

        .= (q + p) by Def2;

      end;

    end

    registration

      let L be add-associative non empty doubleLoopStr;

      cluster ( Formal-Series L) -> add-associative;

      coherence

      proof

        let p,q,r be Element of ( Formal-Series L);

        reconsider p1 = p, q1 = q, r1 = r as sequence of L by Def2;

        

         A1: (q + r) = (q1 + r1) by Def2;

        (p + q) = (p1 + q1) by Def2;

        

        hence ((p + q) + r) = ((p1 + q1) + r1) by Def2

        .= (p1 + (q1 + r1)) by POLYNOM3: 26

        .= (p + (q + r)) by A1, Def2;

      end;

    end

    registration

      let L be right_zeroed non empty doubleLoopStr;

      cluster ( Formal-Series L) -> right_zeroed;

      coherence

      proof

        let p be Element of ( Formal-Series L);

        reconsider p1 = p as sequence of L by Def2;

        ( 0. ( Formal-Series L)) = ( 0_. L) by Def2;

        

        hence (p + ( 0. ( Formal-Series L))) = (p1 + ( 0_. L)) by Def2

        .= p by POLYNOM3: 28;

      end;

    end

    registration

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

      cluster ( Formal-Series L) -> right_complementable;

      coherence

      proof

        let p be Element of ( Formal-Series L);

        reconsider p1 = p as sequence of L by Def2;

        reconsider q = ( - p1) as Element of ( Formal-Series L) by Def2;

        take q;

        

        thus (p + q) = (p1 + ( - p1)) by Def2

        .= (p1 - p1) by POLYNOM3:def 6

        .= ( 0_. L) by POLYNOM3: 29

        .= ( 0. ( Formal-Series L)) by Def2;

      end;

    end

    registration

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

      cluster ( Formal-Series L) -> commutative;

      coherence

      proof

        let p,q be Element of ( Formal-Series L);

        reconsider p1 = p, q1 = q as sequence of L by Def2;

        

        thus (p * q) = (p1 *' q1) by Def2

        .= (q * p) by Def2;

      end;

    end

    registration

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

      cluster ( Formal-Series L) -> associative;

      coherence

      proof

        let p,q,r be Element of ( Formal-Series L);

        reconsider p1 = p, q1 = q, r1 = r as sequence of L by Def2;

        

         A1: (q * r) = (q1 *' r1) by Def2;

        (p * q) = (p1 *' q1) by Def2;

        

        hence ((p * q) * r) = ((p1 *' q1) *' r1) by Def2

        .= (p1 *' (q1 *' r1)) by POLYNOM3: 33

        .= (p * (q * r)) by A1, Def2;

      end;

    end

    registration

      cluster add-associative associative right_zeroed left_zeroed well-unital right_complementable distributive for non empty doubleLoopStr;

      existence

      proof

        take F_Real ;

        thus thesis;

      end;

    end

    ::$Canceled

     Lm1:

    now

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

      set F = ( Formal-Series L);

      let x,e be Element of F;

      reconsider a = x, b = e as sequence of L by Def2;

      assume

       A1: e = ( 1_. L);

      

      thus (x * e) = (a *' b) by Def2

      .= x by A1, POLYNOM3: 35;

      

      thus (e * x) = (b *' a) by Def2

      .= x by A1, POLYNOM3: 36;

    end;

    registration

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

      cluster ( Formal-Series L) -> well-unital;

      coherence

      proof

        let x be Element of ( Formal-Series L);

        set F = ( Formal-Series L);

        ( 1. F) = ( 1_. L) by Def2;

        hence thesis by Lm1;

      end;

    end

    registration

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

      cluster ( Formal-Series L) -> right-distributive;

      coherence

      proof

        let p,q,r be Element of ( Formal-Series L);

        reconsider p1 = p, q1 = q, r1 = r as sequence of L by Def2;

        

         A1: (p * q) = (p1 *' q1) & (p * r) = (p1 *' r1) by Def2;

        (q + r) = (q1 + r1) by Def2;

        

        hence (p * (q + r)) = (p1 *' (q1 + r1)) by Def2

        .= ((p1 *' q1) + (p1 *' r1)) by POLYNOM3: 31

        .= ((p * q) + (p * r)) by A1, Def2;

      end;

      cluster ( Formal-Series L) -> left-distributive;

      coherence

      proof

        let p,q,r be Element of ( Formal-Series L);

        reconsider p1 = p, q1 = q, r1 = r as sequence of L by Def2;

        

         A2: (q * p) = (q1 *' p1) & (r * p) = (r1 *' p1) by Def2;

        (q + r) = (q1 + r1) by Def2;

        

        hence ((q + r) * p) = ((q1 + r1) *' p1) by Def2

        .= ((q1 *' p1) + (r1 *' p1)) by POLYNOM3: 32

        .= ((q * p) + (r * p)) by A2, Def2;

      end;

    end

    theorem :: POLYALG1:6

    

     Th6: for L be Abelian add-associative right_zeroed right_complementable distributive non empty doubleLoopStr holds for a be Element of L, p,q be sequence of L holds (a * (p + q)) = ((a * p) + (a * q))

    proof

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

      let a be Element of L, p,q be sequence of L;

      for i be Element of NAT holds ((a * (p + q)) . i) = (((a * p) + (a * q)) . i)

      proof

        let i be Element of NAT ;

        (a * ((p + q) . i)) = (a * ((p . i) + (q . i))) by NORMSP_1:def 2

        .= ((a * (p . i)) + (a * (q . i))) by VECTSP_1:def 7

        .= (((a * p) . i) + (a * (q . i))) by POLYNOM5:def 4

        .= (((a * p) . i) + ((a * q) . i)) by POLYNOM5:def 4

        .= (((a * p) + (a * q)) . i) by NORMSP_1:def 2;

        hence thesis by POLYNOM5:def 4;

      end;

      hence thesis by FUNCT_2: 63;

    end;

    theorem :: POLYALG1:7

    

     Th7: for L be Abelian add-associative right_zeroed right_complementable distributive non empty doubleLoopStr holds for a,b be Element of L, p be sequence of L holds ((a + b) * p) = ((a * p) + (b * p))

    proof

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

      let a,b be Element of L, p be sequence of L;

      for i be Element of NAT holds (((a + b) * p) . i) = (((a * p) + (b * p)) . i)

      proof

        let i be Element of NAT ;

        

        thus (((a + b) * p) . i) = ((a + b) * (p . i)) by POLYNOM5:def 4

        .= ((a * (p . i)) + (b * (p . i))) by VECTSP_1:def 7

        .= (((a * p) . i) + (b * (p . i))) by POLYNOM5:def 4

        .= (((a * p) . i) + ((b * p) . i)) by POLYNOM5:def 4

        .= (((a * p) + (b * p)) . i) by NORMSP_1:def 2;

      end;

      hence thesis by FUNCT_2: 63;

    end;

    theorem :: POLYALG1:8

    

     Th8: for L be associative non empty doubleLoopStr holds for a,b be Element of L, p be sequence of L holds ((a * b) * p) = (a * (b * p))

    proof

      let L be associative non empty doubleLoopStr;

      let a,b be Element of L, p be sequence of L;

      for i be Element of NAT holds (((a * b) * p) . i) = ((a * (b * p)) . i)

      proof

        let i be Element of NAT ;

        

        thus (((a * b) * p) . i) = ((a * b) * (p . i)) by POLYNOM5:def 4

        .= (a * (b * (p . i))) by GROUP_1:def 3

        .= (a * ((b * p) . i)) by POLYNOM5:def 4

        .= ((a * (b * p)) . i) by POLYNOM5:def 4;

      end;

      hence thesis by FUNCT_2: 63;

    end;

    theorem :: POLYALG1:9

    

     Th9: for L be associative well-unital non empty doubleLoopStr holds for p be sequence of L holds (( 1. L) * p) = p

    proof

      let L be associative well-unital non empty doubleLoopStr;

      let p be sequence of L;

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

      proof

        let i be Element of NAT ;

        

        thus ((( 1. L) * p) . i) = (( 1. L) * (p . i)) by POLYNOM5:def 4

        .= (p . i);

      end;

      hence thesis by FUNCT_2: 63;

    end;

    registration

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

      cluster ( Formal-Series L) -> vector-distributive scalar-distributive scalar-associative scalar-unital;

      coherence

      proof

        set F = ( Formal-Series L);

        thus F is vector-distributive

        proof

          let x be Element of L;

          let v,w be Element of ( Formal-Series L);

          reconsider p = v, q = w as sequence of L by Def2;

          reconsider x9 = x as Element of L;

          reconsider k = (v + w) as Element of ( Formal-Series L);

          

           A1: (x * v) = (x * p) by Def2;

          reconsider r = k as sequence of L by Def2;

          

           A2: (x * w) = (x * q) by Def2;

          (x * k) = (x * r) by Def2;

          

          hence (x * (v + w)) = (x * (p + q)) by Def2

          .= ((x9 * p) + (x9 * q)) by Th6

          .= ((x * v) + (x * w)) by A1, A2, Def2;

        end;

        thus F is scalar-distributive

        proof

          let x,y be Element of L;

          let v be Element of ( Formal-Series L);

          reconsider p = v as sequence of L by Def2;

          reconsider x9 = x, y9 = y as Element of L;

          

           A3: (x * v) = (x * p) by Def2;

          

           A4: (y * v) = (y * p) by Def2;

          

          thus ((x + y) * v) = ((x9 + y9) * p) by Def2

          .= ((x9 * p) + (y9 * p)) by Th7

          .= ((x * v) + (y * v)) by A3, A4, Def2;

        end;

        thus F is scalar-associative

        proof

          let x,y be Element of L;

          let v be Element of ( Formal-Series L);

          reconsider p = v as sequence of L by Def2;

          reconsider x9 = x, y9 = y as Element of L;

          

           A5: (y * v) = (y * p) by Def2;

          

          thus ((x * y) * v) = ((x9 * y9) * p) by Def2

          .= (x9 * (y9 * p)) by Th8

          .= (x * (y * v)) by A5, Def2;

        end;

        let v be Element of F;

        reconsider p = v as sequence of L by Def2;

        

        thus (( 1. L) * v) = (( 1. L) * p) by Def2

        .= v by Th9;

      end;

    end

    theorem :: POLYALG1:10

    

     Th10: for L be Abelian left_zeroed add-associative associative right_zeroed right_complementable distributive non empty doubleLoopStr holds for a be Element of L, p,q be sequence of L holds (a * (p *' q)) = ((a * p) *' q)

    proof

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

      let a be Element of L, p,q be sequence of L;

      for x be Element of NAT holds ((a * (p *' q)) . x) = (((a * p) *' q) . x)

      proof

        let i be Element of NAT ;

        consider f1 be FinSequence of the carrier of L such that

         A1: ( len f1) = (i + 1) and

         A2: ((p *' q) . i) = ( Sum f1) and

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

        consider f2 be FinSequence of the carrier of L such that

         A4: ( len f2) = (i + 1) and

         A5: (((a * p) *' q) . i) = ( Sum f2) and

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

        

         A7: ( dom (a * f1)) = ( dom f1) by POLYNOM1:def 1

        .= ( dom f2) by A1, A4, FINSEQ_3: 29;

        

         A8: for k be Nat st k in ( dom f2) holds (f2 . k) = ((a * f1) . k)

        proof

          let k be Nat such that

           A9: k in ( dom f2);

          

           A10: k in ( dom f1) by A1, A4, A9, FINSEQ_3: 29;

          

          then

           A11: ((p . (k -' 1)) * (q . ((i + 1) -' k))) = (f1 . k) by A3

          .= (f1 /. k) by A10, PARTFUN1:def 6;

          

          thus (f2 . k) = (((a * p) . (k -' 1)) * (q . ((i + 1) -' k))) by A6, A9

          .= ((a * (p . (k -' 1))) * (q . ((i + 1) -' k))) by POLYNOM5:def 4

          .= (a * (f1 /. k)) by A11, GROUP_1:def 3

          .= ((a * f1) /. k) by A10, POLYNOM1:def 1

          .= ((a * f1) . k) by A7, A9, PARTFUN1:def 6;

        end;

        

        thus ((a * (p *' q)) . i) = (a * ( Sum f1)) by A2, POLYNOM5:def 4

        .= ( Sum (a * f1)) by BINOM: 4

        .= (((a * p) *' q) . i) by A5, A7, A8, FINSEQ_1: 13;

      end;

      hence thesis by FUNCT_2: 63;

    end;

    registration

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

      cluster ( Formal-Series L) -> mix-associative;

      coherence

      proof

        let a be Element of L, x,y be Element of ( Formal-Series L);

        reconsider x1 = x, y1 = y as Element of ( Formal-Series L);

        reconsider p = x1, q = y1 as sequence of L by Def2;

        

         A1: (a * x) = (a * p) by Def2;

        (x * y) = (p *' q) by Def2;

        

        hence (a * (x * y)) = (a * (p *' q)) by Def2

        .= ((a * p) *' q) by Th10

        .= ((a * x) * y) by A1, Def2;

      end;

    end

    definition

      let L be 1-sorted;

      let A be AlgebraStr over L;

      :: POLYALG1:def3

      mode Subalgebra of A -> AlgebraStr over L means

      : Def3: the carrier of it c= the carrier of A & ( 1. it ) = ( 1. A) & ( 0. it ) = ( 0. A) & the addF of it = (the addF of A || the carrier of it ) & the multF of it = (the multF of A || the carrier of it ) & the lmult of it = (the lmult of A | [:the carrier of L, the carrier of it :]);

      existence

      proof

        take A;

        thus thesis;

      end;

    end

    theorem :: POLYALG1:11

    

     Th11: for L be 1-sorted holds for A be AlgebraStr over L holds A is Subalgebra of A

    proof

      let L be 1-sorted;

      let A be AlgebraStr over L;

      thus the carrier of A c= the carrier of A & ( 1. A) = ( 1. A) & ( 0. A) = ( 0. A) & the addF of A = (the addF of A || the carrier of A) & the multF of A = (the multF of A || the carrier of A) & the lmult of A = (the lmult of A | [:the carrier of L, the carrier of A:]);

    end;

    theorem :: POLYALG1:12

    for L be 1-sorted holds for A,B,C be AlgebraStr over L st A is Subalgebra of B & B is Subalgebra of C holds A is Subalgebra of C

    proof

      let L be 1-sorted;

      let A,B,C be AlgebraStr over L such that

       A1: A is Subalgebra of B and

       A2: B is Subalgebra of C;

      

       A3: the carrier of A c= the carrier of B by A1, Def3;

      then

       A4: [:the carrier of A, the carrier of A:] c= [:the carrier of B, the carrier of B:] by ZFMISC_1: 96;

      the carrier of B c= the carrier of C by A2, Def3;

      hence the carrier of A c= the carrier of C by A3;

      

      thus ( 1. A) = ( 1. B) by A1, Def3

      .= ( 1. C) by A2, Def3;

      

      thus ( 0. A) = ( 0. B) by A1, Def3

      .= ( 0. C) by A2, Def3;

      

      thus the addF of A = (the addF of B || the carrier of A) by A1, Def3

      .= ((the addF of C || the carrier of B) || the carrier of A) by A2, Def3

      .= (the addF of C || the carrier of A) by A4, FUNCT_1: 51;

      

      thus the multF of A = (the multF of B || the carrier of A) by A1, Def3

      .= ((the multF of C || the carrier of B) || the carrier of A) by A2, Def3

      .= (the multF of C || the carrier of A) by A4, FUNCT_1: 51;

      

       A5: [:the carrier of L, the carrier of A:] c= [:the carrier of L, the carrier of B:] by A3, ZFMISC_1: 96;

      

      thus the lmult of A = (the lmult of B | [:the carrier of L, the carrier of A:]) by A1, Def3

      .= ((the lmult of C | [:the carrier of L, the carrier of B:]) | [:the carrier of L, the carrier of A:]) by A2, Def3

      .= (the lmult of C | [:the carrier of L, the carrier of A:]) by A5, FUNCT_1: 51;

    end;

    theorem :: POLYALG1:13

    for L be 1-sorted holds for A,B be AlgebraStr over L st A is Subalgebra of B & B is Subalgebra of A holds the AlgebraStr of A = the AlgebraStr of B

    proof

      let L be 1-sorted;

      let A,B be AlgebraStr over L such that

       A1: A is Subalgebra of B and

       A2: B is Subalgebra of A;

      

       A3: the carrier of B c= the carrier of A by A2, Def3;

      

       A4: the carrier of A c= the carrier of B by A1, Def3;

      then

       A5: the carrier of A = the carrier of B by A3, XBOOLE_0:def 10;

      

       A6: ( dom the lmult of B) = [:the carrier of L, the carrier of B:] by Th2;

      

       A7: the lmult of A = (the lmult of B | [:the carrier of L, the carrier of A:]) by A1, Def3

      .= the lmult of B by A3, A6, RELAT_1: 68, ZFMISC_1: 96;

      

       A8: ( 0. A) = ( 0. B) & ( 1. A) = ( 1. B) by A1, Def3;

      

       A9: the multF of A = (the multF of B || the carrier of A) by A1, Def3

      .= the multF of B by A5;

      the addF of A = (the addF of B || the carrier of A) by A1, Def3

      .= the addF of B by A5;

      hence thesis by A4, A3, A9, A7, A8, XBOOLE_0:def 10;

    end;

    theorem :: POLYALG1:14

    

     Th14: for L be 1-sorted holds for A,B be AlgebraStr over L st the AlgebraStr of A = the AlgebraStr of B holds A is Subalgebra of B

    proof

      let L be 1-sorted;

      let A,B be AlgebraStr over L such that

       A1: the AlgebraStr of A = the AlgebraStr of B;

      thus the carrier of A c= the carrier of B by A1;

      thus ( 1. A) = ( 1. B) by A1;

      thus ( 0. A) = ( 0. B) by A1;

      thus the addF of A = (the addF of B || the carrier of A) by A1;

      thus the multF of A = (the multF of B || the carrier of A) by A1;

      thus thesis by A1;

    end;

    registration

      let L be non empty 1-sorted;

      cluster non empty strict for AlgebraStr over L;

      existence

      proof

         0 in { 0 } by TARSKI:def 1;

        then

        reconsider lm = ( [:the carrier of L, { 0 }:] --> 0 ) as Function of [:the carrier of L, { 0 }:], { 0 } by FUNCOP_1: 45;

        reconsider z = 0 as Element of { 0 } by TARSKI:def 1;

        set A = { 0 };

        set a = the BinOp of A;

        take B = AlgebraStr (# { 0 }, a, a, z, z, lm #);

        thus B is non empty;

        thus thesis;

      end;

    end

    registration

      let L be 1-sorted;

      let B be AlgebraStr over L;

      cluster strict for Subalgebra of B;

      existence

      proof

        reconsider b = AlgebraStr (# the carrier of B, the addF of B, the multF of B, ( 0. B), ( 1. B), the lmult of B #) as Subalgebra of B by Th14;

        take b;

        thus thesis;

      end;

    end

    registration

      let L be non empty 1-sorted;

      let B be non empty AlgebraStr over L;

      cluster strict non empty for Subalgebra of B;

      existence

      proof

        reconsider b = AlgebraStr (# the carrier of B, the addF of B, the multF of B, ( 0. B), ( 1. B), the lmult of B #) as Subalgebra of B by Th14;

        take b;

        thus thesis;

      end;

    end

    definition

      let L be non empty multMagma;

      let B be non empty AlgebraStr over L;

      let A be Subset of B;

      :: POLYALG1:def4

      attr A is opers_closed means

      : Def4: A is linearly-closed & (for x,y be Element of B st x in A & y in A holds (x * y) in A) & ( 1. B) in A & ( 0. B) in A;

    end

    theorem :: POLYALG1:15

    

     Th15: for L be non empty multMagma holds for B be non empty AlgebraStr over L holds for A be non empty Subalgebra of B holds for x,y be Element of B, x9,y9 be Element of A st x = x9 & y = y9 holds (x + y) = (x9 + y9)

    proof

      let L be non empty multMagma;

      let B be non empty AlgebraStr over L;

      let A be non empty Subalgebra of B;

      let x,y be Element of B, x9,y9 be Element of A such that

       A1: x = x9 & y = y9;

       [x9, y9] in [:the carrier of A, the carrier of A:] by ZFMISC_1: 87;

      

      hence (x + y) = ((the addF of B || the carrier of A) . [x9, y9]) by A1, FUNCT_1: 49

      .= (x9 + y9) by Def3;

    end;

    theorem :: POLYALG1:16

    

     Th16: for L be non empty multMagma holds for B be non empty AlgebraStr over L holds for A be non empty Subalgebra of B holds for x,y be Element of B, x9,y9 be Element of A st x = x9 & y = y9 holds (x * y) = (x9 * y9)

    proof

      let L be non empty multMagma;

      let B be non empty AlgebraStr over L;

      let A be non empty Subalgebra of B;

      let x,y be Element of B, x9,y9 be Element of A such that

       A1: x = x9 & y = y9;

       [x9, y9] in [:the carrier of A, the carrier of A:] by ZFMISC_1: 87;

      

      hence (x * y) = ((the multF of B || the carrier of A) . [x9, y9]) by A1, FUNCT_1: 49

      .= (x9 * y9) by Def3;

    end;

    theorem :: POLYALG1:17

    

     Th17: for L be non empty multMagma holds for B be non empty AlgebraStr over L holds for A be non empty Subalgebra of B holds for a be Element of L holds for x be Element of B, x9 be Element of A st x = x9 holds (a * x) = (a * x9)

    proof

      let L be non empty multMagma;

      let B be non empty AlgebraStr over L;

      let A be non empty Subalgebra of B;

      let a be Element of L;

      let x be Element of B, x9 be Element of A such that

       A1: x = x9;

       [a, x9] in [:the carrier of L, the carrier of A:] by ZFMISC_1: 87;

      

      hence (a * x) = ((the lmult of B | [:the carrier of L, the carrier of A:]) . [a, x9]) by A1, FUNCT_1: 49

      .= (a * x9) by Def3;

    end;

    theorem :: POLYALG1:18

    for L be non empty multMagma holds for B be non empty AlgebraStr over L holds for A be non empty Subalgebra of B holds ex C be Subset of B st the carrier of A = C & C is opers_closed

    proof

      let L be non empty multMagma;

      let B be non empty AlgebraStr over L;

      let A be non empty Subalgebra of B;

      take C = the carrier of A;

      

       A1: ( 1. B) = ( 1. A) & ( 0. B) = ( 0. A) by Def3;

      reconsider C as Subset of B by Def3;

      

       A2: for a be Element of L, v be Element of B st v in C holds (a * v) in C

      proof

        let a be Element of L, v be Element of B;

        assume v in C;

        then

        reconsider x = v as Element of A;

        (a * v) = (a * x) by Th17;

        hence thesis;

      end;

      

       A3: for x,y be Element of B st x in C & y in C holds (x * y) in C

      proof

        let x,y be Element of B such that

         A4: x in C & y in C;

        reconsider x9 = x, y9 = y as Element of B;

        reconsider x1 = x9, y1 = y9 as Element of A by A4;

        (x * y) = (x1 * y1) by Th16;

        hence thesis;

      end;

      for v,u be Element of B st v in C & u in C holds (v + u) in C

      proof

        let v,u be Element of B;

        assume v in C & u in C;

        then

        reconsider x = u, y = v as Element of A;

        (v + u) = (y + x) by Th15;

        hence thesis;

      end;

      then C is linearly-closed by A2, VECTSP_4:def 1;

      hence thesis by A1, A3, Def4;

    end;

    theorem :: POLYALG1:19

    

     Th19: for L be non empty multMagma holds for B be non empty AlgebraStr over L holds for A be Subset of B st A is opers_closed holds ex C be strict Subalgebra of B st the carrier of C = A

    proof

      let L be non empty multMagma;

      let B be non empty AlgebraStr over L;

      let A be Subset of B such that

       A1: A is opers_closed;

      reconsider z = ( 0. B) as Element of A by A1;

      reconsider f4 = (the lmult of B | [:the carrier of L, A:]) as Function;

      

       A2: for x be object st x in [:the carrier of L, A:] holds (f4 . x) in A

      proof

        

         A3: A is linearly-closed by A1;

        let x be object such that

         A4: x in [:the carrier of L, A:];

        consider y,z be object such that

         A5: y in the carrier of L and

         A6: z in A and

         A7: x = [y, z] by A4, ZFMISC_1:def 2;

        reconsider z as Element of B by A6;

        reconsider y as Element of L by A5;

        (f4 . x) = (y * z) by A4, A7, FUNCT_1: 49;

        hence thesis by A6, A3, VECTSP_4:def 1;

      end;

       [:the carrier of L, A:] c= [:the carrier of L, the carrier of B:] by ZFMISC_1: 96;

      then [:the carrier of L, A:] c= ( dom the lmult of B) by Th2;

      then ( dom f4) = [:the carrier of L, A:] by RELAT_1: 62;

      then

      reconsider lm = f4 as Function of [:the carrier of L, A:], A by A2, FUNCT_2: 3;

      reconsider f1 = (the addF of B || A) as Function;

      reconsider f2 = (the multF of B || A) as Function;

      

       A8: for x be object st x in [:A, A:] holds (f2 . x) in A

      proof

        let x be object such that

         A9: x in [:A, A:];

        consider y,z be object such that

         A10: y in A & z in A and

         A11: x = [y, z] by A9, ZFMISC_1:def 2;

        reconsider y, z as Element of B by A10;

        (f2 . x) = (y * z) by A9, A11, FUNCT_1: 49;

        hence thesis by A1, A10;

      end;

      

       A12: [:A, A:] c= [:the carrier of B, the carrier of B:] by ZFMISC_1: 96;

      then [:A, A:] c= ( dom the multF of B) by Th1;

      then ( dom f2) = [:A, A:] by RELAT_1: 62;

      then

      reconsider mu = f2 as BinOp of A by A8, FUNCT_2: 3;

      ( dom f1) = [:A, A:] & for x be object st x in [:A, A:] holds (f1 . x) in A

      proof

         [:A, A:] c= ( dom the addF of B) by A12, Th1;

        hence ( dom f1) = [:A, A:] by RELAT_1: 62;

        let x be object such that

         A13: x in [:A, A:];

        consider y,z be object such that

         A14: y in A & z in A and

         A15: x = [y, z] by A13, ZFMISC_1:def 2;

        

         A16: A is linearly-closed by A1;

        reconsider y, z as Element of B by A14;

        (f1 . x) = (y + z) by A13, A15, FUNCT_1: 49;

        hence thesis by A14, A16, VECTSP_4:def 1;

      end;

      then

      reconsider ad = f1 as BinOp of A by FUNCT_2: 3;

      reconsider u = ( 1. B) as Element of A by A1;

      set c = AlgebraStr (# A, ad, mu, z, u, lm #);

      ( 1. c) = ( 1. B) & ( 0. c) = ( 0. B);

      then

      reconsider C = c as strict Subalgebra of B by Def3;

      take C;

      thus thesis;

    end;

    theorem :: POLYALG1:20

    

     Th20: for L be non empty multMagma holds for B be non empty AlgebraStr over L holds for A be non empty Subset of B holds for X be Subset-Family of B st (for Y be set holds Y in X iff Y c= the carrier of B & ex C be Subalgebra of B st Y = the carrier of C & A c= Y) holds ( meet X) is opers_closed

    proof

      let L be non empty multMagma;

      let B be non empty AlgebraStr over L;

      let A be non empty Subset of B;

      let X be Subset-Family of B such that

       A1: for Y be set holds Y in X iff Y c= the carrier of B & ex C be Subalgebra of B st Y = the carrier of C & A c= Y;

      B is Subalgebra of B by Th11;

      then

       A2: X <> {} by A1;

      

       A3: for x,y be Element of B st x in ( meet X) & y in ( meet X) holds (x + y) in ( meet X)

      proof

        let x,y be Element of B such that

         A4: x in ( meet X) & y in ( meet X);

        now

          reconsider x9 = x, y9 = y as Element of B;

          let Y be set;

          assume

           A5: Y in X;

          then

          consider C be Subalgebra of B such that

           A6: Y = the carrier of C and

           A7: A c= Y by A1;

          reconsider C as non empty Subalgebra of B by A6, A7;

          reconsider x1 = x9, y1 = y9 as Element of C by A4, A5, A6, SETFAM_1:def 1;

          (x + y) = (x1 + y1) by Th15;

          hence (x + y) in Y by A6;

        end;

        hence thesis by A2, SETFAM_1:def 1;

      end;

      for a be Element of L, v be Element of B st v in ( meet X) holds (a * v) in ( meet X)

      proof

        let a be Element of L, v be Element of B such that

         A8: v in ( meet X);

        now

          let Y be set;

          assume

           A9: Y in X;

          then

          consider C be Subalgebra of B such that

           A10: Y = the carrier of C and

           A11: A c= Y by A1;

          reconsider C as non empty Subalgebra of B by A10, A11;

          reconsider v9 = v as Element of C by A8, A9, A10, SETFAM_1:def 1;

          (a * v) = (a * v9) by Th17;

          hence (a * v) in Y by A10;

        end;

        hence thesis by A2, SETFAM_1:def 1;

      end;

      hence ( meet X) is linearly-closed by A3, VECTSP_4:def 1;

      thus for x,y be Element of B st x in ( meet X) & y in ( meet X) holds (x * y) in ( meet X)

      proof

        let x,y be Element of B such that

         A12: x in ( meet X) & y in ( meet X);

        now

          reconsider x9 = x, y9 = y as Element of B;

          let Y be set;

          assume

           A13: Y in X;

          then

          consider C be Subalgebra of B such that

           A14: Y = the carrier of C and

           A15: A c= Y by A1;

          reconsider C as non empty Subalgebra of B by A14, A15;

          reconsider x1 = x9, y1 = y9 as Element of C by A12, A13, A14, SETFAM_1:def 1;

          (x * y) = (x1 * y1) by Th16;

          hence (x * y) in Y by A14;

        end;

        hence thesis by A2, SETFAM_1:def 1;

      end;

      now

        let Y be set;

        assume Y in X;

        then

        consider C be Subalgebra of B such that

         A16: Y = the carrier of C and

         A17: A c= Y by A1;

        reconsider C as non empty Subalgebra of B by A16, A17;

        ( 1. B) = ( 1. C) by Def3;

        hence ( 1. B) in Y by A16;

      end;

      hence ( 1. B) in ( meet X) by A2, SETFAM_1:def 1;

      now

        let Y be set;

        assume Y in X;

        then

        consider C be Subalgebra of B such that

         A18: Y = the carrier of C and

         A19: A c= Y by A1;

        reconsider C as non empty Subalgebra of B by A18, A19;

        ( 0. B) = ( 0. C) by Def3;

        hence ( 0. B) in Y by A18;

      end;

      hence thesis by A2, SETFAM_1:def 1;

    end;

    definition

      let L be non empty multMagma;

      let B be non empty AlgebraStr over L;

      let A be non empty Subset of B;

      :: POLYALG1:def5

      func GenAlg A -> strict non empty Subalgebra of B means

      : Def5: A c= the carrier of it & for C be Subalgebra of B st A c= the carrier of C holds the carrier of it c= the carrier of C;

      existence

      proof

        defpred P[ set] means ex C be Subalgebra of B st $1 = the carrier of C & A c= $1;

        consider X be Subset-Family of B such that

         A1: for Y be Subset of B holds Y in X iff P[Y] from SUBSET_1:sch 3;

         A2:

        now

          let Y be set;

          assume Y in X;

          then ex C be Subalgebra of B st Y = the carrier of C & A c= Y by A1;

          hence A c= Y;

        end;

        set M = ( meet X);

        for Y be set holds Y in X iff Y c= the carrier of B & ex C be Subalgebra of B st Y = the carrier of C & A c= Y by A1;

        then

         A3: M is opers_closed by Th20;

        then

        consider C be strict Subalgebra of B such that

         A4: M = the carrier of C by Th19;

        reconsider C as non empty strict Subalgebra of B by A3, A4;

        take C;

        B is Subalgebra of B & the carrier of B in ( bool the carrier of B) by Th11, ZFMISC_1:def 1;

        then X <> {} by A1;

        hence A c= the carrier of C by A4, A2, SETFAM_1: 5;

        let C1 be Subalgebra of B such that

         A5: A c= the carrier of C1;

        the carrier of C1 c= the carrier of B by Def3;

        then the carrier of C1 in X by A1, A5;

        hence thesis by A4, SETFAM_1: 3;

      end;

      uniqueness

      proof

        let P1,P2 be strict non empty Subalgebra of B;

        assume A c= the carrier of P1 & (for C be Subalgebra of B st A c= the carrier of C holds the carrier of P1 c= the carrier of C) & A c= the carrier of P2 & for C be Subalgebra of B st A c= the carrier of C holds the carrier of P2 c= the carrier of C;

        then

         A6: the carrier of P1 c= the carrier of P2 & the carrier of P2 c= the carrier of P1;

        then

         A7: the carrier of P1 = the carrier of P2 by XBOOLE_0:def 10;

        now

          let x be Element of P1, y be Element of P2;

          reconsider y1 = y as Element of P1 by A6;

          reconsider x1 = x as Element of P2 by A6;

          

           A8: the carrier of P2 c= the carrier of B by Def3;

          then

          reconsider x9 = x1 as Element of B;

          reconsider y9 = y as Element of B by A8;

          

          thus (the multF of P1 . (x,y)) = (x * y1)

          .= (x9 * y9) by Th16

          .= (x1 * y) by Th16

          .= (the multF of P2 . (x,y));

        end;

        then

         A9: the multF of P1 = the multF of P2 by A7, BINOP_1: 2;

        

         A10: ( 0. P1) = ( 0. B) by Def3

        .= ( 0. P2) by Def3;

         A11:

        now

          let x be Element of L, y be Element of P1;

          reconsider y1 = y as Element of P2 by A6;

          the carrier of P2 c= the carrier of B by Def3;

          then

          reconsider y9 = y1 as Element of B;

          

          thus (the lmult of P1 . (x,y)) = (x * y)

          .= (x * y9) by Th17

          .= (x * y1) by Th17

          .= (the lmult of P2 . (x,y));

        end;

        

         A12: ( 1. P1) = ( 1. B) by Def3

        .= ( 1. P2) by Def3;

        now

          let x be Element of P1, y be Element of P2;

          reconsider y1 = y as Element of P1 by A6;

          reconsider x1 = x as Element of P2 by A6;

          

           A13: the carrier of P2 c= the carrier of B by Def3;

          then

          reconsider x9 = x1 as Element of B;

          reconsider y9 = y as Element of B by A13;

          

          thus (the addF of P1 . (x,y)) = (x + y1)

          .= (x9 + y9) by Th15

          .= (x1 + y) by Th15

          .= (the addF of P2 . (x,y));

        end;

        then the addF of P1 = the addF of P2 by A7, BINOP_1: 2;

        hence thesis by A7, A9, A10, A12, A11, BINOP_1: 2;

      end;

    end

    theorem :: POLYALG1:21

    

     Th21: for L be non empty multMagma holds for B be non empty AlgebraStr over L holds for A be non empty Subset of B st A is opers_closed holds the carrier of ( GenAlg A) = A

    proof

      let L be non empty multMagma;

      let B be non empty AlgebraStr over L;

      let A be non empty Subset of B;

      assume A is opers_closed;

      then ex C be strict Subalgebra of B st the carrier of C = A by Th19;

      then

       A1: the carrier of ( GenAlg A) c= A by Def5;

      A c= the carrier of ( GenAlg A) by Def5;

      hence thesis by A1, XBOOLE_0:def 10;

    end;

    begin

    definition

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

      :: POLYALG1:def6

      func Polynom-Algebra L -> strict non empty AlgebraStr over L means

      : Def6: ex A be non empty Subset of ( Formal-Series L) st A = the carrier of ( Polynom-Ring L) & it = ( GenAlg A);

      existence

      proof

        the carrier of ( Polynom-Ring L) c= the carrier of ( Formal-Series L)

        proof

          let x be object;

          assume x in the carrier of ( Polynom-Ring L);

          then x is AlgSequence of L by POLYNOM3:def 10;

          hence thesis by Def2;

        end;

        then

        reconsider A = the carrier of ( Polynom-Ring L) as non empty Subset of ( Formal-Series L);

        take ( GenAlg A);

        thus thesis;

      end;

      uniqueness ;

    end

    registration

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

      cluster ( Polynom-Ring L) -> Loop-like;

      coherence

      proof

        

         A1: for a,b be Element of ( Polynom-Ring L) holds ex x be Element of ( Polynom-Ring L) st (x + a) = b

        proof

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

          reconsider x = (b - a) as Element of ( Polynom-Ring L);

          take x;

          

          thus (x + a) = (b + (( - a) + a)) by RLVECT_1:def 3

          .= (b + ( 0. ( Polynom-Ring L))) by RLVECT_1: 5

          .= b by RLVECT_1: 4;

        end;

        

         A2: for a,x,y be Element of ( Polynom-Ring L) holds (x + a) = (y + a) implies x = y by RLVECT_1: 8;

        (for a,b be Element of ( Polynom-Ring L) holds ex x be Element of ( Polynom-Ring L) st (a + x) = b) & for a,x,y be Element of ( Polynom-Ring L) holds (a + x) = (a + y) implies x = y by RLVECT_1: 7, RLVECT_1: 8;

        hence thesis by A1, A2, ALGSTR_1: 6;

      end;

    end

    theorem :: POLYALG1:22

    

     Th22: for L be add-associative right_zeroed right_complementable distributive non empty doubleLoopStr holds for A be non empty Subset of ( Formal-Series L) st A = the carrier of ( Polynom-Ring L) holds A is opers_closed

    proof

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

      set B = ( Formal-Series L);

      let A be non empty Subset of ( Formal-Series L) such that

       A1: A = the carrier of ( Polynom-Ring L);

      

       A2: for a be Element of L, v be Element of B st v in A holds (a * v) in A

      proof

        let a be Element of L, v be Element of B;

        assume v in A;

        then

        reconsider p = v as AlgSequence of L by A1, POLYNOM3:def 10;

        reconsider a9 = a as Element of L;

        (a * v) = (a9 * p) by Def2;

        hence thesis by A1, POLYNOM3:def 10;

      end;

      for v,u be Element of B st v in A & u in A holds (v + u) in A

      proof

        let v,u be Element of B;

        assume v in A & u in A;

        then

        reconsider p = v, q = u as AlgSequence of L by A1, POLYNOM3:def 10;

        (v + u) = (p + q) by Def2;

        hence thesis by A1, POLYNOM3:def 10;

      end;

      hence A is linearly-closed by A2, VECTSP_4:def 1;

      thus for u,v be Element of B st u in A & v in A holds (u * v) in A

      proof

        let u,v be Element of B;

        assume u in A & v in A;

        then

        reconsider p = u, q = v as AlgSequence of L by A1, POLYNOM3:def 10;

        (u * v) = (p *' q) by Def2;

        hence thesis by A1, POLYNOM3:def 10;

      end;

      ( 1. B) = ( 1_. L) by Def2

      .= ( 1. ( Polynom-Ring L)) by POLYNOM3:def 10;

      hence ( 1. B) in A by A1;

      ( 0. B) = ( 0_. L) by Def2

      .= ( 0. ( Polynom-Ring L)) by POLYNOM3:def 10;

      hence thesis by A1;

    end;

    theorem :: POLYALG1:23

    for L be add-associative right_zeroed right_complementable distributive non empty doubleLoopStr holds the doubleLoopStr of ( Polynom-Algebra L) = ( Polynom-Ring L)

    proof

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

      

       A1: ex A be non empty Subset of ( Formal-Series L) st A = the carrier of ( Polynom-Ring L) & ( Polynom-Algebra L) = ( GenAlg A) by Def6;

      then

       A2: the carrier of ( Polynom-Algebra L) = the carrier of ( Polynom-Ring L) by Th21, Th22;

      

       A3: the carrier of ( Polynom-Algebra L) c= the carrier of ( Formal-Series L) by A1, Def3;

      

       A4: for x be Element of ( Polynom-Algebra L) holds for y be Element of ( Polynom-Ring L) holds (the addF of ( Polynom-Algebra L) . (x,y)) = (the addF of ( Polynom-Ring L) . (x,y))

      proof

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

        reconsider y1 = y as Element of ( Polynom-Algebra L) by A1, Th21, Th22;

        reconsider y9 = y1 as Element of ( Formal-Series L) by A1, TARSKI:def 3;

        reconsider x9 = x as Element of ( Formal-Series L) by A3;

        reconsider p = x as AlgSequence of L by A2, POLYNOM3:def 10;

        reconsider x1 = x as Element of ( Polynom-Ring L) by A1, Th21, Th22;

        reconsider q = y as AlgSequence of L by POLYNOM3:def 10;

        

        thus (the addF of ( Polynom-Algebra L) . (x,y)) = (x + y1)

        .= (x9 + y9) by A1, Th15

        .= (p + q) by Def2

        .= (x1 + y) by POLYNOM3:def 10

        .= (the addF of ( Polynom-Ring L) . (x,y));

      end;

      now

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

        reconsider y1 = y as Element of ( Polynom-Algebra L) by A1, Th21, Th22;

        reconsider y9 = y1 as Element of ( Formal-Series L) by A1, TARSKI:def 3;

        reconsider x9 = x as Element of ( Formal-Series L) by A3;

        reconsider p = x as AlgSequence of L by A2, POLYNOM3:def 10;

        reconsider x1 = x as Element of ( Polynom-Ring L) by A1, Th21, Th22;

        reconsider q = y as AlgSequence of L by POLYNOM3:def 10;

        

        thus (the multF of ( Polynom-Algebra L) . (x,y)) = (x * y1)

        .= (x9 * y9) by A1, Th16

        .= (p *' q) by Def2

        .= (x1 * y) by POLYNOM3:def 10

        .= (the multF of ( Polynom-Ring L) . (x,y));

      end;

      then

       A5: the multF of ( Polynom-Algebra L) = the multF of ( Polynom-Ring L) by A2, BINOP_1: 2;

      

       A6: ( 1. ( Polynom-Algebra L)) = ( 1. ( Formal-Series L)) by A1, Def3

      .= ( 1_. L) by Def2

      .= ( 1. ( Polynom-Ring L)) by POLYNOM3:def 10;

      ( 0. ( Polynom-Algebra L)) = ( 0. ( Formal-Series L)) by A1, Def3

      .= ( 0_. L) by Def2

      .= ( 0. ( Polynom-Ring L)) by POLYNOM3:def 10;

      hence thesis by A2, A4, A5, A6, BINOP_1: 2;

    end;

    theorem :: POLYALG1:24

    for L be add-associative right_zeroed right_complementable well-unital distributive non empty doubleLoopStr holds ( 1_ ( Formal-Series L)) = ( 1_. L) by Def2;