monoid_0.miz



    begin

    reserve x,y,X,Y for set;

    deffunc carr( 1-sorted) = the carrier of $1;

    deffunc op( multMagma) = the multF of $1;

    definition

      let G be 1-sorted;

      mode BinOp of G is BinOp of the carrier of G;

    end

    definition

      let IT be 1-sorted;

      :: MONOID_0:def1

      attr IT is constituted-Functions means

      : Def1: for a be Element of IT holds a is Function;

      :: MONOID_0:def2

      attr IT is constituted-FinSeqs means

      : Def2: for a be Element of IT holds a is FinSequence;

    end

    registration

      cluster constituted-Functions for 1-sorted;

      existence

      proof

        set f = the Function;

        take X = 1-sorted (# {f} #);

        let a be Element of X;

        thus thesis;

      end;

      cluster constituted-FinSeqs for 1-sorted;

      existence

      proof

        set f = the FinSequence;

        take X = 1-sorted (# {f} #);

        let a be Element of X;

        thus thesis by TARSKI:def 1;

      end;

    end

    registration

      let X be constituted-Functions 1-sorted;

      cluster -> Function-like Relation-like for Element of X;

      coherence by Def1;

    end

    registration

      cluster constituted-FinSeqs -> constituted-Functions for 1-sorted;

      coherence ;

    end

    registration

      let X be constituted-FinSeqs 1-sorted;

      cluster -> FinSequence-like for Element of X;

      coherence by Def2;

    end

    definition

      let D be set, p,q be FinSequence of D;

      :: original: ^

      redefine

      func p ^ q -> Element of (D * ) ;

      coherence

      proof

        thus (p ^ q) is Element of (D * ) by FINSEQ_1:def 11;

      end;

    end

    notation

      let g,f be Function;

      synonym f (*) g for f * g;

    end

    definition

      let D be non empty set;

      let IT be BinOp of D;

      :: MONOID_0:def3

      attr IT is left-invertible means for a,b be Element of D holds ex l be Element of D st (IT . (l,a)) = b;

      :: MONOID_0:def4

      attr IT is right-invertible means for a,b be Element of D holds ex r be Element of D st (IT . (a,r)) = b;

      :: MONOID_0:def5

      attr IT is invertible means for a,b be Element of D holds ex r,l be Element of D st (IT . (a,r)) = b & (IT . (l,a)) = b;

      :: MONOID_0:def6

      attr IT is left-cancelable means for a,b,c be Element of D st (IT . (a,b)) = (IT . (a,c)) holds b = c;

      :: MONOID_0:def7

      attr IT is right-cancelable means for a,b,c be Element of D st (IT . (b,a)) = (IT . (c,a)) holds b = c;

      :: MONOID_0:def8

      attr IT is cancelable means for a,b,c be Element of D st (IT . (a,b)) = (IT . (a,c)) or (IT . (b,a)) = (IT . (c,a)) holds b = c;

      :: MONOID_0:def9

      attr IT is uniquely-decomposable means IT is having_a_unity & for a,b be Element of D st (IT . (a,b)) = ( the_unity_wrt IT) holds a = b & b = ( the_unity_wrt IT);

    end

    theorem :: MONOID_0:1

    

     Th1: for D be non empty set, f be BinOp of D holds f is invertible iff f is left-invertible right-invertible

    proof

      let D be non empty set, f be BinOp of D;

      thus f is invertible implies f is left-invertible right-invertible

      proof

        assume

         A1: for a,b be Element of D holds ex r,l be Element of D st (f . (a,r)) = b & (f . (l,a)) = b;

        now

          let a,b be Element of D;

          consider r,l be Element of D such that (f . (a,r)) = b and

           A2: (f . (l,a)) = b by A1;

          take l;

          thus (f . (l,a)) = b by A2;

        end;

        hence for a,b be Element of D holds ex l be Element of D st (f . (l,a)) = b;

        let a,b be Element of D;

        consider r,l be Element of D such that

         A3: (f . (a,r)) = b and (f . (l,a)) = b by A1;

        take r;

        thus thesis by A3;

      end;

      assume that

       A4: for a,b be Element of D holds ex l be Element of D st (f . (l,a)) = b and

       A5: for a,b be Element of D holds ex r be Element of D st (f . (a,r)) = b;

      let a,b be Element of D;

      consider l be Element of D such that

       A6: (f . (l,a)) = b by A4;

      consider r be Element of D such that

       A7: (f . (a,r)) = b by A5;

      take r, l;

      thus thesis by A6, A7;

    end;

    theorem :: MONOID_0:2

    for D be non empty set, f be BinOp of D holds f is cancelable iff f is left-cancelable right-cancelable;

    theorem :: MONOID_0:3

    

     Th3: for f be BinOp of {x} holds f = ((x,x) .--> x) & f is having_a_unity & f is commutative & f is associative & f is idempotent & f is invertible cancelable uniquely-decomposable

    proof

      let f be BinOp of {x};

      reconsider a = x as Element of {x} by TARSKI:def 1;

      

       A1: [: {x}, {x}:] = { [x, x]} by ZFMISC_1: 29;

       A2:

      now

        let y be object;

        assume

         A3: y in { [x, x]};

        then

        reconsider b = y as Element of [: {x}, {x}:] by ZFMISC_1: 29;

        

        thus (f . y) = (f . b)

        .= x by TARSKI:def 1

        .= (((x,x) .--> x) . y) by A3, FUNCOP_1: 7;

      end;

      ( dom f) = [: {x}, {x}:] & ( dom ((x,x) .--> x)) = { [x, x]} by FUNCT_2:def 1;

      hence f = ((x,x) .--> x) by A1, A2, FUNCT_1: 2;

       A4:

      now

        let a,b be Element of {x};

        a = x by TARSKI:def 1;

        hence a = b by TARSKI:def 1;

      end;

      then for b be Element of {x} holds (f . (a,b)) = b & (f . (b,a)) = b;

      then

       A5: a is_a_unity_wrt f by BINOP_1: 3;

      hence ex a be Element of {x} st a is_a_unity_wrt f;

      thus for a,b be Element of {x} holds (f . (a,b)) = (f . (b,a)) by A4;

      thus for a,b,c be Element of {x} holds (f . (a,(f . (b,c)))) = (f . ((f . (a,b)),c)) by A4;

      thus for a be Element of {x} holds (f . (a,a)) = a by A4;

      thus for a,b be Element of {x} holds ex r,l be Element of {x} st (f . (a,r)) = b & (f . (l,a)) = b

      proof

        let a,b be Element of {x};

        take a, a;

        thus thesis by A4;

      end;

      thus for a,b,c be Element of {x} st (f . (a,b)) = (f . (a,c)) or (f . (b,a)) = (f . (c,a)) holds b = c by A4;

      thus ex a be Element of {x} st a is_a_unity_wrt f by A5;

      let a,b be Element of {x};

      thus thesis by A4;

    end;

    begin

    reserve G for non empty multMagma,

D for non empty set,

a,b,c,r,l for Element of G;

    definition

      let IT be non empty multMagma;

      :: original: unital

      redefine

      :: MONOID_0:def10

      attr IT is unital means

      : Def10: the multF of IT is having_a_unity;

      compatibility

      proof

        thus IT is unital implies the multF of IT is having_a_unity;

        given x be Element of IT such that

         A1: x is_a_unity_wrt the multF of IT;

        take x;

        let h be Element of IT;

        thus thesis by A1, BINOP_1: 3;

      end;

    end

    definition

      let G;

      :: original: commutative

      redefine

      :: MONOID_0:def11

      attr G is commutative means

      : Def11: the multF of G is commutative;

      compatibility

      proof

        thus G is commutative implies the multF of G is commutative

        proof

          assume

           A1: (a * b) = (b * a);

          let a, b;

          ( op(G) . (a,b)) = (a * b) & ( op(G) . (b,a)) = (b * a);

          hence thesis by A1;

        end;

        assume

         A2: for a, b holds ( op(G) . (a,b)) = ( op(G) . (b,a));

        let a, b;

        thus thesis by A2;

      end;

      :: original: associative

      redefine

      :: MONOID_0:def12

      attr G is associative means

      : Def12: the multF of G is associative;

      compatibility ;

    end

    definition

      let IT be non empty multMagma;

      :: MONOID_0:def13

      attr IT is idempotent means the multF of IT is idempotent;

      :: MONOID_0:def14

      attr IT is left-invertible means the multF of IT is left-invertible;

      :: MONOID_0:def15

      attr IT is right-invertible means the multF of IT is right-invertible;

      :: MONOID_0:def16

      attr IT is invertible means the multF of IT is invertible;

      :: MONOID_0:def17

      attr IT is left-cancelable means the multF of IT is left-cancelable;

      :: MONOID_0:def18

      attr IT is right-cancelable means the multF of IT is right-cancelable;

      :: MONOID_0:def19

      attr IT is cancelable means the multF of IT is cancelable;

      :: MONOID_0:def20

      attr IT is uniquely-decomposable means

      : Def20: the multF of IT is uniquely-decomposable;

    end

    registration

      cluster unital commutative associative cancelable idempotent invertible uniquely-decomposable constituted-Functions constituted-FinSeqs strict for non empty multMagma;

      existence

      proof

        set p = the FinSequence, o = the BinOp of {p};

        take G = multMagma (# {p}, o #);

        thus op(G) is having_a_unity & op(G) is commutative & op(G) is associative & op(G) is cancelable & op(G) is idempotent & op(G) is invertible uniquely-decomposable by Th3;

        thus (for x be Element of G holds x is Function) & for x be Element of G holds x is FinSequence by TARSKI:def 1;

        thus thesis;

      end;

    end

    theorem :: MONOID_0:4

    

     Th4: G is unital implies ( the_unity_wrt the multF of G) is_a_unity_wrt the multF of G

    proof

      given a such that

       A1: a is_a_unity_wrt op(G);

      thus thesis by A1, BINOP_1:def 8;

    end;

    theorem :: MONOID_0:5

    G is unital iff for a holds (( the_unity_wrt the multF of G) * a) = a & (a * ( the_unity_wrt the multF of G)) = a

    proof

      set u = ( the_unity_wrt the multF of G);

      thus G is unital implies for b holds (u * b) = b & (b * u) = b

      proof

        given a such that

         A1: a is_a_unity_wrt op(G);

        let b;

        u = a by A1, BINOP_1:def 8;

        hence thesis by A1, BINOP_1: 3;

      end;

      assume

       A2: (u * b) = b & (b * u) = b;

      take a = u;

      thus a is_a_left_unity_wrt the multF of G

      proof

        let b;

        (a * b) = b by A2;

        hence thesis;

      end;

      let b;

      (b * a) = b by A2;

      hence thesis;

    end;

    theorem :: MONOID_0:6

    

     Th6: G is unital iff ex a st for b holds (a * b) = b & (b * a) = b;

    

     Lm1: G is associative iff for a, b, c holds ((a * b) * c) = (a * (b * c));

    theorem :: MONOID_0:7

    

     Th7: G is idempotent iff for a holds (a * a) = a

    proof

      thus G is idempotent implies for a holds (a * a) = a

      proof

        assume

         A1: ( op(G) . (a,a)) = a;

        let a;

        thus thesis by A1;

      end;

      assume

       A2: (a * a) = a;

      let a;

      

      thus ( op(G) . (a,a)) = (a * a)

      .= a by A2;

    end;

    theorem :: MONOID_0:8

    G is left-invertible iff for a, b holds ex l st (l * a) = b

    proof

      thus G is left-invertible implies for a, b holds ex l st (l * a) = b

      proof

        assume

         A1: for a, b holds ex l st ( op(G) . (l,a)) = b;

        let a, b;

        consider l such that

         A2: ( op(G) . (l,a)) = b by A1;

        take l;

        thus thesis by A2;

      end;

      assume

       A3: for a, b holds ex l st (l * a) = b;

      let a, b;

      consider l such that

       A4: (l * a) = b by A3;

      take l;

      thus thesis by A4;

    end;

    theorem :: MONOID_0:9

    G is right-invertible iff for a, b holds ex r st (a * r) = b

    proof

      thus G is right-invertible implies for a, b holds ex r st (a * r) = b

      proof

        assume

         A1: for a, b holds ex r st ( op(G) . (a,r)) = b;

        let a, b;

        consider r such that

         A2: ( op(G) . (a,r)) = b by A1;

        take r;

        thus thesis by A2;

      end;

      assume

       A3: for a, b holds ex r st (a * r) = b;

      let a, b;

      consider r such that

       A4: (a * r) = b by A3;

      take r;

      thus thesis by A4;

    end;

    theorem :: MONOID_0:10

    

     Th10: G is invertible iff for a, b holds ex r, l st (a * r) = b & (l * a) = b

    proof

      thus G is invertible implies for a, b holds ex r, l st (a * r) = b & (l * a) = b

      proof

        assume

         A1: for a, b holds ex r, l st ( op(G) . (a,r)) = b & ( op(G) . (l,a)) = b;

        let a, b;

        consider r, l such that

         A2: ( op(G) . (a,r)) = b & ( op(G) . (l,a)) = b by A1;

        take r, l;

        thus thesis by A2;

      end;

      assume

       A3: for a, b holds ex r, l st (a * r) = b & (l * a) = b;

      let a, b;

      consider r, l such that

       A4: (a * r) = b & (l * a) = b by A3;

      take r, l;

      thus thesis by A4;

    end;

    theorem :: MONOID_0:11

    G is left-cancelable iff for a, b, c st (a * b) = (a * c) holds b = c

    proof

      thus G is left-cancelable implies for a, b, c st (a * b) = (a * c) holds b = c

      proof

        assume

         A1: ( op(G) . (a,b)) = ( op(G) . (a,c)) implies b = c;

        let a, b, c;

        thus thesis by A1;

      end;

      assume

       A2: for a, b, c st (a * b) = (a * c) holds b = c;

      let a, b, c;

      (a * b) = ( op(G) . (a,b)) & (a * c) = ( op(G) . (a,c));

      hence thesis by A2;

    end;

    theorem :: MONOID_0:12

    G is right-cancelable iff for a, b, c st (b * a) = (c * a) holds b = c

    proof

      thus G is right-cancelable implies for a, b, c st (b * a) = (c * a) holds b = c

      proof

        assume

         A1: for a, b, c st ( op(G) . (b,a)) = ( op(G) . (c,a)) holds b = c;

        let a, b, c;

        thus thesis by A1;

      end;

      assume

       A2: for a, b, c st (b * a) = (c * a) holds b = c;

      let a, b, c;

      (b * a) = ( op(G) . (b,a)) & (c * a) = ( op(G) . (c,a));

      hence thesis by A2;

    end;

    theorem :: MONOID_0:13

    

     Th13: G is cancelable iff for a, b, c st (a * b) = (a * c) or (b * a) = (c * a) holds b = c

    proof

      thus G is cancelable implies for a, b, c st (a * b) = (a * c) or (b * a) = (c * a) holds b = c

      proof

        assume

         A1: ( op(G) . (a,b)) = ( op(G) . (a,c)) or ( op(G) . (b,a)) = ( op(G) . (c,a)) implies b = c;

        let a, b, c;

        thus thesis by A1;

      end;

      assume

       A2: for a, b, c st (a * b) = (a * c) or (b * a) = (c * a) holds b = c;

      let a, b, c;

      

       A3: (b * a) = ( op(G) . (b,a)) & (c * a) = ( op(G) . (c,a));

      (a * b) = ( op(G) . (a,b)) & (a * c) = ( op(G) . (a,c));

      hence thesis by A2, A3;

    end;

    theorem :: MONOID_0:14

    

     Th14: G is uniquely-decomposable iff the multF of G is having_a_unity & for a,b be Element of G st (a * b) = ( the_unity_wrt the multF of G) holds a = b & b = ( the_unity_wrt the multF of G)

    proof

      thus G is uniquely-decomposable implies op(G) is having_a_unity & for a,b be Element of G st (a * b) = ( the_unity_wrt op(G)) holds a = b & b = ( the_unity_wrt the multF of G)

      proof

        assume that

         A1: op(G) is having_a_unity and

         A2: for a,b be Element of G st ( op(G) . (a,b)) = ( the_unity_wrt op(G)) holds a = b & b = ( the_unity_wrt op(G));

        thus op(G) is having_a_unity by A1;

        let a,b be Element of G;

        thus thesis by A2;

      end;

      assume that

       A3: op(G) is having_a_unity and

       A4: for a,b be Element of G st (a * b) = ( the_unity_wrt op(G)) holds a = b & b = ( the_unity_wrt op(G));

      thus op(G) is having_a_unity by A3;

      let a,b be Element of G;

      (a * b) = ( op(G) . (a,b));

      hence thesis by A4;

    end;

    theorem :: MONOID_0:15

    

     Th15: G is associative implies (G is invertible iff G is unital & the multF of G is having_an_inverseOp)

    proof

      assume

       A1: G is associative;

      thus G is invertible implies G is unital & op(G) is having_an_inverseOp

      proof

        set e = the Element of G;

        assume

         A2: G is invertible;

        then

        consider x,y be Element of G such that

         A3: (e * x) = e and

         A4: (y * e) = e by Th10;

         A5:

        now

          let a;

          

           A6: ex b, c st (e * b) = a & (c * e) = a by A2, Th10;

          hence (y * a) = a by A1, A4;

          thus (a * x) = a by A1, A3, A6;

        end;

        then

         A7: (y * x) = x & (y * x) = y;

        hence G is unital by A5;

        defpred P[ Element of G, Element of G] means ($1 * $2) = x & ($2 * $1) = x;

        

         A8: for a holds ex b st P[a, b]

        proof

          let a;

          consider b, c such that

           A9: (a * b) = x & (c * a) = x by A2, Th10;

          take b;

          (c * (a * b)) = ((c * a) * b) & (x * b) = b by A1, A5, A7;

          hence thesis by A5, A9;

        end;

        ex f be Function of the carrier of G, the carrier of G st for x be Element of G holds P[x, (f . x)] from FUNCT_2:sch 3( A8);

        then

        consider u be UnOp of carr(G) such that

         A10: for a be Element of G holds P[a, (u . a)];

        now

          let b;

          (x * b) = ( op(G) . (x,b)) & (b * x) = ( op(G) . (b,x));

          hence ( op(G) . (x,b)) = b & ( op(G) . (b,x)) = b by A5, A7;

        end;

        then x is_a_unity_wrt op(G) by BINOP_1: 3;

        then

         A11: x = ( the_unity_wrt op(G)) by BINOP_1:def 8;

        take u;

        let a;

        ( op(G) . (a,(u . a))) = (a * (u . a)) & ( op(G) . ((u . a),a)) = ((u . a) * a);

        hence thesis by A10, A11;

      end;

      assume

       A12: op(G) is having_a_unity;

      given u be UnOp of carr(G) such that

       A13: u is_an_inverseOp_wrt op(G);

      let a, c;

      take l = ((u . a) * c), r = (c * (u . a));

      

      thus ( op(G) . (a,l)) = (a * l)

      .= ((a * (u . a)) * c) by A1

      .= ( op(G) . (( the_unity_wrt op(G)),c)) by A13

      .= c by A12, SETWISEO: 15;

      

      thus ( op(G) . (r,a)) = (r * a)

      .= (c * ((u . a) * a)) by A1

      .= ( op(G) . (c,( the_unity_wrt op(G)))) by A13

      .= c by A12, SETWISEO: 15;

    end;

    

     Lm2: G is invertible iff G is left-invertible right-invertible by Th1;

    

     Lm3: G is cancelable iff G is left-cancelable right-cancelable

    proof

      thus G is cancelable implies G is left-cancelable right-cancelable

      proof

        assume op(G) is cancelable;

        hence op(G) is left-cancelable right-cancelable;

      end;

      assume op(G) is left-cancelable right-cancelable;

      hence op(G) is cancelable;

    end;

    

     Lm4: G is associative invertible implies G is Group-like

    proof

      assume

       A1: G is associative invertible;

      then G is unital by Th15;

      then

      consider a such that

       A2: for b holds (a * b) = b & (b * a) = b;

      take a;

      let b;

      thus (b * a) = b & (a * b) = b by A2;

       op(G) is invertible by A1;

      then

      consider l,r be Element of G such that

       A3: ( op(G) . (b,l)) = a & ( op(G) . (r,b)) = a;

      take l;

      

       A4: (b * l) = a & (r * b) = a by A3;

      r = (r * a) by A2

      .= (a * l) by A1, A4

      .= l by A2;

      hence thesis by A3;

    end;

    registration

      cluster associative Group-like -> invertible for non empty multMagma;

      coherence by Th15;

      cluster associative invertible -> Group-like for non empty multMagma;

      coherence by Lm4;

    end

    registration

      cluster invertible -> left-invertible right-invertible for non empty multMagma;

      coherence by Lm2;

      cluster left-invertible right-invertible -> invertible for non empty multMagma;

      coherence by Lm2;

      cluster cancelable -> left-cancelable right-cancelable for non empty multMagma;

      coherence by Lm3;

      cluster left-cancelable right-cancelable -> cancelable for non empty multMagma;

      coherence by Lm3;

      cluster associative invertible -> unital cancelable for non empty multMagma;

      coherence

      proof

        let G be non empty multMagma;

        assume G is associative invertible;

        then

        reconsider G as associative invertible non empty multMagma;

        for a,b,c be Element of G st (a * b) = (a * c) or (b * a) = (c * a) holds b = c by GROUP_1: 6;

        hence thesis by Th13;

      end;

    end

    begin

    deffunc un( multLoopStr) = ( 1. $1);

    reserve M for non empty multLoopStr;

    definition

      let IT be non empty multLoopStr;

      :: original: well-unital

      redefine

      :: MONOID_0:def21

      attr IT is well-unital means

      : Def21: ( 1. IT) is_a_unity_wrt the multF of IT;

      compatibility

      proof

        thus IT is well-unital implies ( 1. IT) is_a_unity_wrt the multF of IT

        proof

          assume

           A1: IT is well-unital;

          thus ( 1. IT) is_a_left_unity_wrt the multF of IT

          proof

            let a be Element of IT;

            

            thus (the multF of IT . (( 1. IT),a)) = (( 1. IT) * a)

            .= a by A1;

          end;

          let a be Element of IT;

          

          thus (the multF of IT . (a,( 1. IT))) = (a * ( 1. IT))

          .= a by A1;

        end;

        assume

         A2: ( 1. IT) is_a_unity_wrt the multF of IT;

        let x be Element of IT;

        ( 1. IT) is_a_right_unity_wrt the multF of IT by A2;

        hence (x * ( 1. IT)) = x;

        ( 1. IT) is_a_left_unity_wrt the multF of IT by A2;

        hence thesis;

      end;

    end

    theorem :: MONOID_0:16

    

     Th16: M is well-unital iff for a be Element of M holds (( 1. M) * a) = a & (a * ( 1. M)) = a;

    theorem :: MONOID_0:17

    

     Th17: for M be non empty multLoopStr st M is well-unital holds ( 1. M) = ( the_unity_wrt the multF of M) by BINOP_1:def 8;

    registration

      cluster well-unital commutative associative cancelable idempotent invertible uniquely-decomposable unital constituted-Functions constituted-FinSeqs strict for non empty multLoopStr;

      existence

      proof

        set p = the FinSequence, o = the BinOp of {p}, e = the Element of {p};

        take G = multLoopStr (# {p}, o, e #);

        reconsider e as Element of G;

        reconsider o as BinOp of G;

        now

          let b be Element of G;

          (o . (e,b)) = p & (o . (b,e)) = p by TARSKI:def 1;

          hence (o . (e,b)) = b & (o . (b,e)) = b by TARSKI:def 1;

        end;

        hence un(G) is_a_unity_wrt op(G) by BINOP_1: 3;

        hence op(G) is commutative & op(G) is associative & op(G) is cancelable & op(G) is idempotent & op(G) is invertible uniquely-decomposable & ex e be Element of G st e is_a_unity_wrt op(G) by Th3;

        thus (for x be Element of G holds x is Function) & for x be Element of G holds x is FinSequence by TARSKI:def 1;

        thus thesis;

      end;

    end

    definition

      mode Monoid is well-unital associative non empty multLoopStr;

    end

    definition

      let G be multMagma;

      :: MONOID_0:def22

      mode MonoidalExtension of G -> multLoopStr means

      : Def22: the multMagma of it = the multMagma of G;

      existence

      proof

        set g = the Element of G;

        take multLoopStr (# carr(G), op(G), g #);

        thus thesis;

      end;

    end

    registration

      let G be non empty multMagma;

      cluster -> non empty for MonoidalExtension of G;

      coherence

      proof

        let M be MonoidalExtension of G;

         the multMagma of M = the multMagma of G by Def22;

        hence the carrier of M is non empty;

      end;

    end

    theorem :: MONOID_0:18

    

     Th18: for M be MonoidalExtension of G holds the carrier of M = the carrier of G & the multF of M = the multF of G & for a,b be Element of M, a9,b9 be Element of G st a = a9 & b = b9 holds (a * b) = (a9 * b9)

    proof

      let M be MonoidalExtension of G;

      

       A1: the multMagma of M = the multMagma of G by Def22;

      hence carr(M) = carr(G) & op(M) = op(G);

      let a,b be Element of M, a9,b9 be Element of G;

      thus thesis by A1;

    end;

    registration

      let G be multMagma;

      cluster strict for MonoidalExtension of G;

      existence

      proof

        set g = the Element of G;

        set M = multLoopStr (# carr(G), op(G), g #);

         the multMagma of M = the multMagma of G;

        then M is MonoidalExtension of G by Def22;

        hence thesis;

      end;

    end

    theorem :: MONOID_0:19

    

     Th19: for G be non empty multMagma, M be MonoidalExtension of G holds (G is unital implies M is unital) & (G is commutative implies M is commutative) & (G is associative implies M is associative) & (G is invertible implies M is invertible) & (G is uniquely-decomposable implies M is uniquely-decomposable) & (G is cancelable implies M is cancelable)

    proof

      let G be non empty multMagma, M be MonoidalExtension of G;

      

       A1: the multMagma of M = the multMagma of G by Def22;

      thus G is unital implies M is unital by A1;

      thus G is commutative implies M is commutative by A1;

      thus G is associative implies M is associative by A1;

      thus G is invertible implies M is invertible by A1;

      thus G is uniquely-decomposable implies M is uniquely-decomposable by A1;

      assume op(G) is cancelable;

      hence op(M) is cancelable by A1;

    end;

    registration

      let G be constituted-Functions multMagma;

      cluster -> constituted-Functions for MonoidalExtension of G;

      coherence

      proof

        let M be MonoidalExtension of G;

        let a be Element of M;

         the multMagma of M = the multMagma of G by Def22;

        hence thesis;

      end;

    end

    registration

      let G be constituted-FinSeqs multMagma;

      cluster -> constituted-FinSeqs for MonoidalExtension of G;

      coherence

      proof

        let M be MonoidalExtension of G;

        let a be Element of M;

         the multMagma of M = the multMagma of G by Def22;

        hence thesis;

      end;

    end

    registration

      let G be unital non empty multMagma;

      cluster -> unital for MonoidalExtension of G;

      coherence by Th19;

    end

    registration

      let G be associative non empty multMagma;

      cluster -> associative for MonoidalExtension of G;

      coherence by Th19;

    end

    registration

      let G be commutative non empty multMagma;

      cluster -> commutative for MonoidalExtension of G;

      coherence by Th19;

    end

    registration

      let G be invertible non empty multMagma;

      cluster -> invertible for MonoidalExtension of G;

      coherence by Th19;

    end

    registration

      let G be cancelable non empty multMagma;

      cluster -> cancelable for MonoidalExtension of G;

      coherence by Th19;

    end

    registration

      let G be uniquely-decomposable non empty multMagma;

      cluster -> uniquely-decomposable for MonoidalExtension of G;

      coherence by Th19;

    end

    registration

      let G be unital non empty multMagma;

      cluster well-unital strict for MonoidalExtension of G;

      existence

      proof

        set M = multLoopStr (# carr(G), op(G), ( the_unity_wrt op(G)) #);

         the multMagma of M = the multMagma of G;

        then

        reconsider M as MonoidalExtension of G by Def22;

        take M;

        thus un(M) is_a_unity_wrt op(M) by Th4;

        thus thesis;

      end;

    end

    theorem :: MONOID_0:20

    

     Th20: for G be unital non empty multMagma holds for M1,M2 be well-unital strict MonoidalExtension of G holds M1 = M2

    proof

      let G be unital non empty multMagma;

      let M1,M2 be well-unital strict MonoidalExtension of G;

      

       A1: un(M1) = ( the_unity_wrt op(M1)) & un(M2) = ( the_unity_wrt op(M2)) by Th17;

       the multMagma of M1 = the multMagma of G & the multMagma of M2 = the multMagma of G by Def22;

      hence thesis by A1;

    end;

    begin

    definition

      let G be multMagma;

      :: MONOID_0:def23

      mode SubStr of G -> multMagma means

      : Def23: the multF of it c= the multF of G;

      existence ;

    end

    registration

      let G be multMagma;

      cluster strict for SubStr of G;

      existence

      proof

         the multMagma of G is SubStr of G by Def23;

        hence thesis;

      end;

    end

    registration

      let G be non empty multMagma;

      cluster strict non empty for SubStr of G;

      existence

      proof

         the multMagma of G is SubStr of G by Def23;

        hence thesis;

      end;

    end

    registration

      let G be unital non empty multMagma;

      cluster unital associative commutative cancelable idempotent invertible uniquely-decomposable strict for non empty SubStr of G;

      existence

      proof

        consider a be Element of G such that

         A1: for b be Element of G holds (a * b) = b & (b * a) = b by Th6;

        

         A2: a = (a * a) by A1;

        set f = the BinOp of {a};

        set H = multMagma (# {a}, f #);

        

         A3: ( dom op(G)) = [: carr(G), carr(G):] by FUNCT_2:def 1;

        f = ((a,a) .--> a) by Th3

        .= ( [a, a] .--> a);

        then op(H) c= op(G) by A2, A3, FUNCT_4: 7;

        then

        reconsider H as non empty SubStr of G by Def23;

        take H;

        thus op(H) is having_a_unity & op(H) is associative & op(H) is commutative & op(H) is cancelable & op(H) is idempotent & op(H) is invertible uniquely-decomposable by Th3;

        thus thesis;

      end;

    end

    definition

      let G be multMagma;

      :: MONOID_0:def24

      mode MonoidalSubStr of G -> multLoopStr means

      : Def24: the multF of it c= the multF of G & for M be multLoopStr st G = M holds ( 1. it ) = ( 1. M);

      existence

      proof

        set M = the MonoidalExtension of G;

         A1:

        now

          given M be multLoopStr such that

           A2: G = M;

          take M;

          thus op(M) c= op(G) by A2;

          thus for N be multLoopStr st G = N holds un(M) = un(N) by A2;

        end;

        

         A3: (ex M be multLoopStr st G = M) or for N be multLoopStr st G = N holds un(M) = un(N);

         the multMagma of M = the multMagma of G by Def22;

        hence thesis by A1, A3;

      end;

    end

    registration

      let G be multMagma;

      cluster strict for MonoidalSubStr of G;

      existence

      proof

        set N = the MonoidalSubStr of G;

         un(multLoopStr) = un(N);

        then

         A1: for M be multLoopStr st G = M holds un(multLoopStr) = un(M) by Def24;

         op(multLoopStr) c= op(G) by Def24;

        then the multLoopStr of N is MonoidalSubStr of G by A1, Def24;

        hence thesis;

      end;

    end

    registration

      let G be non empty multMagma;

      cluster strict non empty for MonoidalSubStr of G;

      existence

      proof

        per cases ;

          suppose G is multLoopStr;

          then

          reconsider L = G as multLoopStr;

          for N be multLoopStr st G = N holds ( 1. the multLoopStr of L) = ( 1. N);

          then

          reconsider M = the multLoopStr of L as MonoidalSubStr of G by Def24;

          take M;

          thus M is strict;

          thus the carrier of M is non empty;

        end;

          suppose

           A1: not G is multLoopStr;

          set M = the strict MonoidalExtension of G;

          

           A2: for N be multLoopStr st G = N holds ( 1. M) = ( 1. N) by A1;

           the multMagma of M = the multMagma of G by Def22;

          then

          reconsider M as MonoidalSubStr of G by A2, Def24;

          take M;

          thus thesis;

        end;

      end;

    end

    definition

      let M be multLoopStr;

      :: original: MonoidalSubStr

      redefine

      :: MONOID_0:def25

      mode MonoidalSubStr of M means

      : Def25: the multF of it c= the multF of M & ( 1. it ) = ( 1. M);

      compatibility

      proof

        let N be multLoopStr;

        thus N is MonoidalSubStr of M implies op(N) c= op(M) & un(N) = un(M)

        proof

          assume op(N) c= op(M) & for K be multLoopStr st M = K holds un(N) = un(K);

          hence thesis;

        end;

        assume op(N) c= op(M) & un(N) = un(M);

        hence op(N) c= op(M) & for K be multLoopStr st M = K holds un(N) = un(K);

      end;

    end

    registration

      let G be well-unital non empty multLoopStr;

      cluster well-unital associative commutative cancelable idempotent invertible uniquely-decomposable strict for non empty MonoidalSubStr of G;

      existence

      proof

        set a = un(G);

        reconsider e = a as Element of {a} by TARSKI:def 1;

        set f = the BinOp of {a};

        set H = multLoopStr (# {a}, f, e #);

        

         A1: a = (a * a) & ( dom op(G)) = [: carr(G), carr(G):] by Th16, FUNCT_2:def 1;

        ( [a, a] .--> a) = ( { [a, a]} --> a) & f = ((a,a) .--> a) by Th3;

        then ( 1. H) = ( 1. G) & op(H) c= op(G) by A1, FUNCT_4: 7;

        then

        reconsider H as non empty MonoidalSubStr of G by Def25;

        take H;

        now

          let b be Element of H;

          b = a by TARSKI:def 1;

          hence ( op(H) . ( un(H),b)) = b & ( op(H) . (b, un(H))) = b by TARSKI:def 1;

        end;

        hence un(H) is_a_unity_wrt op(H) by BINOP_1: 3;

        thus op(H) is associative & op(H) is commutative & op(H) is cancelable & op(H) is idempotent & op(H) is invertible uniquely-decomposable by Th3;

        thus thesis;

      end;

    end

    theorem :: MONOID_0:21

    

     Th21: for G be multMagma, M be MonoidalSubStr of G holds M is SubStr of G

    proof

      let G be multMagma, M be MonoidalSubStr of G;

      thus op(M) c= op(G) by Def24;

    end;

    definition

      let G be multMagma, M be MonoidalExtension of G;

      :: original: SubStr

      redefine

      mode SubStr of M -> SubStr of G ;

      coherence

      proof

        let N be SubStr of M;

         the multMagma of M = the multMagma of G by Def22;

        hence op(N) c= op(G) by Def23;

      end;

    end

    definition

      let G1 be multMagma, G2 be SubStr of G1;

      :: original: SubStr

      redefine

      mode SubStr of G2 -> SubStr of G1 ;

      coherence

      proof

        let G be SubStr of G2;

         op(G) c= op(G2) & op(G2) c= op(G1) by Def23;

        hence op(G) c= op(G1);

      end;

    end

    definition

      let G1 be multMagma, G2 be MonoidalSubStr of G1;

      :: original: SubStr

      redefine

      mode SubStr of G2 -> SubStr of G1 ;

      coherence

      proof

        reconsider H = G2 as SubStr of G1 by Th21;

        let G be SubStr of G2;

        G is SubStr of H;

        hence thesis;

      end;

    end

    definition

      let G be multMagma, M be MonoidalSubStr of G;

      :: original: MonoidalSubStr

      redefine

      mode MonoidalSubStr of M -> MonoidalSubStr of G ;

      coherence

      proof

        let M9 be MonoidalSubStr of M;

        

         A1: un(M9) = un(M) by Def24;

         op(M9) c= op(M) & op(M) c= op(G) by Def24;

        hence op(M9) c= op(G) & for N be multLoopStr st G = N holds un(M9) = un(N) by A1, Def24;

      end;

    end

    theorem :: MONOID_0:22

    G is SubStr of G & M is MonoidalSubStr of M

    proof

      thus op(G) c= op(G);

      thus op(M) c= op(M);

      thus thesis;

    end;

    reserve H for non empty SubStr of G,

N for non empty MonoidalSubStr of G;

    theorem :: MONOID_0:23

    

     Th23: the carrier of H c= the carrier of G & the carrier of N c= the carrier of G

    proof

      

       A1: ( dom op(N)) = [: carr(N), carr(N):] by FUNCT_2:def 1;

      

       A2: ( dom op(G)) = [: carr(G), carr(G):] by FUNCT_2:def 1;

       op(H) c= op(G) by Def23;

      then

       A3: ( dom op(H)) c= ( dom op(G)) by GRFUNC_1: 2;

      

       A4: ( dom op(H)) = [: carr(H), carr(H):] by FUNCT_2:def 1;

      thus carr(H) c= carr(G)

      proof

        let x be object;

        assume x in carr(H);

        then [x, x] in ( dom op(H)) by A4, ZFMISC_1: 87;

        hence thesis by A3, A2, ZFMISC_1: 87;

      end;

      let x be object;

       op(N) c= op(G) by Def24;

      then

       A5: ( dom op(N)) c= ( dom op(G)) by GRFUNC_1: 2;

      assume x in carr(N);

      then [x, x] in ( dom op(N)) by A1, ZFMISC_1: 87;

      hence thesis by A5, A2, ZFMISC_1: 87;

    end;

    theorem :: MONOID_0:24

    

     Th24: for G be non empty multMagma, H be non empty SubStr of G holds the multF of H = (the multF of G || the carrier of H)

    proof

      let G be non empty multMagma, H be non empty SubStr of G;

       op(H) c= op(G) & ( dom op(H)) = [: carr(H), carr(H):] by Def23, FUNCT_2:def 1;

      hence thesis by GRFUNC_1: 23;

    end;

    theorem :: MONOID_0:25

    

     Th25: for a,b be Element of H, a9,b9 be Element of G st a = a9 & b = b9 holds (a * b) = (a9 * b9)

    proof

      let a,b be Element of H, a9,b9 be Element of G such that

       A1: a = a9 & b = b9;

      

       A2: ( dom op(H)) = [: carr(H), carr(H):] & op(H) c= op(G) by Def23, FUNCT_2:def 1;

      

      thus (a * b) = ( op(H) . [a, b])

      .= (a9 * b9) by A1, A2, GRFUNC_1: 2;

    end;

    theorem :: MONOID_0:26

    

     Th26: for H1,H2 be non empty SubStr of G st the carrier of H1 = the carrier of H2 holds the multMagma of H1 = the multMagma of H2

    proof

      let H1,H2 be non empty SubStr of G;

      

       A1: op(H2) c= op(G) by Def23;

       op(H1) c= op(G) & ( dom op(H1)) = [: carr(H1), carr(H1):] by Def23, FUNCT_2:def 1;

      then

       A2: op(H1) = ( op(G) || carr(H1)) by GRFUNC_1: 23;

      assume

       A3: carr(H1) = carr(H2);

      then ( dom op(H2)) = [: carr(H1), carr(H1):] by FUNCT_2:def 1;

      hence thesis by A3, A1, A2, GRFUNC_1: 23;

    end;

    theorem :: MONOID_0:27

    for H1,H2 be non empty MonoidalSubStr of M st the carrier of H1 = the carrier of H2 holds the multLoopStr of H1 = the multLoopStr of H2

    proof

      let H1,H2 be non empty MonoidalSubStr of M such that

       A1: the carrier of H1 = the carrier of H2;

      reconsider N1 = H1, N2 = H2 as SubStr of M by Th21;

      

       A2: un(H1) = un(M) & un(H2) = un(M) by Def25;

       the multMagma of N1 = the multMagma of N2 by A1, Th26;

      hence thesis by A2;

    end;

    theorem :: MONOID_0:28

    

     Th28: for H1,H2 be non empty SubStr of G st the carrier of H1 c= the carrier of H2 holds H1 is SubStr of H2

    proof

      let H1,H2 be non empty SubStr of G;

      assume carr(H1) c= carr(H2);

      then [: carr(H1), carr(H1):] c= [: carr(H2), carr(H2):] by ZFMISC_1: 96;

      then

       A1: (( op(G) || carr(H2)) || carr(H1)) = ( op(G) || carr(H1)) by FUNCT_1: 51;

       op(H2) c= op(G) & ( dom op(H2)) = [: carr(H2), carr(H2):] by Def23, FUNCT_2:def 1;

      then

       A2: op(H2) = ( op(G) || carr(H2)) by GRFUNC_1: 23;

       op(H1) c= op(G) & ( dom op(H1)) = [: carr(H1), carr(H1):] by Def23, FUNCT_2:def 1;

      then op(H1) = ( op(G) || carr(H1)) by GRFUNC_1: 23;

      hence op(H1) c= op(H2) by A1, A2, RELAT_1: 59;

    end;

    theorem :: MONOID_0:29

    for H1,H2 be non empty MonoidalSubStr of M st the carrier of H1 c= the carrier of H2 holds H1 is MonoidalSubStr of H2

    proof

      let H1,H2 be non empty MonoidalSubStr of M such that

       A1: carr(H1) c= carr(H2);

      H1 is SubStr of M & H2 is SubStr of M by Th21;

      then H1 is SubStr of H2 by A1, Th28;

      hence op(H1) c= op(H2) by Def23;

       un(H1) = un(M) by Def25;

      hence thesis by Def25;

    end;

    theorem :: MONOID_0:30

    

     Th30: G is unital & ( the_unity_wrt the multF of G) in the carrier of H implies H is unital & ( the_unity_wrt the multF of G) = ( the_unity_wrt the multF of H)

    proof

      set e9 = ( the_unity_wrt op(G));

      assume G is unital;

      then

       A1: e9 is_a_unity_wrt op(G) by Th4;

      assume ( the_unity_wrt op(G)) in carr(H);

      then

      reconsider e = ( the_unity_wrt op(G)) as Element of H;

       A2:

      now

        let a be Element of H;

         carr(H) c= carr(G) by Th23;

        then

        reconsider a9 = a as Element of G;

        

        thus (e * a) = (e9 * a9) by Th25

        .= a by A1, BINOP_1: 3;

        

        thus (a * e) = (a9 * e9) by Th25

        .= a by A1, BINOP_1: 3;

      end;

      hence H is unital;

      now

        let a be Element of H;

        (e * a) = ( op(H) . (e,a)) & (a * e) = ( op(H) . (a,e));

        hence ( op(H) . (e,a)) = a & ( op(H) . (a,e)) = a by A2;

      end;

      then e is_a_unity_wrt op(H) by BINOP_1: 3;

      hence thesis by BINOP_1:def 8;

    end;

    theorem :: MONOID_0:31

    

     Th31: for M be well-unital non empty multLoopStr holds for N be non empty MonoidalSubStr of M holds N is well-unital

    proof

      let M be well-unital non empty multLoopStr, N be non empty MonoidalSubStr of M;

      

       A1: un(M) is_a_unity_wrt op(M) by Def21;

      

       A2: N is SubStr of M & un(N) = un(M) by Def24, Th21;

      now

        let a be Element of N;

         carr(N) c= carr(M) by Th23;

        then

        reconsider a9 = a as Element of M;

        

        thus ( op(N) . ( un(N),a)) = ( un(N) * a)

        .= ( un(M) * a9) by A2, Th25

        .= a by A1, BINOP_1: 3;

        

        thus ( op(N) . (a, un(N))) = (a * un(N))

        .= (a9 * un(M)) by A2, Th25

        .= a by A1, BINOP_1: 3;

      end;

      hence un(N) is_a_unity_wrt op(N) by BINOP_1: 3;

    end;

    theorem :: MONOID_0:32

    

     Th32: G is commutative implies H is commutative

    proof

      assume

       A1: G is commutative;

      now

        let a,b be Element of H;

         carr(H) c= carr(G) by Th23;

        then

        reconsider a9 = a, b9 = b as Element of G;

        

        thus (a * b) = (a9 * b9) by Th25

        .= (b9 * a9) by A1

        .= (b * a) by Th25;

      end;

      hence thesis;

    end;

    theorem :: MONOID_0:33

    

     Th33: G is associative implies H is associative

    proof

      assume

       A1: G is associative;

      now

        let a,b,c be Element of H;

         carr(H) c= carr(G) by Th23;

        then

        reconsider a9 = a, b9 = b, c9 = c, ab = (a * b), bc = (b * c) as Element of G;

        

        thus ((a * b) * c) = (ab * c9) by Th25

        .= ((a9 * b9) * c9) by Th25

        .= (a9 * (b9 * c9)) by A1

        .= (a9 * bc) by Th25

        .= (a * (b * c)) by Th25;

      end;

      hence thesis;

    end;

    theorem :: MONOID_0:34

    

     Th34: G is idempotent implies H is idempotent

    proof

      assume

       A1: G is idempotent;

      

       A2: carr(H) c= carr(G) by Th23;

      now

        let a be Element of H;

        reconsider a9 = a as Element of G by A2;

        

        thus (a * a) = (a9 * a9) by Th25

        .= a by A1, Th7;

      end;

      hence thesis by Th7;

    end;

    theorem :: MONOID_0:35

    

     Th35: G is cancelable implies H is cancelable

    proof

      assume

       A1: G is cancelable;

      

       A2: carr(H) c= carr(G) by Th23;

      now

        let a,b,c be Element of H;

        reconsider a9 = a, b9 = b, c9 = c as Element of G by A2;

        

         A3: (b * a) = (b9 * a9) & (c * a) = (c9 * a9) by Th25;

        (a * b) = (a9 * b9) & (a * c) = (a9 * c9) by Th25;

        hence (a * b) = (a * c) or (b * a) = (c * a) implies b = c by A1, A3, Th13;

      end;

      hence thesis by Th13;

    end;

    theorem :: MONOID_0:36

    

     Th36: ( the_unity_wrt the multF of G) in the carrier of H & G is uniquely-decomposable implies H is uniquely-decomposable

    proof

      assume

       A1: ( the_unity_wrt op(G)) in carr(H);

      assume that

       A2: op(G) is having_a_unity and

       A3: for a,b be Element of G st ( op(G) . (a,b)) = ( the_unity_wrt op(G)) holds a = b & b = ( the_unity_wrt op(G));

      

       A4: G is unital by A2;

      then H is unital by A1, Th30;

      hence op(H) is having_a_unity;

      let a,b be Element of H;

       carr(H) c= carr(G) by Th23;

      then

      reconsider a9 = a, b9 = b as Element of G;

      

       A5: ( op(H) . (a,b)) = (a * b)

      .= (a9 * b9) by Th25

      .= ( op(G) . (a9,b9));

      ( the_unity_wrt op(G)) = ( the_unity_wrt op(H)) by A1, A4, Th30;

      hence thesis by A3, A5;

    end;

    theorem :: MONOID_0:37

    

     Th37: for M be well-unital uniquely-decomposable non empty multLoopStr holds for N be non empty MonoidalSubStr of M holds N is uniquely-decomposable

    proof

      let M be well-unital uniquely-decomposable non empty multLoopStr;

      let N be non empty MonoidalSubStr of M;

      

       A1: un(M) = un(N) by Def25;

      N is SubStr of M & un(M) = ( the_unity_wrt op(M)) by Th17, Th21;

      hence thesis by A1, Th36;

    end;

    registration

      let G be constituted-Functions non empty multMagma;

      cluster -> constituted-Functions for non empty SubStr of G;

      coherence

      proof

        let H be non empty SubStr of G;

        let a be Element of H;

         carr(H) c= carr(G) by Th23;

        then a is Element of G;

        hence thesis;

      end;

      cluster -> constituted-Functions for non empty MonoidalSubStr of G;

      coherence

      proof

        let H be non empty MonoidalSubStr of G;

        let a be Element of H;

         carr(H) c= carr(G) by Th23;

        then a is Element of G;

        hence thesis;

      end;

    end

    registration

      let G be constituted-FinSeqs non empty multMagma;

      cluster -> constituted-FinSeqs for non empty SubStr of G;

      coherence

      proof

        let H be non empty SubStr of G;

        let a be Element of H;

         carr(H) c= carr(G) by Th23;

        then a is Element of G;

        hence thesis;

      end;

      cluster -> constituted-FinSeqs for non empty MonoidalSubStr of G;

      coherence

      proof

        let H be non empty MonoidalSubStr of G;

        let a be Element of H;

         carr(H) c= carr(G) by Th23;

        then a is Element of G;

        hence thesis;

      end;

    end

    registration

      let M be well-unital non empty multLoopStr;

      cluster -> well-unital for non empty MonoidalSubStr of M;

      coherence by Th31;

    end

    registration

      let G be commutative non empty multMagma;

      cluster -> commutative for non empty SubStr of G;

      coherence by Th32;

      cluster -> commutative for non empty MonoidalSubStr of G;

      coherence

      proof

        let N be non empty MonoidalSubStr of G;

        N is SubStr of G by Th21;

        hence thesis;

      end;

    end

    registration

      let G be associative non empty multMagma;

      cluster -> associative for non empty SubStr of G;

      coherence by Th33;

      cluster -> associative for non empty MonoidalSubStr of G;

      coherence

      proof

        let N be non empty MonoidalSubStr of G;

        N is SubStr of G by Th21;

        hence thesis;

      end;

    end

    registration

      let G be idempotent non empty multMagma;

      cluster -> idempotent for non empty SubStr of G;

      coherence by Th34;

      cluster -> idempotent for non empty MonoidalSubStr of G;

      coherence

      proof

        let N be non empty MonoidalSubStr of G;

        N is SubStr of G by Th21;

        hence thesis;

      end;

    end

    registration

      let G be cancelable non empty multMagma;

      cluster -> cancelable for non empty SubStr of G;

      coherence by Th35;

      cluster -> cancelable for non empty MonoidalSubStr of G;

      coherence

      proof

        let N be non empty MonoidalSubStr of G;

        N is SubStr of G by Th21;

        hence thesis;

      end;

    end

    registration

      let M be well-unital uniquely-decomposable non empty multLoopStr;

      cluster -> uniquely-decomposable for non empty MonoidalSubStr of M;

      coherence by Th37;

    end

     Lm5:

    now

      let G be non empty multMagma, D be non empty Subset of G;

      assume

       A1: for x,y be Element of D holds (x * y) in D;

      thus ex H be strict non empty SubStr of G st the carrier of H = D

      proof

        set op = the multF of G, carr = the carrier of G;

        

         A2: ( dom op) = [:carr, carr:] by FUNCT_2:def 1;

        

         A3: ( rng (op || D)) c= D

        proof

          let x be object;

          assume x in ( rng (op || D));

          then

          consider y be object such that

           A4: y in ( dom (op || D)) and

           A5: x = ((op || D) . y) by FUNCT_1:def 3;

          reconsider y as Element of [:D, D:] by A2, A4, RELAT_1: 62;

          reconsider y1 = (y `1 ), y2 = (y `2 ) as Element of D;

          y = [y1, y2] by MCART_1: 21;

          then x = (y1 * y2) by A4, A5, FUNCT_1: 47;

          hence thesis by A1;

        end;

        ( dom (op || D)) = [:D, D:] by A2, RELAT_1: 62;

        then

        reconsider f = (op || D) as BinOp of D by A3, FUNCT_2:def 1, RELSET_1: 4;

        f c= op by RELAT_1: 59;

        then

        reconsider H = multMagma (# D, f #) as strict non empty SubStr of G by Def23;

        take H;

        thus thesis;

      end;

    end;

    scheme :: MONOID_0:sch1

    SubStrEx2 { G() -> non empty multMagma , P[ object] } :

ex H be strict non empty SubStr of G() st for x be Element of G() holds x in the carrier of H iff P[x]

      provided

       A1: for x,y be Element of G() holds P[x] & P[y] implies P[(x * y)]

       and

       A2: ex x be Element of G() st P[x];

      consider X such that

       A3: for x be object holds x in X iff x in carr(G) & P[x] from XBOOLE_0:sch 1;

      reconsider X as non empty set by A2, A3;

      X c= carr(G) by A3;

      then

      reconsider X as non empty Subset of G();

       A4:

      now

        let x,y be Element of X;

        P[x] & P[y] by A3;

        then P[(x * y)] by A1;

        hence (x * y) in X by A3;

      end;

      consider H be strict non empty SubStr of G() such that

       A5: the carrier of H = X by Lm5, A4;

      take H;

      thus thesis by A3, A5;

    end;

    scheme :: MONOID_0:sch2

    MonoidalSubStrEx2 { G() -> non empty multLoopStr , P[ set] } :

ex M be strict non empty MonoidalSubStr of G() st for x be Element of G() holds x in the carrier of M iff P[x]

      provided

       A1: for x,y be Element of G() holds P[x] & P[y] implies P[(x * y)]

       and

       A2: P[( 1. G())];

      reconsider G = G() as non empty multMagma;

      

       A3: ex x be Element of G st P[x] by A2;

      

       A4: for x,y be Element of G holds P[x] & P[y] implies P[(x * y)] by A1;

      consider H be strict non empty SubStr of G such that

       A5: for x be Element of G holds x in the carrier of H iff P[x] from SubStrEx2( A4, A3);

      reconsider e = ( 1. G()) as Element of H by A2, A5;

      set M = multLoopStr (# carr(H), op(H), e #);

      ( 1. G()) = ( 1. M) & the multF of H c= the multF of G() by Def23;

      then

      reconsider M as strict non empty MonoidalSubStr of G() by Def25;

      take M;

      thus thesis by A5;

    end;

    notation

      let G be multMagma, a,b be Element of G;

      synonym a [*] b for a * b;

    end

    begin

    definition

      :: MONOID_0:def26

      func <REAL,+> -> non empty multMagma equals multMagma (# REAL , addreal #);

      coherence ;

    end

    registration

      cluster <REAL,+> -> unital associative invertible commutative cancelable strict;

      coherence by GROUP_1: 46;

    end

    theorem :: MONOID_0:38

    x is Element of <REAL,+> iff x is Element of REAL ;

    theorem :: MONOID_0:39

    

     Th39: for N be non empty SubStr of <REAL,+> holds for a,b be Element of N, x,y be Real st a = x & b = y holds (a * b) = (x + y)

    proof

      let N be non empty SubStr of <REAL,+> ;

      let a,b be Element of N;

       carr(N) c= carr(<REAL,+>) by Th23;

      then

      reconsider a9 = a, b9 = b as Element of <REAL,+> ;

      (a * b) = (a9 * b9) by Th25;

      hence thesis by BINOP_2:def 9;

    end;

    theorem :: MONOID_0:40

    

     Th40: for N be unital non empty SubStr of <REAL,+> holds ( the_unity_wrt the multF of N) = 0

    proof

      let N be unital non empty SubStr of <REAL,+> ;

      consider a be Element of N such that

       A1: for b be Element of N holds (a * b) = b & (b * a) = b by Th6;

       carr(N) c= REAL by Th23;

      then

      reconsider x = a as Real;

      now

        let b be Element of N;

        (a * b) = ( op(N) . (a,b)) & (b * a) = ( op(N) . (b,a));

        hence ( op(N) . (a,b)) = b & ( op(N) . (b,a)) = b by A1;

      end;

      then

       A2: a is_a_unity_wrt op(N) by BINOP_1: 3;

      (x + 0 ) = (a * a) by A1

      .= (x + x) by Th39;

      hence thesis by A2, BINOP_1:def 8;

    end;

    registration

      let G be unital non empty multMagma;

      cluster associative invertible -> unital cancelable Group-like for non empty SubStr of G;

      coherence ;

    end

    definition

      :: original: INT.Group

      redefine

      func INT.Group -> strict non empty SubStr of <REAL,+> ;

      coherence

      proof

        ( dom addreal ) = [: REAL , REAL :] by FUNCT_2:def 1;

        then

         A1: ( dom ( addreal || INT )) = [: INT , INT :] by NUMBERS: 15, RELAT_1: 62, ZFMISC_1: 96;

         A2:

        now

          let x be object;

          assume

           A3: x in [: INT , INT :];

          then

           A4: x = [(x `1 ), (x `2 )] by MCART_1: 21;

          reconsider i1 = (x `1 ), i2 = (x `2 ) as Element of INT by A3, MCART_1: 10;

          

          thus ( addint . x) = ( addint . (i1,i2)) by A3, MCART_1: 21

          .= ( addreal . (i1,i2)) by GR_CY_1:def 1

          .= (( addreal || INT ) . x) by A1, A3, A4, FUNCT_1: 47;

        end;

        ( dom addint ) = [: INT , INT :] by FUNCT_2:def 1;

        then addint = ( addreal || INT ) by A1, A2, FUNCT_1: 2;

        then op(INT.Group) c= op(<REAL,+>) by GR_CY_1:def 3, RELAT_1: 59;

        hence thesis by Def23;

      end;

    end

    theorem :: MONOID_0:41

    for G be strict non empty SubStr of <REAL,+> holds G = INT.Group iff the carrier of G = INT by Th26, GR_CY_1:def 3;

    theorem :: MONOID_0:42

    x is Element of INT.Group iff x is Integer by GR_CY_1:def 3, INT_1:def 2;

    definition

      :: MONOID_0:def27

      func <NAT,+> -> unital uniquely-decomposable strict non empty SubStr of INT.Group means

      : Def27: the carrier of it = NAT ;

      existence

      proof

        set f = ( addint || NAT );

        ( dom addint ) = [: INT , INT :] by FUNCT_2:def 1;

        then

         A1: ( dom f) = [: NAT , NAT :] by NUMBERS: 17, RELAT_1: 62, ZFMISC_1: 96;

        ( rng f) c= NAT

        proof

          let x be object;

          assume x in ( rng f);

          then

          consider y be object such that

           A2: y in ( dom f) and

           A3: x = (f . y) by FUNCT_1:def 3;

          reconsider n1 = (y `1 ), n2 = (y `2 ) as Element of NAT by A1, A2, MCART_1: 10;

          reconsider i1 = n1, i2 = n2 as Integer;

          x = ( addint . y) by A2, A3, FUNCT_1: 47

          .= ( addint . (i1,i2)) by A1, A2, MCART_1: 21

          .= (n1 + n2) by BINOP_2:def 20;

          hence thesis by ORDINAL1:def 12;

        end;

        then

        reconsider f as BinOp of NAT by A1, FUNCT_2:def 1, RELSET_1: 4;

        f c= op(INT.Group) by GR_CY_1:def 3, RELAT_1: 59;

        then

        reconsider N = multMagma (# NAT , f #) as strict non empty SubStr of INT.Group by Def23;

        reconsider a = 0 as Element of N;

         A4:

        now

          let b be Element of N;

          reconsider n = b as Element of NAT ;

          

          thus (a * b) = ( 0 + n) by Th39

          .= b;

          

          thus (b * a) = (n + 0 ) by Th39

          .= b;

        end;

        now

          let b be Element of N;

          

          thus ( op(N) . (a,b)) = (a * b)

          .= b by A4;

          

          thus ( op(N) . (b,a)) = (b * a)

          .= b by A4;

        end;

        then

         A5: a is_a_unity_wrt op(N) by BINOP_1: 3;

        then

         A6: ( the_unity_wrt op(N)) = a by BINOP_1:def 8;

         A7:

        now

          let a,b be Element of N such that

           A8: (a * b) = ( the_unity_wrt op(N));

          reconsider n = a, m = b as Element of NAT ;

          

           A9: (a * b) = (n + m) by Th39;

          then a = 0 by A6, A8;

          hence a = b & b = ( the_unity_wrt op(N)) by A5, A8, A9, BINOP_1:def 8;

        end;

        

         A10: N is unital by A4;

        then N is uniquely-decomposable by A7, Th14;

        hence thesis by A10;

      end;

      uniqueness by Th26;

    end

    definition

      :: MONOID_0:def28

      func <NAT,+,0> -> well-unital strict non empty MonoidalExtension of <NAT,+> means not contradiction;

      existence ;

      uniqueness by Th20;

    end

    definition

      :: original: addnat

      redefine

      :: MONOID_0:def29

      func addnat equals the multF of <NAT,+> ;

      compatibility

      proof

        let b be BinOp of NAT ;

        

         A1: the carrier of <NAT,+> = NAT by Def27;

        now

          let n1,n2 be Element of NAT ;

          

          thus ( addnat . (n1,n2)) = (n1 + n2) by BINOP_2:def 23

          .= ( addint . (n1,n2)) by BINOP_2:def 20

          .= (( addint || NAT ) . [n1, n2]) by FUNCT_1: 49

          .= (the multF of <NAT,+> . (n1,n2)) by A1, Th24, GR_CY_1:def 3;

        end;

        hence thesis by A1, BINOP_1: 2;

      end;

    end

    theorem :: MONOID_0:43

    

     Th43: <NAT,+> = multMagma (# NAT , addnat #) by Def27;

    theorem :: MONOID_0:44

    x is Element of <NAT,+,0> iff x is Element of NAT

    proof

       carr(<NAT,+,0>) = carr(<NAT,+>) by Th18

      .= NAT by Def27;

      hence thesis;

    end;

    theorem :: MONOID_0:45

    for n1,n2 be Element of NAT , m1,m2 be Element of <NAT,+,0> st n1 = m1 & n2 = m2 holds (m1 * m2) = (n1 + n2)

    proof

       op(<NAT,+,0>) = op(<NAT,+>) by Th18;

      then <NAT,+,0> is SubStr of <NAT,+> qua SubStr of <REAL,+> by Def23;

      hence thesis by Th39;

    end;

    theorem :: MONOID_0:46

     <NAT,+,0> = multLoopStr (# NAT , addnat , 0 #)

    proof

      set N = <NAT,+,0> ;

       the multMagma of N = <NAT,+> & ( the_unity_wrt op(N)) = un(N) by Def22, Th17;

      hence thesis by Th40, Th43;

    end;

    theorem :: MONOID_0:47

     addnat = ( addreal || NAT ) & addnat = ( addint || NAT )

    proof

       carr(<NAT,+>) = NAT by Def27;

      hence thesis by Th24, GR_CY_1:def 3;

    end;

    theorem :: MONOID_0:48

     0 is_a_unity_wrt addnat & addnat is uniquely-decomposable

    proof

      ( the_unity_wrt addnat ) = 0 & ex n be Element of NAT st n is_a_unity_wrt addnat by Th40, Th43, SETWISEO:def 2;

      hence 0 is_a_unity_wrt addnat by BINOP_1:def 8;

      thus thesis by Def20, Th43;

    end;

    definition

      :: MONOID_0:def30

      func <REAL,*> -> unital commutative associative strict non empty multMagma equals multMagma (# REAL , multreal #);

      coherence by Def10, Def11, Def12;

    end

    theorem :: MONOID_0:49

    x is Element of <REAL,*> iff x is Element of REAL ;

    theorem :: MONOID_0:50

    

     Th50: for N be non empty SubStr of <REAL,*> holds for a,b be Element of N, x,y be Real st a = x & b = y holds (a * b) = (x * y)

    proof

      let N be non empty SubStr of <REAL,*> ;

      let a,b be Element of N;

       carr(N) c= carr(<REAL,*>) by Th23;

      then

      reconsider a9 = a, b9 = b as Element of <REAL,*> ;

      (a * b) = (a9 * b9) by Th25;

      hence thesis by BINOP_2:def 11;

    end;

    theorem :: MONOID_0:51

    for N be unital non empty SubStr of <REAL,*> holds ( the_unity_wrt the multF of N) = 0 or ( the_unity_wrt the multF of N) = 1

    proof

      let N be unital non empty SubStr of <REAL,*> ;

      set e = ( the_unity_wrt op(N));

       carr(N) c= carr(<REAL,*>) by Th23;

      then

      reconsider x = e as Real;

      e is_a_unity_wrt op(N) by Th4;

      

      then e = (e * e) by BINOP_1: 3

      .= (x * x) by Th50;

      then (x * 1) = (x * x);

      hence thesis by XCMPLX_1: 5;

    end;

    definition

      :: MONOID_0:def31

      func <NAT,*> -> unital uniquely-decomposable strict non empty SubStr of <REAL,*> means

      : Def31: the carrier of it = NAT ;

      existence

      proof

        set f = ( multreal || NAT );

        

         A1: ( dom multreal ) = [: REAL , REAL :] by FUNCT_2:def 1;

         [: NAT , NAT :] c= [: REAL , REAL :] by ZFMISC_1: 96, NUMBERS: 19;

        then

         A2: ( dom f) = [: NAT , NAT :] by RELAT_1: 62, A1;

        ( rng f) c= NAT

        proof

          let x be object;

          assume x in ( rng f);

          then

          consider y be object such that

           A3: y in ( dom f) and

           A4: x = (f . y) by FUNCT_1:def 3;

          reconsider n1 = (y `1 ), n2 = (y `2 ) as Element of NAT by A2, A3, MCART_1: 10;

          x = ( multreal . y) by A3, A4, FUNCT_1: 47

          .= ( multreal . (n1,n2)) by A2, A3, MCART_1: 21

          .= (n1 * n2) by BINOP_2:def 11;

          hence thesis by ORDINAL1:def 12;

        end;

        then

        reconsider f as BinOp of NAT by A2, FUNCT_2:def 1, RELSET_1: 4;

        f c= op(<REAL,*>) by RELAT_1: 59;

        then

        reconsider N = multMagma (# NAT , f #) as strict non empty SubStr of <REAL,*> by Def23;

        reconsider a = 1 as Element of N;

         A5:

        now

          let b be Element of N;

          reconsider n = b as Element of NAT ;

          

          thus (a * b) = (1 * n) by Th50

          .= b;

          

          thus (b * a) = (n * 1) by Th50

          .= b;

        end;

        now

          let b be Element of N;

          

          thus ( op(N) . (a,b)) = (a * b)

          .= b by A5;

          

          thus ( op(N) . (b,a)) = (b * a)

          .= b by A5;

        end;

        then

         A6: a is_a_unity_wrt op(N) by BINOP_1: 3;

        then

         A7: ( the_unity_wrt op(N)) = a by BINOP_1:def 8;

         A8:

        now

          let a,b be Element of N such that

           A9: (a * b) = ( the_unity_wrt op(N));

          reconsider n = a, m = b as Element of NAT ;

          

           A10: (a * b) = (n * m) by Th50;

          then a = 1 by A7, A9, NAT_1: 15;

          hence a = b & b = ( the_unity_wrt op(N)) by A6, A9, A10, BINOP_1:def 8;

        end;

        

         A11: N is unital by A5;

        then N is uniquely-decomposable by A8, Th14;

        hence thesis by A11;

      end;

      uniqueness by Th26;

    end

    definition

      :: MONOID_0:def32

      func <NAT,*,1> -> well-unital strict non empty MonoidalExtension of <NAT,*> means not contradiction;

      uniqueness by Th20;

      existence ;

    end

    definition

      :: original: multnat

      redefine

      :: MONOID_0:def33

      func multnat equals the multF of <NAT,*> ;

      compatibility

      proof

        let b be BinOp of NAT ;

        

         A1: the carrier of <NAT,*> = NAT by Def31;

        now

          let n1,n2 be Element of NAT ;

          

          thus ( multnat . (n1,n2)) = (n1 * n2) by BINOP_2:def 24

          .= ( multreal . (n1,n2)) by BINOP_2:def 11

          .= (( multreal || NAT ) . [n1, n2]) by FUNCT_1: 49

          .= (the multF of <NAT,*> . (n1,n2)) by A1, Th24;

        end;

        hence thesis by A1, BINOP_1: 2;

      end;

    end

    theorem :: MONOID_0:52

    

     Th52: <NAT,*> = multMagma (# NAT , multnat #) by Def31;

    theorem :: MONOID_0:53

    for n1,n2 be Element of NAT , m1,m2 be Element of <NAT,*> st n1 = m1 & n2 = m2 holds (m1 * m2) = (n1 * n2) by Th50;

    theorem :: MONOID_0:54

    

     Th54: ( the_unity_wrt the multF of <NAT,*> ) = 1

    proof

       carr(<NAT,*>) = NAT by Def31;

      hence thesis by Th30, BINOP_2: 7;

    end;

    theorem :: MONOID_0:55

    for n1,n2 be Element of NAT , m1,m2 be Element of <NAT,*,1> st n1 = m1 & n2 = m2 holds (m1 * m2) = (n1 * n2)

    proof

      let n1,n2 be Element of NAT , m1,m2 be Element of <NAT,*,1> ;

       the multMagma of <NAT,*,1> = <NAT,*> by Def22;

      then

      reconsider x1 = m1, x2 = m2 as Element of <NAT,*> ;

      (x1 * x2) = (m1 * m2) by Th18;

      hence thesis by Th50;

    end;

    theorem :: MONOID_0:56

     <NAT,*,1> = multLoopStr (# NAT , multnat , 1 #)

    proof

      set N = <NAT,*,1> ;

       the multMagma of N = <NAT,*> & ( the_unity_wrt op(N)) = un(N) by Def22, Th17;

      hence thesis by Def31, Th54;

    end;

    theorem :: MONOID_0:57

     multnat = ( multreal || NAT ) by Th24, Th52;

    theorem :: MONOID_0:58

    1 is_a_unity_wrt multnat & multnat is uniquely-decomposable

    proof

      ex n be Element of NAT st n is_a_unity_wrt multnat by SETWISEO:def 2;

      hence 1 is_a_unity_wrt multnat by Th52, Th54, BINOP_1:def 8;

      thus thesis by Def20, Th52;

    end;

    begin

    definition

      let D be non empty set;

      :: MONOID_0:def34

      func D *+^ -> unital associative cancelable uniquely-decomposable constituted-FinSeqs strict non empty multMagma means

      : Def34: the carrier of it = (D * ) & for p,q be Element of it holds (p [*] q) = (p ^ q);

      existence

      proof

        deffunc F( Element of (D * ), Element of (D * )) = ($1 qua Element of (D * ) ^ $2 qua Element of (D * ));

        consider f be BinOp of (D * ) such that

         A1: for a,b be Element of (D * ) holds (f . (a,b)) = F(a,b) from BINOP_1:sch 4;

        set G = multMagma (# (D * ), f #);

        G is constituted-FinSeqs;

        then

        reconsider G as constituted-FinSeqs strict non empty multMagma;

        G is unital associative cancelable uniquely-decomposable

        proof

          set N = G, f = op(N);

          ( <*> D) = {} ;

          then

          reconsider a = {} as Element of N by FINSEQ_1:def 11;

           A2:

          now

            let b be Element of N;

            

            thus (a [*] b) = (a ^ b) by A1

            .= b by FINSEQ_1: 34;

            

            thus (b [*] a) = (b ^ a) by A1

            .= b by FINSEQ_1: 34;

          end;

          hence N is unital;

          now

            let a,b,c be Element of N;

            reconsider p = (a [*] b), q = (b [*] c) as Element of N;

            

            thus ((a * b) * c) = (p ^ c) by A1

            .= ((a ^ b) ^ c) by A1

            .= (a ^ (b ^ c)) by FINSEQ_1: 32

            .= (a ^ q) by A1

            .= (a * (b * c)) by A1;

          end;

          hence N is associative;

          now

            let a,b,c be Element of N;

            

             A3: (b * a) = (b ^ a) & (c * a) = (c ^ a) by A1;

            (a * b) = (a ^ b) & (a * c) = (a ^ c) by A1;

            hence (a * b) = (a * c) or (b * a) = (c * a) implies b = c by A3, FINSEQ_1: 33;

          end;

          hence N is cancelable by Th13;

          N is unital by A2;

          hence op(N) is having_a_unity;

          let a9,b be Element of N;

          now

            let b be Element of N;

            (a [*] b) = (f . (a,b)) & (b [*] a) = (f . (b,a));

            hence (f . (a,b)) = b & (f . (b,a)) = b by A2;

          end;

          then

           A4: a is_a_unity_wrt op(N) by BINOP_1: 3;

          assume (f . (a9,b)) = ( the_unity_wrt op(N));

          

          then

           A5: {} = (a9 [*] b) by A4, BINOP_1:def 8

          .= (a9 ^ b) by A1;

          then a = b;

          hence thesis by A4, A5, BINOP_1:def 8;

        end;

        then

        reconsider G as unital associative cancelable uniquely-decomposable constituted-FinSeqs strict non empty multMagma;

        take G;

        thus thesis by A1;

      end;

      uniqueness

      proof

        let G1,G2 be unital associative cancelable uniquely-decomposable constituted-FinSeqs strict non empty multMagma such that

         A6: carr(G1) = (D * ) and

         A7: for p,q be Element of G1 holds (p [*] q) = (p ^ q) and

         A8: carr(G2) = (D * ) and

         A9: for p,q be Element of G2 holds (p [*] q) = (p ^ q);

        set f1 = op(G1), f2 = op(G2);

        now

          let a,b be Element of (D * );

          reconsider a2 = a, b2 = b as Element of G2 by A8;

          reconsider a1 = a, b1 = b as Element of G1 by A6;

          reconsider p = a, q = b as Element of (D * );

          (a2 [*] b2) = (p ^ q) & (a1 [*] b1) = (p ^ q) by A7, A9;

          hence (f1 . (a,b)) = (f2 . (a,b));

        end;

        hence thesis by A6, A8, BINOP_1: 2;

      end;

    end

    definition

      let D;

      :: MONOID_0:def35

      func D *+^+<0> -> well-unital strict non empty MonoidalExtension of (D *+^ ) means not contradiction;

      correctness by Th20;

      :: MONOID_0:def36

      func D -concatenation -> BinOp of (D * ) equals the multF of (D *+^ );

      correctness

      proof

         carr(*+^) = (D * ) by Def34;

        hence thesis;

      end;

    end

    theorem :: MONOID_0:59

    (D *+^ ) = multMagma (# (D * ), (D -concatenation ) #) by Def34;

    theorem :: MONOID_0:60

    

     Th60: ( the_unity_wrt the multF of (D *+^ )) = {}

    proof

      set N = (D *+^ ), f = op(N);

       carr(N) = (D * ) & {} = ( <*> D) by Def34;

      then

      reconsider a = {} as Element of N by FINSEQ_1:def 11;

      now

        let b be Element of N;

        

        thus (f . (a,b)) = (a [*] b)

        .= ( {} ^ b) by Def34

        .= b by FINSEQ_1: 34;

        

        thus (f . (b,a)) = (b [*] a)

        .= (b ^ {} ) by Def34

        .= b by FINSEQ_1: 34;

      end;

      then a is_a_unity_wrt op(N) by BINOP_1: 3;

      hence thesis by BINOP_1:def 8;

    end;

    theorem :: MONOID_0:61

    the carrier of (D *+^+<0> ) = (D * ) & the multF of (D *+^+<0> ) = (D -concatenation ) & ( 1. (D *+^+<0> )) = {}

    proof

      set M = (D *+^+<0> );

       the multMagma of M = (D *+^ ) & ( the_unity_wrt op(M)) = un(M) by Def22, Th17;

      hence thesis by Def34, Th60;

    end;

    theorem :: MONOID_0:62

    for a,b be Element of (D *+^+<0> ) holds (a [*] b) = (a ^ b)

    proof

      let a,b be Element of (D *+^+<0> );

       the multMagma of (D *+^+<0> ) = (D *+^ ) by Def22;

      then

      reconsider p = a, q = b as Element of (D *+^ );

      

      thus (a [*] b) = (p [*] q) by Th18

      .= (a ^ b) by Def34;

    end;

    theorem :: MONOID_0:63

    

     Th63: for F be non empty SubStr of (D *+^ ) holds for p,q be Element of F holds (p [*] q) = (p ^ q)

    proof

      let F be non empty SubStr of (D *+^ ), p,q be Element of F;

       carr(F) c= carr(*+^) by Th23;

      then

      reconsider p9 = p, q9 = q as Element of (D *+^ );

      

      thus (p [*] q) = (p9 [*] q9) by Th25

      .= (p ^ q) by Def34;

    end;

    theorem :: MONOID_0:64

    for F be unital non empty SubStr of (D *+^ ) holds ( the_unity_wrt the multF of F) = {}

    proof

      let F be unital non empty SubStr of (D *+^ );

      set p = ( the_unity_wrt op(F));

      reconsider q = p as Element of F qua SubStr of (D *+^ );

      (q ^ {} ) = p by FINSEQ_1: 34

      .= (p [*] p) by SETWISEO: 15

      .= (q ^ q) by Th63;

      hence thesis by FINSEQ_1: 33;

    end;

    theorem :: MONOID_0:65

    for F be non empty SubStr of (D *+^ ) st {} is Element of F holds F is unital & ( the_unity_wrt the multF of F) = {}

    proof

      let F be non empty SubStr of (D *+^ );

      ( the_unity_wrt op(*+^)) = {} by Th60;

      hence thesis by Th30;

    end;

    theorem :: MONOID_0:66

    for A,B be non empty set st A c= B holds (A *+^ ) is SubStr of (B *+^ )

    proof

      let A,B be non empty set;

       carr(*+^) = (A * ) by Def34;

      then

       A1: ( dom op(*+^)) = [:(A * ), (A * ):] by FUNCT_2:def 1;

       carr(*+^) = (B * ) by Def34;

      then

       A2: ( dom op(*+^)) = [:(B * ), (B * ):] by FUNCT_2:def 1;

      assume A c= B;

      then

       A3: (A * ) c= (B * ) by FINSEQ_1: 62;

       A4:

      now

        let x be object;

        assume

         A5: x in [:(A * ), (A * ):];

        then

         A6: (x `1 ) in (A * ) & (x `2 ) in (A * ) by MCART_1: 10;

        then

        reconsider x1 = (x `1 ), x2 = (x `2 ) as Element of (A *+^ ) by Def34;

        reconsider y1 = (x `1 ), y2 = (x `2 ) as Element of (B *+^ ) by A3, A6, Def34;

        

        thus ( op(*+^) . x) = (x1 [*] x2) by A5, MCART_1: 21

        .= (x1 ^ x2) by Def34

        .= (y1 [*] y2) by Def34

        .= ( op(*+^) . x) by A5, MCART_1: 21;

      end;

       [:(A * ), (A * ):] c= [:(B * ), (B * ):] by A3, ZFMISC_1: 96;

      hence op(*+^) c= op(*+^) by A1, A2, A4, GRFUNC_1: 2;

    end;

    theorem :: MONOID_0:67

    (D -concatenation ) is having_a_unity & ( the_unity_wrt (D -concatenation )) = {} & (D -concatenation ) is associative

    proof

       multMagma (# (D * ), (D -concatenation ) #) = (D *+^ ) by Def34;

      hence thesis by Th60;

    end;

    begin

    definition

      let X be set;

      :: MONOID_0:def37

      func GPFuncs X -> constituted-Functions strict multMagma means

      : Def37: the carrier of it = ( PFuncs (X,X)) & for f,g be Element of it holds (f [*] g) = (g (*) f);

      existence

      proof

        reconsider g = ( id X) as PartFunc of X, X;

        set D = ( PFuncs (X,X));

        defpred P[ Element of D, Element of D, Element of D] means ex f,g be PartFunc of X, X st $1 = f & $2 = g & $3 = (g (*) f);

        

         A1: for a,b be Element of D holds ex c be Element of D st P[a, b, c]

        proof

          let a,b be Element of D;

          reconsider f = a, g = b as PartFunc of X, X by PARTFUN1: 46;

          reconsider c = (g * f) as Element of D by PARTFUN1: 45;

          take c, f, g;

          thus thesis;

        end;

        consider f be BinOp of D such that

         A2: for a,b be Element of D holds P[a, b, (f . (a,b))] from BINOP_1:sch 3( A1);

        set G = multMagma (# D, f #);

        G is constituted-Functions;

        then

        reconsider G as constituted-Functions strict multMagma;

        take G;

        thus carr(G) = ( PFuncs (X,X));

        let g,h be Element of G;

        reconsider g9 = g, h9 = h as Element of D;

        ex g,h be PartFunc of X, X st g9 = g & h9 = h & (f . (g9,h9)) = (h (*) g) by A2;

        hence thesis;

      end;

      uniqueness

      proof

        let G1,G2 be constituted-Functions strict multMagma such that

         A3: carr(G1) = ( PFuncs (X,X)) and

         A4: for f,g be Element of G1 holds (f [*] g) = (g (*) f) and

         A5: carr(G2) = ( PFuncs (X,X)) and

         A6: for f,g be Element of G2 holds (f [*] g) = (g (*) f);

        set f1 = op(G1), f2 = op(G2);

        now

          let a,b be Element of G1;

          reconsider a9 = a, b9 = b as Element of G2 by A3, A5;

          (a [*] b) = (b (*) a) & (a9 [*] b9) = (b9 (*) a9) by A4, A6;

          hence (f1 . (a,b)) = (f2 . (a,b));

        end;

        hence thesis by A3, A5, BINOP_1: 2;

      end;

    end

    registration

      let X be set;

      cluster ( GPFuncs X) -> unital associative non empty;

      coherence

      proof

        set G = ( GPFuncs X);

        reconsider g = ( id X) as PartFunc of X, X;

        set D = ( PFuncs (X,X));

        

         A1: the carrier of ( GPFuncs X) = D by Def37;

         A2:

        now

          let f9,g,h be Element of G;

          reconsider fg = (f9 [*] g), gh = (g [*] h) as Element of G;

          

          thus ((f9 [*] g) [*] h) = (h (*) fg) by Def37

          .= (h (*) (g (*) f9)) by Def37

          .= ((h (*) g) (*) f9) by RELAT_1: 36

          .= (gh (*) f9) by Def37

          .= (f9 [*] (g [*] h)) by Def37;

        end;

        reconsider f1 = g as Element of G by A1, PARTFUN1: 45;

        now

          let h be Element of G;

          reconsider j = h as PartFunc of X, X by A1, PARTFUN1: 46;

          

          thus (f1 [*] h) = (j (*) g) by Def37

          .= h by PARTFUN1: 6;

          

          thus (h [*] f1) = (g (*) j) by Def37

          .= h by PARTFUN1: 7;

        end;

        hence thesis by A1, A2;

      end;

    end

    definition

      let X be set;

      :: MONOID_0:def38

      func MPFuncs X -> well-unital strict non empty MonoidalExtension of ( GPFuncs X) means not contradiction;

      existence ;

      uniqueness by Th20;

      :: MONOID_0:def39

      func X -composition -> BinOp of ( PFuncs (X,X)) equals the multF of ( GPFuncs X);

      correctness

      proof

         carr(GPFuncs) = ( PFuncs (X,X)) by Def37;

        hence thesis;

      end;

    end

    theorem :: MONOID_0:68

    x is Element of ( GPFuncs X) iff x is PartFunc of X, X

    proof

       carr(GPFuncs) = ( PFuncs (X,X)) by Def37;

      hence thesis by PARTFUN1: 45, PARTFUN1: 46;

    end;

    theorem :: MONOID_0:69

    

     Th69: ( the_unity_wrt the multF of ( GPFuncs X)) = ( id X)

    proof

      reconsider g = ( id X) as PartFunc of X, X;

      set op = op(GPFuncs);

      

       A1: carr(GPFuncs) = ( PFuncs (X,X)) by Def37;

      then

      reconsider f = g as Element of ( GPFuncs X) by PARTFUN1: 45;

      now

        let h be Element of ( GPFuncs X);

        reconsider j = h as PartFunc of X, X by A1, PARTFUN1: 46;

        

        thus (op . (f,h)) = (f [*] h)

        .= (j (*) g) by Def37

        .= h by PARTFUN1: 6;

        

        thus (op . (h,f)) = (h [*] f)

        .= (g (*) j) by Def37

        .= h by PARTFUN1: 7;

      end;

      then f is_a_unity_wrt op by BINOP_1: 3;

      hence thesis by BINOP_1:def 8;

    end;

    theorem :: MONOID_0:70

    

     Th70: for F be non empty SubStr of ( GPFuncs X) holds for f,g be Element of F holds (f [*] g) = (g (*) f)

    proof

      let F be non empty SubStr of ( GPFuncs X);

      let f,g be Element of F;

       carr(F) c= carr(GPFuncs) by Th23;

      then

      reconsider f9 = f, g9 = g as Element of ( GPFuncs X);

      (f [*] g) = (f9 [*] g9) by Th25;

      hence thesis by Def37;

    end;

    theorem :: MONOID_0:71

    

     Th71: for F be non empty SubStr of ( GPFuncs X) st ( id X) is Element of F holds F is unital & ( the_unity_wrt the multF of F) = ( id X)

    proof

      let F be non empty SubStr of ( GPFuncs X);

      ( the_unity_wrt op(GPFuncs)) = ( id X) by Th69;

      hence thesis by Th30;

    end;

    theorem :: MONOID_0:72

    Y c= X implies ( GPFuncs Y) is SubStr of ( GPFuncs X)

    proof

       carr(GPFuncs) = ( PFuncs (Y,Y)) by Def37;

      then

       A1: ( dom op(GPFuncs)) = [:( PFuncs (Y,Y)), ( PFuncs (Y,Y)):] by FUNCT_2:def 1;

       carr(GPFuncs) = ( PFuncs (X,X)) by Def37;

      then

       A2: ( dom op(GPFuncs)) = [:( PFuncs (X,X)), ( PFuncs (X,X)):] by FUNCT_2:def 1;

      assume Y c= X;

      then

       A3: ( PFuncs (Y,Y)) c= ( PFuncs (X,X)) by PARTFUN1: 50;

       A4:

      now

        let x be object;

        assume

         A5: x in [:( PFuncs (Y,Y)), ( PFuncs (Y,Y)):];

        then

         A6: (x `1 ) in ( PFuncs (Y,Y)) & (x `2 ) in ( PFuncs (Y,Y)) by MCART_1: 10;

        then

        reconsider x1 = (x `1 ), x2 = (x `2 ) as Element of ( GPFuncs Y) by Def37;

        reconsider y1 = (x `1 ), y2 = (x `2 ) as Element of ( GPFuncs X) by A3, A6, Def37;

        

        thus ( op(GPFuncs) . x) = (x1 [*] x2) by A5, MCART_1: 21

        .= (x2 (*) x1) by Def37

        .= (y1 [*] y2) by Def37

        .= ( op(GPFuncs) . x) by A5, MCART_1: 21;

      end;

       [:( PFuncs (Y,Y)), ( PFuncs (Y,Y)):] c= [:( PFuncs (X,X)), ( PFuncs (X,X)):] by A3, ZFMISC_1: 96;

      hence op(GPFuncs) c= op(GPFuncs) by A1, A2, A4, GRFUNC_1: 2;

    end;

    definition

      let X be set;

      :: MONOID_0:def40

      func GFuncs X -> strict SubStr of ( GPFuncs X) means

      : Def40: the carrier of it = ( Funcs (X,X));

      existence

      proof

        ( Funcs (X,X)) c= ( PFuncs (X,X)) by FUNCT_2: 72;

        then

        reconsider F = ( Funcs (X,X)) as non empty Subset of ( GPFuncs X) by Def37;

        

         A1: for x,y be Element of F holds (x [*] y) in F

        proof

          let x,y be Element of F;

          reconsider f = x, g = y as Function of X, X by FUNCT_2: 66;

          (x [*] y) = (g * f) by Def37;

          hence thesis by FUNCT_2: 9;

        end;

        consider G be strict non empty SubStr of ( GPFuncs X) such that

         A2: the carrier of G = F by Lm5, A1;

        take G;

        thus thesis by A2;

      end;

      uniqueness by Th26;

    end

    registration

      let X be set;

      cluster ( GFuncs X) -> unital non empty;

      coherence

      proof

        

         A1: the carrier of ( GFuncs X) = ( Funcs (X,X)) by Def40;

        ( id X) in ( Funcs (X,X)) by FUNCT_2: 9;

        hence thesis by A1, Th71;

      end;

    end

    definition

      let X be set;

      :: MONOID_0:def41

      func MFuncs X -> well-unital strict MonoidalExtension of ( GFuncs X) means not contradiction;

      correctness by Th20;

    end

    theorem :: MONOID_0:73

    x is Element of ( GFuncs X) iff x is Function of X, X

    proof

       carr(GFuncs) = ( Funcs (X,X)) by Def40;

      hence thesis by FUNCT_2: 9, FUNCT_2: 66;

    end;

    theorem :: MONOID_0:74

    

     Th74: the multF of ( GFuncs X) = ((X -composition ) || ( Funcs (X,X)))

    proof

      

       A1: carr(GFuncs) = ( Funcs (X,X)) by Def40;

       op(GFuncs) c= op(GPFuncs) & ( dom op(GFuncs)) = [: carr(GFuncs), carr(GFuncs):] by Def23, FUNCT_2:def 1;

      hence thesis by A1, GRFUNC_1: 23;

    end;

    theorem :: MONOID_0:75

    

     Th75: ( the_unity_wrt the multF of ( GFuncs X)) = ( id X)

    proof

      ( id X) in ( Funcs (X,X)) & carr(GFuncs) = ( Funcs (X,X)) by Def40, FUNCT_2: 9;

      hence thesis by Th71;

    end;

    theorem :: MONOID_0:76

    the carrier of ( MFuncs X) = ( Funcs (X,X)) & the multF of ( MFuncs X) = ((X -composition ) || ( Funcs (X,X))) & ( 1. ( MFuncs X)) = ( id X)

    proof

      ( the_unity_wrt op(GFuncs)) = ( id X) & the multMagma of ( MFuncs X) = ( GFuncs X) by Def22, Th75;

      hence thesis by Def40, Th17, Th74;

    end;

    definition

      let X be set;

      :: MONOID_0:def42

      func GPerms X -> strict non empty SubStr of ( GFuncs X) means

      : Def42: for f be Element of ( GFuncs X) holds f in the carrier of it iff f is Permutation of X;

      existence

      proof

        defpred P[ Element of ( GFuncs X)] means $1 is Permutation of X;

        

         A1: ex x be Element of ( GFuncs X) st P[x]

        proof

          set f = the Permutation of X;

           carr(GFuncs) = ( Funcs (X,X)) by Def40;

          then

          reconsider x = f as Element of ( GFuncs X) by FUNCT_2: 9;

          take x;

          thus thesis;

        end;

         carr(GFuncs) = ( Funcs (X,X)) by Def40;

        then

        reconsider f = ( id X) as Element of ( GFuncs X) by FUNCT_2: 9;

        

         A2: for x,y be Element of ( GFuncs X) st P[x] & P[y] holds P[(x [*] y)]

        proof

          let x,y be Element of ( GFuncs X);

          assume x is Permutation of X & y is Permutation of X;

          then

          reconsider f = x, g = y as Permutation of X;

          (x [*] y) = (g * f) by Th70;

          hence thesis;

        end;

        consider G be strict non empty SubStr of ( GFuncs X) such that

         A3: for f be Element of ( GFuncs X) holds f in the carrier of G iff P[f] from SubStrEx2( A2, A1);

        take G;

        thus thesis by A3;

      end;

      uniqueness

      proof

        let G1,G2 be strict non empty SubStr of ( GFuncs X) such that

         A4: for f be Element of ( GFuncs X) holds f in carr(G1) iff f is Permutation of X and

         A5: for f be Element of ( GFuncs X) holds f in carr(G2) iff f is Permutation of X;

        

         A6: carr(G2) c= carr(GFuncs) by Th23;

        

         A7: carr(G1) c= carr(GFuncs) by Th23;

         carr(G1) = carr(G2)

        proof

          thus carr(G1) c= carr(G2)

          proof

            let x be object;

            assume

             A8: x in carr(G1);

            then

            reconsider f = x as Element of ( GFuncs X) by A7;

            f is Permutation of X by A4, A8;

            hence thesis by A5;

          end;

          let x be object;

          assume

           A9: x in carr(G2);

          then

          reconsider f = x as Element of ( GFuncs X) by A6;

          f is Permutation of X by A5, A9;

          hence thesis by A4;

        end;

        hence thesis by Th26;

      end;

    end

    registration

      let X be set;

      cluster ( GPerms X) -> unital invertible;

      coherence

      proof

        set G = ( GPerms X);

        

         A1: carr(GFuncs) = ( Funcs (X,X)) by Def40;

        then

        reconsider f = ( id X) as Element of ( GFuncs X) by FUNCT_2: 9;

        f in carr(G) by Def42;

        hence G is unital by Th71;

        now

          reconsider i = f as Element of G by Def42;

          let a,b be Element of G;

           carr(G) c= carr(GFuncs) by Th23;

          then

          reconsider a9 = a, b9 = b as Element of ( GFuncs X);

          reconsider f = a9, g = b9 as Permutation of X by Def42;

          

           A2: i = (f (*) (f " )) & i = ((f " ) (*) f) by FUNCT_2: 61;

          reconsider f9 = (f " ) as Element of ( GFuncs X) by A1, FUNCT_2: 9;

          

           A3: (g (*) i) = g & (i (*) g) = g by FUNCT_2: 17;

          reconsider f9 as Element of G by Def42;

          reconsider r = (f9 [*] b), l = (b [*] f9) as Element of G;

          take r, l;

          

           A4: (i [*] b) = (g (*) ( id X)) & (b [*] i) = (( id X) (*) g) by Th70;

          (a [*] f9) = ((f " ) (*) f) & (f9 [*] a) = (f (*) (f " )) by Th70;

          hence (a [*] r) = b & (l [*] a) = b by A2, A3, A4, Lm1;

        end;

        hence thesis by Th10;

      end;

    end

    theorem :: MONOID_0:77

    

     Th77: x is Element of ( GPerms X) iff x is Permutation of X

    proof

      

       A1: x is Permutation of X implies x in ( Funcs (X,X)) by FUNCT_2: 9;

       carr(GPerms) c= carr(GFuncs) by Th23;

      then

       A2: x is Element of ( GPerms X) implies x is Element of ( GFuncs X);

       carr(GFuncs) = ( Funcs (X,X)) by Def40;

      hence thesis by A1, A2, Def42;

    end;

    theorem :: MONOID_0:78

    

     Th78: ( the_unity_wrt the multF of ( GPerms X)) = ( id X) & ( 1_ ( GPerms X)) = ( id X)

    proof

      reconsider i = ( id X) as Element of ( GPerms X) by Th77;

      now

        let a be Element of ( GPerms X);

        reconsider f = a as Permutation of X by Th77;

        (a [*] i) = (i (*) a) by Th70;

        then

         A1: ( op(GPerms) . (a,i)) = (i (*) f);

        (i [*] a) = (a (*) i) by Th70;

        hence ( op(GPerms) . (i,a)) = a & ( op(GPerms) . (a,i)) = a by A1, FUNCT_2: 17;

      end;

      then i is_a_unity_wrt op(GPerms) by BINOP_1: 3;

      hence ( the_unity_wrt op(GPerms)) = ( id X) by BINOP_1:def 8;

      hence thesis by GROUP_1: 22;

    end;

    theorem :: MONOID_0:79

    for f be Element of ( GPerms X) holds (f " ) = (f qua Function " )

    proof

      let f be Element of ( GPerms X);

      reconsider g = f as Permutation of X by Th77;

      

       A1: (g (*) (g " )) = ( id X) & ((g " ) (*) g) = ( id X) by FUNCT_2: 61;

      reconsider b = (g " ) as Element of ( GPerms X) by Th77;

      reconsider b as Element of ( GPerms X);

      

       A2: (b [*] f) = (g (*) (g " )) by Th70;

      ( id X) = ( 1_ ( GPerms X)) & (f [*] b) = ((g " ) (*) g) by Th70, Th78;

      hence thesis by A1, A2, GROUP_1:def 5;

    end;

    theorem :: MONOID_0:80

    for S be 1-sorted st the carrier of S is functional holds S is constituted-Functions;

    theorem :: MONOID_0:81

    for G be non empty multMagma, D be non empty Subset of G st for x,y be Element of D holds (x * y) in D holds ex H be strict non empty SubStr of G st the carrier of H = D by Lm5;

    theorem :: MONOID_0:82

    for G be non empty multLoopStr, D be non empty Subset of G st (for x,y be Element of D holds (x * y) in D) & ( 1. G) in D holds ex H be strict non empty MonoidalSubStr of G st the carrier of H = D

    proof

      let G be non empty multLoopStr, D be non empty Subset of G;

      assume that

       A1: for x,y be Element of D holds (x * y) in D and

       A2: ( 1. G) in D;

      thus ex H be strict non empty MonoidalSubStr of G st the carrier of H = D

      proof

        consider H be strict non empty SubStr of G such that

         A3: the carrier of H = D by Lm5, A1;

        reconsider e = ( 1. G) as Element of H by A2, A3;

        set N = multLoopStr (# the carrier of H, the multF of H, e #);

         op(N) c= op(G) & for M be multLoopStr st G = M holds ( 1. N) = ( 1. M) by Def23;

        then

        reconsider N as strict non empty MonoidalSubStr of G by Def25;

        take N;

        thus thesis by A3;

      end;

    end;