monoid_1.miz

    begin

    reserve x,y,z,X,Y,Z for set,

n for Element of NAT ;

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

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

    definition

      let f be Function, x1,x2,y be set;

      :: MONOID_1:def1

      func f .. (x1,x2,y) -> set equals (f .. ( [x1, x2],y));

      correctness ;

    end

    definition

      let A,D1,D2,D be non empty set;

      let f be Function of [:D1, D2:], ( Funcs (A,D));

      let x1 be Element of D1;

      let x2 be Element of D2;

      let x be Element of A;

      :: original: ..

      redefine

      func f .. (x1,x2,x) -> Element of D ;

      coherence

      proof

        reconsider g = (f . (x1,x2)) as Element of ( Funcs (A,D));



         A1: [x1, x2] in [:D1, D2:];

        ( dom f) = [:D1, D2:] & ( dom g) = A by FUNCT_2:def 1;

        then (f .. (x1,x2,x)) = (g . x) by A1, FUNCT_5: 38;

        hence thesis;

      end;

    end

    definition

      let A be set;

      let D1,D2,D be non empty set, f be Function of [:D1, D2:], D;

      let g1 be Function of A, D1;

      let g2 be Function of A, D2;

      :: original: .:

      redefine

      func f .: (g1,g2) -> Element of ( Funcs (A,D)) ;

      coherence

      proof

        (f .: (g1,g2)) = (f * <:g1, g2:>) by FUNCOP_1:def 3;

        then ( dom (f .: (g1,g2))) = A & ( rng (f .: (g1,g2))) c= D by FUNCT_2:def 1, RELAT_1:def 19;

        hence thesis by FUNCT_2:def 2;

      end;

    end

    notation

      let A be non empty set;

      let n be Element of NAT , x be Element of A;

      synonym n .--> x for n |-> x;

    end

    definition

      let A be non empty set;

      let n be Element of NAT , x be Element of A;

      :: original: .-->

      redefine

      func n .--> x -> FinSequence of A ;

      coherence by FINSEQ_2: 63;

    end

    definition

      let D be non empty set, A be set, d be Element of D;

      :: original: -->

      redefine

      func A --> d -> Element of ( Funcs (A,D)) ;

      coherence

      proof

        ( dom (A --> d)) = A & ( rng (A --> d)) c= {d} by FUNCOP_1: 13;

        hence thesis by FUNCT_2:def 2;

      end;

    end

    definition

      let A be set;

      let D1,D2,D be non empty set, f be Function of [:D1, D2:], D;

      let d be Element of D1;

      let g be Function of A, D2;

      :: original: [;]

      redefine

      func f [;] (d,g) -> Element of ( Funcs (A,D)) ;

      coherence

      proof

        ( dom g) = A by FUNCT_2:def 1;

        then (f [;] (d,g)) = (f * <:(A --> d), g:>) by FUNCOP_1:def 5;

        then ( dom (f [;] (d,g))) = A & ( rng (f [;] (d,g))) c= D by FUNCT_2:def 1, RELAT_1:def 19;

        hence thesis by FUNCT_2:def 2;

      end;

    end

    definition

      let A be set;

      let D1,D2,D be non empty set, f be Function of [:D1, D2:], D;

      let g be Function of A, D1;

      let d be Element of D2;

      :: original: [:]

      redefine

      func f [:] (g,d) -> Element of ( Funcs (A,D)) ;

      coherence

      proof

        ( dom g) = A by FUNCT_2:def 1;

        then (f [:] (g,d)) = (f * <:g, (A --> d):>) by FUNCOP_1:def 4;

        then ( dom (f [:] (g,d))) = A & ( rng (f [:] (g,d))) c= D by FUNCT_2:def 1, RELAT_1:def 19;

        hence thesis by FUNCT_2:def 2;

      end;

    end

    theorem :: MONOID_1:1

    for f,g be Function, X be set holds ((f | X) * g) = (f * (X |` g))

    proof

      let f,g be Function, X be set;



       A1: ( dom (f | X)) = (( dom f) /\ X) by RELAT_1: 61;



       A2: ( dom ((f | X) * g)) = ( dom (f * (X |` g)))

      proof

        thus ( dom ((f | X) * g)) c= ( dom (f * (X |` g)))

        proof

          let x be object;

          assume

           A3: x in ( dom ((f | X) * g));

          then

           A4: x in ( dom g) by FUNCT_1: 11;



           A5: (g . x) in ( dom (f | X)) by A3, FUNCT_1: 11;

          then

           A6: (g . x) in ( dom f) by A1, XBOOLE_0:def 4;

          (g . x) in X by A1, A5, XBOOLE_0:def 4;

          then

           A7: x in ( dom (X |` g)) by A4, FUNCT_1: 53;

          then (g . x) = ((X |` g) . x) by FUNCT_1: 53;

          hence thesis by A6, A7, FUNCT_1: 11;

        end;

        let x be object;

        assume

         A8: x in ( dom (f * (X |` g)));

        then

         A9: x in ( dom (X |` g)) by FUNCT_1: 11;

        then

         A10: x in ( dom g) by FUNCT_1: 53;

        ((X |` g) . x) in ( dom f) by A8, FUNCT_1: 11;

        then

         A11: (g . x) in ( dom f) by A9, FUNCT_1: 53;

        (g . x) in X by A9, FUNCT_1: 53;

        then (g . x) in ( dom (f | X)) by A1, A11, XBOOLE_0:def 4;

        hence thesis by A10, FUNCT_1: 11;

      end;

      now

        let x be object;

        assume

         A12: x in ( dom ((f | X) * g));

        then (((f | X) * g) . x) = ((f | X) . (g . x)) & (g . x) in ( dom (f | X)) by FUNCT_1: 11, FUNCT_1: 12;

        then

         A13: (((f | X) * g) . x) = (f . (g . x)) by FUNCT_1: 47;

        ((f * (X |` g)) . x) = (f . ((X |` g) . x)) & x in ( dom (X |` g)) by A2, A12, FUNCT_1: 11, FUNCT_1: 12;

        hence (((f | X) * g) . x) = ((f * (X |` g)) . x) by A13, FUNCT_1: 53;

      end;

      hence thesis by A2, FUNCT_1: 2;

    end;

    scheme :: MONOID_1:sch1

    NonUniqFuncDEx { X() -> set , Y() -> non empty set , P[ object, object] } :

ex f be Function of X(), Y() st for x be object st x in X() holds P[x, (f . x)]

      provided

       A1: for x be object st x in X() holds ex y be Element of Y() st P[x, y];



       A2: for x be object st x in X() holds ex y be object st y in Y() & P[x, y]

      proof

        let x be object;

        assume x in X();

        then

        consider y be Element of Y() such that

         A3: P[x, y] by A1;

        take y;

        thus thesis by A3;

      end;

      consider f be Function such that

       A4: ( dom f) = X() & ( rng f) c= Y() & for x be object st x in X() holds P[x, (f . x)] from FUNCT_1:sch 6( A2);

      reconsider f as Function of X(), Y() by A4, FUNCT_2:def 1, RELSET_1: 4;

      take f;

      thus thesis by A4;

    end;

    begin

    definition

      let D1,D2,D be non empty set;

      let f be Function of [:D1, D2:], D;

      let A be set;

      :: MONOID_1:def2

      func (f,D) .: A -> Function of [:( Funcs (A,D1)), ( Funcs (A,D2)):], ( Funcs (A,D)) means

      : Def2: for f1 be Element of ( Funcs (A,D1)) holds for f2 be Element of ( Funcs (A,D2)) holds (it . (f1,f2)) = (f .: (f1,f2));

      existence

      proof

        deffunc G( Element of ( Funcs (A,D1)), Element of ( Funcs (A,D2))) = (f .: ($1,$2));

        consider b be Function of [:( Funcs (A,D1)), ( Funcs (A,D2)):], ( Funcs (A,D)) such that

         A1: for f1 be Element of ( Funcs (A,D1)) holds for f2 be Element of ( Funcs (A,D2)) holds (b . (f1,f2)) = G(f1,f2) from BINOP_1:sch 4;

        take b;

        let f1 be Element of ( Funcs (A,D1)), f2 be Element of ( Funcs (A,D2));

        thus thesis by A1;

      end;

      uniqueness

      proof

        let o1,o2 be Function of [:( Funcs (A,D1)), ( Funcs (A,D2)):], ( Funcs (A,D)) such that

         A2: for f1 be Element of ( Funcs (A,D1)) holds for f2 be Element of ( Funcs (A,D2)) holds (o1 . (f1,f2)) = (f .: (f1,f2)) and

         A3: for f1 be Element of ( Funcs (A,D1)) holds for f2 be Element of ( Funcs (A,D2)) holds (o2 . (f1,f2)) = (f .: (f1,f2));

        now

          let f1 be Element of ( Funcs (A,D1)), f2 be Element of ( Funcs (A,D2));



          thus (o1 . (f1,f2)) = (f .: (f1,f2)) by A2

          .= (o2 . (f1,f2)) by A3;

        end;

        hence thesis;

      end;

    end

    theorem :: MONOID_1:2

    for D1,D2,D be non empty set holds for f be Function of [:D1, D2:], D holds for A be set, f1 be Function of A, D1, f2 be Function of A, D2 holds for x st x in A holds (((f,D) .: A) .. (f1,f2,x)) = (f . ((f1 . x),(f2 . x)))

    proof

      let D1,D2,D be non empty set;

      let f be Function of [:D1, D2:], D;

      let A be set, f1 be Function of A, D1, f2 be Function of A, D2;

      ( dom f2) = A & ( rng f2) c= D2 by FUNCT_2:def 1;

      then

      reconsider f2 as Element of ( Funcs (A,D2)) by FUNCT_2:def 2;

      ( dom f1) = A & ( rng f1) c= D1 by FUNCT_2:def 1;

      then

      reconsider f1 as Element of ( Funcs (A,D1)) by FUNCT_2:def 2;



       A1: ( dom (f .: (f1,f2))) = A by FUNCT_2:def 1;



       A2: (((f,D) .: A) . (f1,f2)) = (f .: (f1,f2)) & [f1, f2] = [f1, f2] by Def2;

      let x such that

       A3: x in A;

      ( dom ((f,D) .: A)) = [:( Funcs (A,D1)), ( Funcs (A,D2)):] & ((f .: (f1,f2)) . x) = (f . ((f1 . x),(f2 . x))) by A3, A1, FUNCOP_1: 22, FUNCT_2:def 1;

      hence thesis by A3, A1, A2, FUNCT_5: 38;

    end;

    reserve A for set,

D for non empty set,

a,b,c,l,r for Element of D,

o,o9 for BinOp of D,

f,g,h for Function of A, D;

    theorem :: MONOID_1:3



     Th3: o is commutative implies (o .: (f,g)) = (o .: (g,f))

    proof



       A1: ( dom (o .: (f,g))) = A by FUNCT_2:def 1;



       A2: ( dom f) = A & ( dom g) = A by FUNCT_2:def 1;



       A3: ( dom (o .: (g,f))) = A by FUNCT_2:def 1;

      assume

       A4: (o . (a,b)) = (o . (b,a));

      now

        let x be object;

        assume

         A5: x in A;

        then (f . x) in ( rng f) & (g . x) in ( rng g) by A2, FUNCT_1:def 3;

        then

        reconsider a = (f . x), b = (g . x) as Element of D;



        thus ((o .: (f,g)) . x) = (o . (a,b)) by A1, A5, FUNCOP_1: 22

        .= (o . (b,a)) by A4

        .= ((o .: (g,f)) . x) by A3, A5, FUNCOP_1: 22;

      end;

      hence thesis by A1, A3, FUNCT_1: 2;

    end;

    theorem :: MONOID_1:4



     Th4: o is associative implies (o .: ((o .: (f,g)),h)) = (o .: (f,(o .: (g,h))))

    proof



       A1: ( dom (o .: (f,g))) = A by FUNCT_2:def 1;



       A2: ( dom (o .: (g,h))) = A by FUNCT_2:def 1;



       A3: ( dom f) = A & ( dom g) = A by FUNCT_2:def 1;



       A4: ( dom (o .: ((o .: (f,g)),h))) = A by FUNCT_2:def 1;



       A5: ( dom h) = A by FUNCT_2:def 1;



       A6: ( dom (o .: (f,(o .: (g,h))))) = A by FUNCT_2:def 1;

      assume

       A7: (o . ((o . (a,b)),c)) = (o . (a,(o . (b,c))));

      now

        let x be object;

        assume

         A8: x in A;

        then

         A9: (h . x) in ( rng h) by A5, FUNCT_1:def 3;

        (f . x) in ( rng f) & (g . x) in ( rng g) by A3, A8, FUNCT_1:def 3;

        then

        reconsider a = (f . x), b = (g . x), c = (h . x) as Element of D by A9;



        thus ((o .: ((o .: (f,g)),h)) . x) = (o . (((o .: (f,g)) . x),c)) by A4, A8, FUNCOP_1: 22

        .= (o . ((o . (a,b)),c)) by A1, A8, FUNCOP_1: 22

        .= (o . (a,(o . (b,c)))) by A7

        .= (o . (a,((o .: (g,h)) . x))) by A2, A8, FUNCOP_1: 22

        .= ((o .: (f,(o .: (g,h)))) . x) by A6, A8, FUNCOP_1: 22;

      end;

      hence thesis by A4, A6, FUNCT_1: 2;

    end;

    theorem :: MONOID_1:5



     Th5: a is_a_unity_wrt o implies (o [;] (a,f)) = f & (o [:] (f,a)) = f

    proof

      assume

       A1: a is_a_unity_wrt o;



       A2: ( dom f) = A by FUNCT_2:def 1;



       A3: ( dom (o [;] (a,f))) = A by FUNCT_2:def 1;

      now

        let x be object;

        assume

         A4: x in A;

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

        then

        reconsider b = (f . x) as Element of D;



        thus ((o [;] (a,f)) . x) = (o . (a,b)) by A3, A4, FUNCOP_1: 32

        .= (f . x) by A1, BINOP_1: 3;

      end;

      hence (o [;] (a,f)) = f by A3, A2, FUNCT_1: 2;



       A5: ( dom (o [:] (f,a))) = A by FUNCT_2:def 1;

      now

        let x be object;

        assume

         A6: x in A;

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

        then

        reconsider b = (f . x) as Element of D;



        thus ((o [:] (f,a)) . x) = (o . (b,a)) by A5, A6, FUNCOP_1: 27

        .= (f . x) by A1, BINOP_1: 3;

      end;

      hence thesis by A5, A2, FUNCT_1: 2;

    end;

    theorem :: MONOID_1:6



     Th6: o is idempotent implies (o .: (f,f)) = f

    proof



       A1: ( dom (o .: (f,f))) = A by FUNCT_2:def 1;

      assume

       A2: (o . (a,a)) = a;

       A3:

      now

        let x be object;

        assume

         A4: x in A;

        then

        reconsider a = (f . x) as Element of D by FUNCT_2: 5;



        thus ((o .: (f,f)) . x) = (o . (a,a)) by A1, A4, FUNCOP_1: 22

        .= (f . x) by A2;

      end;

      ( dom f) = A by FUNCT_2:def 1;

      hence thesis by A1, A3, FUNCT_1: 2;

    end;

    theorem :: MONOID_1:7



     Th7: o is commutative implies ((o,D) .: A) is commutative

    proof

      assume

       A1: o is commutative;

      set h = ((o,D) .: A);

      let f,g be Element of ( Funcs (A,D));



      thus (h . (f,g)) = (o .: (f,g)) by Def2

      .= (o .: (g,f)) by A1, Th3

      .= (h . (g,f)) by Def2;

    end;

    theorem :: MONOID_1:8



     Th8: o is associative implies ((o,D) .: A) is associative

    proof

      assume

       A1: o is associative;

      set F = ((o,D) .: A);

      let f,g,h be Element of ( Funcs (A,D));



      thus (F . ((F . (f,g)),h)) = (F . ((o .: (f,g)),h)) by Def2

      .= (o .: ((o .: (f,g)),h)) by Def2

      .= (o .: (f,(o .: (g,h)))) by A1, Th4

      .= (F . (f,(o .: (g,h)))) by Def2

      .= (F . (f,(F . (g,h)))) by Def2;

    end;

    theorem :: MONOID_1:9



     Th9: a is_a_unity_wrt o implies (A --> a) is_a_unity_wrt ((o,D) .: A)

    proof

      set e = (A --> a);

      set F = ((o,D) .: A);

      assume

       A1: a is_a_unity_wrt o;

      now

        let f be Element of ( Funcs (A,D));



         A2: ( dom f) = A by FUNCT_2:def 1;



        thus (F . (e,f)) = (o .: (e,f)) by Def2

        .= (o [;] (a,f)) by A2, FUNCOP_1: 31

        .= f by A1, Th5;



        thus (F . (f,e)) = (o .: (f,e)) by Def2

        .= (o [:] (f,a)) by A2, FUNCOP_1: 26

        .= f by A1, Th5;

      end;

      hence thesis by BINOP_1: 3;

    end;

    theorem :: MONOID_1:10



     Th10: o is having_a_unity implies ( the_unity_wrt ((o,D) .: A)) = (A --> ( the_unity_wrt o)) & ((o,D) .: A) is having_a_unity

    proof

      given a such that

       A1: a is_a_unity_wrt o;

      a = ( the_unity_wrt o) & (A --> a) is_a_unity_wrt ((o,D) .: A) by A1, Th9, BINOP_1:def 8;

      hence ( the_unity_wrt ((o,D) .: A)) = (A --> ( the_unity_wrt o)) by BINOP_1:def 8;

      take (A --> a);

      thus thesis by A1, Th9;

    end;

    theorem :: MONOID_1:11



     Th11: o is idempotent implies ((o,D) .: A) is idempotent

    proof

      assume

       A1: o is idempotent;

      let f be Element of ( Funcs (A,D));



      thus (((o,D) .: A) . (f,f)) = (o .: (f,f)) by Def2

      .= f by A1, Th6;

    end;

    theorem :: MONOID_1:12



     Th12: o is invertible implies ((o,D) .: A) is invertible

    proof

      assume

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

      let f,g be Element of ( Funcs (A,D));

      defpred P[ object, object] means (o . ((f . $1),$2)) = (g . $1);



       A2: for x be object st x in A holds ex c st P[x, c]

      proof

        let x be object;

        assume x in A;

        then

        reconsider a = (f . x), b = (g . x) as Element of D by FUNCT_2: 5;

        consider r, l such that

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

        take r;

        thus thesis by A3;

      end;

      consider h1 be Function of A, D such that

       A4: for x be object st x in A holds P[x, (h1 . x)] from NonUniqFuncDEx( A2);

      defpred Q[ object, object] means (o . ($2,(f . $1))) = (g . $1);



       A5: for x be object st x in A holds ex c st Q[x, c]

      proof

        let x be object;

        assume x in A;

        then

        reconsider a = (f . x), b = (g . x) as Element of D by FUNCT_2: 5;

        consider r, l such that (o . (a,r)) = b and

         A6: (o . (l,a)) = b by A1;

        take l;

        thus thesis by A6;

      end;

      consider h2 be Function of A, D such that

       A7: for x be object st x in A holds Q[x, (h2 . x)] from NonUniqFuncDEx( A5);



       A8: ( dom h1) = A & ( dom h2) = A by FUNCT_2:def 1;

      ( rng h1) c= D & ( rng h2) c= D;

      then

      reconsider h1, h2 as Element of ( Funcs (A,D)) by A8, FUNCT_2:def 2;

      take h1, h2;



       A9: ( dom g) = A by FUNCT_2:def 1;



       A10: ( dom (o .: (f,h1))) = A by FUNCT_2:def 1;

       A11:

      now

        let x be object;

        assume

         A12: x in A;



        hence ((o .: (f,h1)) . x) = (o . ((f . x),(h1 . x))) by A10, FUNCOP_1: 22

        .= (g . x) by A4, A12;

      end;

      (o .: (f,h1)) = (((o,D) .: A) . (f,h1)) by Def2;

      hence (((o,D) .: A) . (f,h1)) = g by A10, A9, A11, FUNCT_1: 2;



       A13: ( dom (o .: (h2,f))) = A by FUNCT_2:def 1;

       A14:

      now

        let x be object;

        assume

         A15: x in A;



        hence ((o .: (h2,f)) . x) = (o . ((h2 . x),(f . x))) by A13, FUNCOP_1: 22

        .= (g . x) by A7, A15;

      end;

      (o .: (h2,f)) = (((o,D) .: A) . (h2,f)) by Def2;

      hence thesis by A13, A9, A14, FUNCT_1: 2;

    end;

    theorem :: MONOID_1:13



     Th13: o is cancelable implies ((o,D) .: A) is cancelable

    proof

      assume

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

      let f,g,h be Element of ( Funcs (A,D)) such that

       A2: (((o,D) .: A) . (f,g)) = (((o,D) .: A) . (f,h)) or (((o,D) .: A) . (g,f)) = (((o,D) .: A) . (h,f));



       A3: A = ( dom (o .: (g,f))) & A = ( dom (o .: (h,f))) by FUNCT_2:def 1;



       A4: (((o,D) .: A) . (f,h)) = (o .: (f,h)) & (((o,D) .: A) . (h,f)) = (o .: (h,f)) by Def2;



       A5: A = ( dom (o .: (f,g))) & A = ( dom (o .: (f,h))) by FUNCT_2:def 1;



       A6: (((o,D) .: A) . (f,g)) = (o .: (f,g)) & (((o,D) .: A) . (g,f)) = (o .: (g,f)) by Def2;

       A7:

      now

        let x be object;

        assume

         A8: x in A;

        then

        reconsider a = (f . x), b = (g . x), c = (h . x) as Element of D by FUNCT_2: 5;



         A9: ((o .: (g,f)) . x) = (o . (b,a)) & ((o .: (h,f)) . x) = (o . (c,a)) by A3, A8, FUNCOP_1: 22;

        ((o .: (f,g)) . x) = (o . (a,b)) & ((o .: (f,h)) . x) = (o . (a,c)) by A5, A8, FUNCOP_1: 22;

        hence (g . x) = (h . x) by A1, A2, A6, A4, A9;

      end;

      ( dom g) = A & ( dom h) = A by FUNCT_2:def 1;

      hence thesis by A7, FUNCT_1: 2;

    end;

    theorem :: MONOID_1:14



     Th14: o is uniquely-decomposable implies ((o,D) .: A) is uniquely-decomposable

    proof

      assume that

       A1: o is having_a_unity and

       A2: for a, b st (o . (a,b)) = ( the_unity_wrt o) holds a = b & b = ( the_unity_wrt o);



       A3: ( the_unity_wrt ((o,D) .: A)) = (A --> ( the_unity_wrt o)) by A1, Th10;

      thus ((o,D) .: A) is having_a_unity by A1, Th10;

      let f,g be Element of ( Funcs (A,D)) such that

       A4: (((o,D) .: A) . (f,g)) = ( the_unity_wrt ((o,D) .: A));



       A5: ( dom (o .: (f,g))) = A by FUNCT_2:def 1;



       A6: (((o,D) .: A) . (f,g)) = (o .: (f,g)) by Def2;

       A7:

      now

        let x be object;

        assume

         A8: x in A;

        then

        reconsider a = (f . x), b = (g . x) as Element of D by FUNCT_2: 5;

        ((o .: (f,g)) . x) = (o . (a,b)) & ((A --> ( the_unity_wrt o)) . x) = ( the_unity_wrt o) by A5, A8, FUNCOP_1: 7, FUNCOP_1: 22;

        hence (f . x) = (g . x) by A2, A4, A6, A3;

      end;

       A9:

      now

        let x be object;

        assume

         A10: x in A;

        then

        reconsider a = (f . x), b = (g . x) as Element of D by FUNCT_2: 5;

        ((o .: (f,g)) . x) = (o . (a,b)) & ((A --> ( the_unity_wrt o)) . x) = ( the_unity_wrt o) by A5, A10, FUNCOP_1: 7, FUNCOP_1: 22;

        hence (g . x) = ((A --> ( the_unity_wrt o)) . x) by A2, A4, A6, A3;

      end;



       A11: ( dom g) = A by FUNCT_2:def 1;

      ( dom f) = A by FUNCT_2:def 1;

      hence f = g by A11, A7, FUNCT_1: 2;

      ( dom (A --> ( the_unity_wrt o))) = A;

      hence thesis by A3, A11, A9, FUNCT_1: 2;

    end;

    theorem :: MONOID_1:15

    o absorbs o9 implies ((o,D) .: A) absorbs ((o9,D) .: A)

    proof

      assume

       A1: (o . (a,(o9 . (a,b)))) = a;

      let f,g be Element of ( Funcs (A,D));



       A2: ( dom (o .: (f,(o9 .: (f,g))))) = A by FUNCT_2:def 1;



       A3: ( dom (o9 .: (f,g))) = A by FUNCT_2:def 1;

       A4:

      now

        let x be object;

        assume

         A5: x in A;

        then

        reconsider a = (f . x), b = (g . x) as Element of D by FUNCT_2: 5;

        ((o .: (f,(o9 .: (f,g)))) . x) = (o . (a,((o9 .: (f,g)) . x))) & ((o9 .: (f,g)) . x) = (o9 . (a,b)) by A3, A2, A5, FUNCOP_1: 22;

        hence (f . x) = ((o .: (f,(o9 .: (f,g)))) . x) by A1;

      end;



       A6: ( dom f) = A by FUNCT_2:def 1;

      (((o9,D) .: A) . (f,g)) = (o9 .: (f,g)) & (((o,D) .: A) . (f,(o9 .: (f,g)))) = (o .: (f,(o9 .: (f,g)))) by Def2;

      hence thesis by A6, A2, A4, FUNCT_1: 2;

    end;

    theorem :: MONOID_1:16



     Th16: for D1,D2,D,E1,E2,E be non empty set, o1 be Function of [:D1, D2:], D, o2 be Function of [:E1, E2:], E st o1 c= o2 holds ((o1,D) .: A) c= ((o2,E) .: A)

    proof

      let D1,D2,D,E1,E2,E be non empty set, o1 be Function of [:D1, D2:], D, o2 be Function of [:E1, E2:], E;



       A1: ( dom o1) = [:D1, D2:] by FUNCT_2:def 1;

      assume

       A2: o1 c= o2;

      then

       A3: ( dom o1) c= ( dom o2) by GRFUNC_1: 2;



       A4: ( dom o2) = [:E1, E2:] by FUNCT_2:def 1;

      then D2 c= E2 by A3, A1, ZFMISC_1: 114;

      then

       A5: ( Funcs (A,D2)) c= ( Funcs (A,E2)) by FUNCT_5: 56;

      D1 c= E1 by A3, A1, A4, ZFMISC_1: 114;

      then

       A6: ( Funcs (A,D1)) c= ( Funcs (A,E1)) by FUNCT_5: 56;

       A7:

      now

        let x be object;

        assume x in ( dom ((o1,D) .: A));

        then

        reconsider y = x as Element of [:( Funcs (A,D1)), ( Funcs (A,D2)):];

        reconsider g2 = (y `2 ) as Element of ( Funcs (A,E2)) by A5;

        reconsider f2 = (y `2 ) as Element of ( Funcs (A,D2));

        reconsider g1 = (y `1 ) as Element of ( Funcs (A,E1)) by A6;

        reconsider f1 = (y `1 ) as Element of ( Funcs (A,D1));



         A8: ( dom (o2 .: (g1,g2))) = A & ( dom (o1 .: (f1,f2))) = A by FUNCT_2:def 1;



         A9: ( dom f1) = A & ( dom f2) = A by FUNCT_2:def 1;

         A10:

        now

          let z be object;

          assume

           A11: z in A;

          then (f1 . z) in ( rng f1) & (f2 . z) in ( rng f2) by A9, FUNCT_1:def 3;

          then

           A12: [(f1 . z), (f2 . z)] in ( dom o1) by A1, ZFMISC_1: 87;

          ((o2 .: (g1,g2)) . z) = (o2 . ((g1 . z),(g2 . z))) & ((o1 .: (f1,f2)) . z) = (o1 . ((f1 . z),(f2 . z))) by A8, A11, FUNCOP_1: 22;

          hence ((o2 .: (g1,g2)) . z) = ((o1 .: (f1,f2)) . z) by A2, A12, GRFUNC_1: 2;

        end;



         A13: [f1, f2] = x by MCART_1: 21;

        (((o1,D) .: A) . (f1,f2)) = (o1 .: (f1,f2)) & (((o2,E) .: A) . (g1,g2)) = (o2 .: (g1,g2)) by Def2;

        hence (((o1,D) .: A) . x) = (((o2,E) .: A) . x) by A8, A10, A13, FUNCT_1: 2;

      end;

      ( dom ((o1,D) .: A)) = [:( Funcs (A,D1)), ( Funcs (A,D2)):] & ( dom ((o2,E) .: A)) = [:( Funcs (A,E1)), ( Funcs (A,E2)):] by FUNCT_2:def 1;

      then ( dom ((o1,D) .: A)) c= ( dom ((o2,E) .: A)) by A6, A5, ZFMISC_1: 96;

      hence thesis by A7, GRFUNC_1: 2;

    end;

    definition

      let G be non empty multMagma;

      let A be set;

      :: MONOID_1:def3

      func .: (G,A) -> multMagma equals

      : Def3: multLoopStr (# ( Funcs (A,the carrier of G)), ((the multF of G,the carrier of G) .: A), (A --> ( the_unity_wrt the multF of G)) #) if G is unital

      otherwise multMagma (# ( Funcs (A,the carrier of G)), ((the multF of G,the carrier of G) .: A) #);

      correctness ;

    end

    registration

      let G be non empty multMagma;

      let A be set;

      cluster ( .: (G,A)) -> non empty;

      coherence

      proof

        per cases ;

          suppose G is unital;

          then ( .: (G,A)) = multLoopStr (# ( Funcs (A,the carrier of G)), ((the multF of G,the carrier of G) .: A), (A --> ( the_unity_wrt the multF of G)) #) by Def3;

          hence the carrier of ( .: (G,A)) is non empty;

        end;

          suppose not G is unital;

          then ( .: (G,A)) = multMagma (# ( Funcs (A,the carrier of G)), ((the multF of G,the carrier of G) .: A) #) by Def3;

          hence the carrier of ( .: (G,A)) is non empty;

        end;

      end;

    end

    reserve G for non empty multMagma;

    deffunc carr( non empty multMagma) = the carrier of $1;

    theorem :: MONOID_1:17



     Th17: the carrier of ( .: (G,X)) = ( Funcs (X,the carrier of G)) & the multF of ( .: (G,X)) = ((the multF of G,the carrier of G) .: X)

    proof



       A1: not G is unital implies ( .: (G,X)) = multMagma (# ( Funcs (X, carr(G))), (( op(G), carr(G)) .: X) #) by Def3;

      G is unital implies ( .: (G,X)) = multLoopStr (# ( Funcs (X, carr(G))), (( op(G), carr(G)) .: X), (X --> ( the_unity_wrt op(G))) #) by Def3;

      hence thesis by A1;

    end;

    theorem :: MONOID_1:18

    x is Element of ( .: (G,X)) iff x is Function of X, the carrier of G

    proof

      x is Element of ( .: (G,X)) implies x is Element of ( Funcs (X, carr(G))) by Th17;

      hence x is Element of ( .: (G,X)) implies x is Function of X, carr(G);

      assume x is Function of X, carr(G);

      then

      reconsider f = x as Function of X, carr(G);



       A1: ( rng f) c= carr(G);

       carr(.:) = ( Funcs (X, carr(G))) & ( dom f) = X by Th17, FUNCT_2:def 1;

      hence thesis by A1, FUNCT_2:def 2;

    end;



     Lm1: ( .: (G,X)) is constituted-Functions

    proof

      let a be Element of ( .: (G,X));

      a is Element of ( Funcs (X, carr(G))) by Th17;

      hence thesis;

    end;

    registration

      let G be non empty multMagma, A be set;

      cluster ( .: (G,A)) -> constituted-Functions;

      coherence by Lm1;

    end

    theorem :: MONOID_1:19



     Th19: for f be Element of ( .: (G,X)) holds ( dom f) = X & ( rng f) c= the carrier of G

    proof

      let f be Element of ( .: (G,X));

      reconsider f as Element of ( Funcs (X, carr(G))) by Th17;

      f = f;

      hence thesis by FUNCT_2:def 1, RELAT_1:def 19;

    end;

    theorem :: MONOID_1:20



     Th20: for f,g be Element of ( .: (G,X)) st for x be object st x in X holds (f . x) = (g . x) holds f = g

    proof

      let f,g be Element of ( .: (G,X));

      ( dom f) = X & ( dom g) = X by Th19;

      hence thesis by FUNCT_1: 2;

    end;

    definition

      let G be non empty multMagma, A be non empty set;

      let f be Element of ( .: (G,A));

      let a be Element of A;

      :: original: .

      redefine

      func f . a -> Element of G ;

      coherence

      proof

        ( dom f) = A by Th19;

        then

         A1: (f . a) in ( rng f) by FUNCT_1:def 3;

        ( rng f) c= carr(G) by Th19;

        hence thesis by A1;

      end;

    end

    registration

      let G be non empty multMagma, A be non empty set;

      let f be Element of ( .: (G,A));

      cluster ( rng f) -> non empty;

      coherence

      proof

        set a = the Element of A;

        ( dom f) = A by Th19;

        then (f . a) in ( rng f) by FUNCT_1:def 3;

        hence thesis;

      end;

    end

    theorem :: MONOID_1:21



     Th21: for f1,f2 be Element of ( .: (G,D)), a be Element of D holds ((f1 * f2) . a) = ((f1 . a) * (f2 . a))

    proof

      let f1,f2 be Element of ( .: (G,D)), a be Element of D;

      reconsider g1 = f1, g2 = f2 as Element of ( Funcs (D, carr(G))) by Th17;

       op(.:) = (( op(G), carr(G)) .: D) by Th17;

      then ( dom ( op(G) .: (g1,g2))) = D & (f1 * f2) = ( op(G) .: (g1,g2)) by Def2, FUNCT_2:def 1;

      hence thesis by FUNCOP_1: 22;

    end;

    definition

      let G be unital non empty multMagma;

      let A be set;

      :: original: .:

      redefine

      func .: (G,A) -> well-unital constituted-Functions strict non empty multLoopStr ;

      coherence

      proof

        set M = multLoopStr (# ( Funcs (A, carr(G))), (( op(G), carr(G)) .: A), (A --> ( the_unity_wrt op(G))) #);

         op(G) is having_a_unity by MONOID_0:def 10;

        then

        consider a be Element of G such that

         A1: a is_a_unity_wrt op(G);



         A2: ( 1. M) = (A --> ( the_unity_wrt the multF of G)) & ( .: (G,A)) = M by Def3;

        a = ( the_unity_wrt op(G)) & (A --> a) is_a_unity_wrt (( op(G), carr(G)) .: A) by A1, Th9, BINOP_1:def 8;

        hence thesis by A2, MONOID_0:def 21;

      end;

    end

    theorem :: MONOID_1:22



     Th22: for G be unital non empty multMagma holds ( 1. ( .: (G,X))) = (X --> ( the_unity_wrt the multF of G))

    proof

      let G be unital non empty multMagma;

      ( .: (G,X)) = multLoopStr (# ( Funcs (X, carr(G))), (( op(G), carr(G)) .: X), (X --> ( the_unity_wrt op(G))) #) by Def3;

      hence thesis;

    end;

    theorem :: MONOID_1:23



     Th23: for G be non empty multMagma, A be set holds (G is commutative implies ( .: (G,A)) is commutative) & (G is associative implies ( .: (G,A)) is associative) & (G is idempotent implies ( .: (G,A)) is idempotent) & (G is invertible implies ( .: (G,A)) is invertible) & (G is cancelable implies ( .: (G,A)) is cancelable) & (G is uniquely-decomposable implies ( .: (G,A)) is uniquely-decomposable)

    proof

      let G;

      let A be set;



       A1: op(.:) = (( op(G), carr(G)) .: A) & carr(.:) = ( Funcs (A, carr(G))) by Th17;

      thus G is commutative implies ( .: (G,A)) is commutative by A1, Th7;

      thus G is associative implies ( .: (G,A)) is associative by A1, Th8;

      thus G is idempotent implies ( .: (G,A)) is idempotent by A1, Th11;

      thus G is invertible implies ( .: (G,A)) is invertible by A1, Th12;

      thus G is cancelable implies ( .: (G,A)) is cancelable by A1, Th13;

      assume op(G) is uniquely-decomposable;

      hence op(.:) is uniquely-decomposable by A1, Th14;

    end;

    theorem :: MONOID_1:24

    for H be non empty SubStr of G holds ( .: (H,X)) is SubStr of ( .: (G,X))

    proof

      let H be non empty SubStr of G;



       A1: op(.:) = (( op(H), carr(H)) .: X) by Th17;

       op(H) c= op(G) & op(.:) = (( op(G), carr(G)) .: X) by Th17, MONOID_0:def 23;

      hence op(.:) c= op(.:) by A1, Th16;

    end;

    theorem :: MONOID_1:25

    for G be unital non empty multMagma, H be non empty SubStr of G st ( the_unity_wrt the multF of G) in the carrier of H holds ( .: (H,X)) is MonoidalSubStr of ( .: (G,X))

    proof

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

      assume

       A1: ( the_unity_wrt the multF of G) in carr(H);

      then

      reconsider G9 = G, H9 = H as unital non empty multMagma by MONOID_0: 30;



       A2: ( the_unity_wrt op(H9)) = ( the_unity_wrt op(G9)) by A1, MONOID_0: 30;



       A3: op(.:) = (( op(H), carr(H)) .: X) by Th17;

       op(H) c= op(G) & op(.:) = (( op(G), carr(G)) .: X) by Th17, MONOID_0:def 23;

      then

       A4: op(.:) c= op(.:) by A3, Th16;

      ( 1. ( .: (G9,X))) = (X --> ( the_unity_wrt op(G))) & ( 1. ( .: (H9,X))) = (X --> ( the_unity_wrt op(H))) by Th22;

      hence thesis by A2, A4, MONOID_0:def 25;

    end;

    definition

      let G be unital associative commutative cancelable uniquely-decomposable non empty multMagma;

      let A be set;

      :: original: .:

      redefine

      func .: (G,A) -> commutative cancelable uniquely-decomposable constituted-Functions strict Monoid ;

      coherence

      proof

        ( .: (G,A)) is commutative cancelable by Th23;

        hence thesis by Th23;

      end;

    end

    begin

    definition

      let A be set;

      :: MONOID_1:def4

      func MultiSet_over A -> commutative cancelable uniquely-decomposable constituted-Functions strict Monoid equals ( .: ( <NAT,+,0> ,A));

      correctness ;

    end

    theorem :: MONOID_1:26



     Th26: the carrier of ( MultiSet_over X) = ( Funcs (X, NAT )) & the multF of ( MultiSet_over X) = (( addnat , NAT ) .: X) & ( 1. ( MultiSet_over X)) = (X --> 0 )

    proof

       the multMagma of <NAT,+,0> = <NAT,+> & ( the_unity_wrt op(<NAT,+>)) = 0 by MONOID_0: 40, MONOID_0:def 22;

      hence thesis by Th17, Th22, MONOID_0: 46;

    end;

    definition

      let A be set;

      mode Multiset of A is Element of ( MultiSet_over A);

    end

    theorem :: MONOID_1:27



     Th27: x is Multiset of X iff x is Function of X, NAT

    proof

       A1:

      now

        let x be Function of X, NAT ;

        ( dom x) = X & ( rng x) c= NAT by FUNCT_2:def 1;

        hence x is Element of ( Funcs (X, NAT )) by FUNCT_2:def 2;

      end;

      x is Multiset of X iff x is Element of ( Funcs (X, NAT )) by Th26;

      hence thesis by A1;

    end;

    theorem :: MONOID_1:28



     Th28: for m be Multiset of X holds ( dom m) = X & ( rng m) c= NAT

    proof

      let m be Multiset of X;

      m is Function of X, NAT by Th27;

      hence thesis by FUNCT_2:def 1, RELAT_1:def 19;

    end;

    registration

      let X;

      cluster -> NAT -valued for Multiset of X;

      coherence by Th28;

    end

    theorem :: MONOID_1:29



     Th29: for m1,m2 be Multiset of D, a be Element of D holds ((m1 [*] m2) . a) = ((m1 . a) + (m2 . a))

    proof

      reconsider N = <NAT,+,0> as non empty multMagma;

      let m1,m2 be Multiset of D, a be Element of D;

      reconsider f1 = m1, f2 = m2 as Element of ( .: (N,D));



      thus ((m1 [*] m2) . a) = ((f1 . a) * (f2 . a)) by Th21

      .= ((m1 . a) + (m2 . a)) by MONOID_0: 45;

    end;

    theorem :: MONOID_1:30



     Th30: ( chi (Y,X)) is Multiset of X

    proof

      ( rng ( chi (Y,X))) c= { 0 , 1};

      then

       A1: ( rng ( chi (Y,X))) c= NAT by XBOOLE_1: 1;

      ( dom ( chi (Y,X))) = X & carr(MultiSet_over) = ( Funcs (X, NAT )) by Th26, FUNCT_3:def 3;

      hence thesis by A1, FUNCT_2:def 2;

    end;

    definition

      let Y, X;

      :: original: chi

      redefine

      func chi (Y,X) -> Multiset of X ;

      coherence by Th30;

    end

    definition

      let X;

      let n be Element of NAT ;

      :: original: -->

      redefine

      func X --> n -> Multiset of X ;

      coherence

      proof

        thus (X --> n) is Multiset of X by Th27;

      end;

    end

    definition

      let A be non empty set, a be Element of A;

      :: MONOID_1:def5

      func chi a -> Multiset of A equals ( chi ( {a},A));

      coherence ;

    end

    theorem :: MONOID_1:31



     Th31: for A be non empty set, a,b be Element of A holds (( chi a) . a) = 1 & (b <> a implies (( chi a) . b) = 0 )

    proof

      let A be non empty set, a,b be Element of A;



       A1: b <> a implies not b in {a} by TARSKI:def 1;

      a in {a} by TARSKI:def 1;

      hence thesis by A1, FUNCT_3:def 3;

    end;

    reserve A for non empty set,

a for Element of A,

p for FinSequence of A,

m1,m2 for Multiset of A;

    theorem :: MONOID_1:32



     Th32: (for a holds (m1 . a) = (m2 . a)) implies m1 = m2

    proof

      assume for a holds (m1 . a) = (m2 . a);

      then for x be object st x in A holds (m1 . x) = (m2 . x);

      hence thesis by Th20;

    end;

    definition

      let A be set;

      :: MONOID_1:def6

      func finite-MultiSet_over A -> strict non empty MonoidalSubStr of ( MultiSet_over A) means

      : Def6: for f be Multiset of A holds f in the carrier of it iff (f " ( NAT \ { 0 })) is finite;

      existence

      proof

        reconsider e = (A --> 0 ) as Function of A, NAT by Th27;

        defpred P[ set] means ex f be Function of A, NAT st $1 = f & (f " ( NAT \ { 0 })) is finite;



         A1: for a,b be Multiset of A holds P[a] & P[b] implies P[(a [*] b)]

        proof

          let a,b be Multiset of A;

          reconsider h = (a [*] b) as Function of A, NAT by Th27;

          given f be Function of A, NAT such that

           A2: a = f and

           A3: (f " ( NAT \ { 0 })) is finite;

          given g be Function of A, NAT such that

           A4: b = g and

           A5: (g " ( NAT \ { 0 })) is finite;

          take h;



           A6: ( dom f) = A & ( dom g) = A by FUNCT_2:def 1;

          (h " ( NAT \ { 0 })) c= ((f " ( NAT \ { 0 })) \/ (g " ( NAT \ { 0 })))

          proof

            let x be object;

            assume

             A7: x in (h " ( NAT \ { 0 }));

            then (h . x) in ( NAT \ { 0 }) by FUNCT_1:def 7;

            then

             A8: not (h . x) in { 0 } by XBOOLE_0:def 5;

            (f . x) in ( rng f) & (g . x) in ( rng g) by A6, A7, FUNCT_1:def 3;

            then

            reconsider n = (f . x), m = (g . x) as Element of NAT ;

            (h . x) = (n + m) by A2, A4, A7, Th29;

            then n <> 0 or m <> 0 by A8, TARSKI:def 1;

            then not n in { 0 } or not m in { 0 } by TARSKI:def 1;

            then n in ( NAT \ { 0 }) or m in ( NAT \ { 0 }) by XBOOLE_0:def 5;

            then x in (f " ( NAT \ { 0 })) or x in (g " ( NAT \ { 0 })) by A6, A7, FUNCT_1:def 7;

            hence thesis by XBOOLE_0:def 3;

          end;

          hence thesis by A3, A5;

        end;



         A9: ( dom e) = A;

        now

          set x = the Element of (e " ( NAT \ { 0 }));

          assume

           A10: (e " ( NAT \ { 0 })) <> {} ;

          then (e . x) in ( NAT \ { 0 }) by FUNCT_1:def 7;

          then

           A11: not (e . x) in { 0 } by XBOOLE_0:def 5;

          x in A by A9, A10, FUNCT_1:def 7;

          then (e . x) = 0 by FUNCOP_1: 7;

          hence contradiction by A11, TARSKI:def 1;

        end;

        then

         A12: P[( 1. ( MultiSet_over A))] by Th26;

        consider M be strict non empty MonoidalSubStr of ( MultiSet_over A) such that

         A13: for a be Multiset of A holds a in the carrier of M iff P[a] from MONOID_0:sch 2( A1, A12);

        reconsider M as strict non empty MonoidalSubStr of ( MultiSet_over A);

        take M;

        let f be Multiset of A;

        thus f in carr(M) implies (f " ( NAT \ { 0 })) is finite

        proof

          assume f in carr(M);

          then ex g be Function of A, NAT st f = g & (g " ( NAT \ { 0 })) is finite by A13;

          hence thesis;

        end;

        reconsider g = f as Function of A, NAT by Th27;

        assume (f " ( NAT \ { 0 })) is finite;

        then (g " ( NAT \ { 0 })) is finite;

        hence thesis by A13;

      end;

      uniqueness

      proof

        set M = ( MultiSet_over A);

        let M1,M2 be strict non empty MonoidalSubStr of ( MultiSet_over A) such that

         A14: for f be Multiset of A holds f in carr(M1) iff (f " ( NAT \ { 0 })) is finite and

         A15: for f be Multiset of A holds f in carr(M2) iff (f " ( NAT \ { 0 })) is finite;



         A16: carr(M2) c= carr(M) by MONOID_0: 23;



         A17: carr(M1) c= carr(M) by MONOID_0: 23;

         carr(M1) = carr(M2)

        proof

          thus carr(M1) c= carr(M2)

          proof

            let x be object;

            assume

             A18: x in carr(M1);

            then

            reconsider f = x as Multiset of A by A17;

            (f " ( NAT \ { 0 })) is finite by A14, A18;

            hence thesis by A15;

          end;

          let x be object;

          assume

           A19: x in carr(M2);

          then

          reconsider f = x as Multiset of A by A16;

          (f " ( NAT \ { 0 })) is finite by A15, A19;

          hence thesis by A14;

        end;

        hence thesis by MONOID_0: 27;

      end;

    end

    theorem :: MONOID_1:33



     Th33: ( chi a) is Element of ( finite-MultiSet_over A)

    proof

      (( chi a) " ( NAT \ { 0 })) c= {a}

      proof

        let x be object;

        assume

         A1: x in (( chi a) " ( NAT \ { 0 }));

        then x in ( dom ( chi a)) by FUNCT_1:def 7;

        then

        reconsider y = x as Element of A by Th28;

        (( chi a) . x) in ( NAT \ { 0 }) by A1, FUNCT_1:def 7;

        then not (( chi a) . y) in { 0 } by XBOOLE_0:def 5;

        then (( chi a) . y) <> 0 by TARSKI:def 1;

        then y = a by Th31;

        hence thesis by TARSKI:def 1;

      end;

      hence thesis by Def6;

    end;

    theorem :: MONOID_1:34



     Th34: ( dom ( {x} |` (p ^ <*x*>))) = (( dom ( {x} |` p)) \/ {(( len p) + 1)})

    proof

      thus ( dom ( {x} |` (p ^ <*x*>))) c= (( dom ( {x} |` p)) \/ {(( len p) + 1)})

      proof

        let a be object;



         A1: ( len <*x*>) = 1 by FINSEQ_1: 40;



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

        assume

         A3: a in ( dom ( {x} |` (p ^ <*x*>)));

        then

         A4: a in ( dom (p ^ <*x*>)) by FUNCT_1: 54;

        then a in ( Seg (( len p) + ( len <*x*>))) by FINSEQ_1:def 7;

        then a in (( Seg ( len p)) \/ {(( len p) + 1)}) by A1, FINSEQ_1: 9;

        then

         A5: a in ( dom p) or a in {(( len p) + 1)} by A2, XBOOLE_0:def 3;



         A6: ((p ^ <*x*>) . a) in {x} by A3, FUNCT_1: 54;

        reconsider a as Element of NAT by A4;

        a in ( dom p) implies ((p ^ <*x*>) . a) = (p . a) by FINSEQ_1:def 7;

        then a in ( dom p) implies a in ( dom ( {x} |` p)) by A6, FUNCT_1: 54;

        hence thesis by A5, XBOOLE_0:def 3;

      end;

      let a be object;

      ( len <*x*>) = 1 by FINSEQ_1: 40;

      then

       A7: ( dom (p ^ <*x*>)) = ( Seg (( len p) + 1)) by FINSEQ_1:def 7;

      assume

       A8: a in (( dom ( {x} |` p)) \/ {(( len p) + 1)});

      then a in ( dom ( {x} |` p)) or a in {(( len p) + 1)} by XBOOLE_0:def 3;

      then

       A9: a in ( dom p) & (p . a) in {x} or a in {(( len p) + 1)} & a = (( len p) + 1) & x in {x} by FUNCT_1: 54, TARSKI:def 1;

      ( Seg ( len p)) = ( dom p) & ( Seg (( len p) + 1)) = (( Seg ( len p)) \/ {(( len p) + 1)}) by FINSEQ_1: 9, FINSEQ_1:def 3;

      then

       A10: ((p ^ <*x*>) . (( len p) + 1)) = x & a in ( dom (p ^ <*x*>)) by A9, A7, FINSEQ_1: 42, XBOOLE_0:def 3;

      reconsider a as Element of NAT by A8;

      a in ( dom p) implies ((p ^ <*x*>) . a) = (p . a) by FINSEQ_1:def 7;

      hence thesis by A9, A10, FUNCT_1: 54;

    end;

    theorem :: MONOID_1:35



     Th35: x <> y implies ( dom ( {x} |` (p ^ <*y*>))) = ( dom ( {x} |` p))

    proof

      assume

       A1: x <> y;

      thus ( dom ( {x} |` (p ^ <*y*>))) c= ( dom ( {x} |` p))

      proof

        let a be object;



         A2: ( len <*y*>) = 1 by FINSEQ_1: 40;



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

        assume

         A4: a in ( dom ( {x} |` (p ^ <*y*>)));

        then

         A5: a in ( dom (p ^ <*y*>)) by FUNCT_1: 54;

        then a in ( Seg (( len p) + ( len <*y*>))) by FINSEQ_1:def 7;

        then a in (( Seg ( len p)) \/ {(( len p) + 1)}) by A2, FINSEQ_1: 9;

        then

         A6: a in ( dom p) or a in {(( len p) + 1)} by A3, XBOOLE_0:def 3;



         A7: ((p ^ <*y*>) . a) in {x} by A4, FUNCT_1: 54;

        reconsider a as Element of NAT by A5;



         A8: ((p ^ <*y*>) . (( len p) + 1)) = y & not y in {x} by A1, FINSEQ_1: 42, TARSKI:def 1;

        then ((p ^ <*y*>) . a) = (p . a) by A7, A6, FINSEQ_1:def 7, TARSKI:def 1;

        hence thesis by A7, A6, A8, FUNCT_1: 54, TARSKI:def 1;

      end;

      let a be object;

      assume

       A9: a in ( dom ( {x} |` p));

      then

       A10: a in ( dom p) by FUNCT_1: 54;

      ( len <*y*>) = 1 by FINSEQ_1: 40;

      then

       A11: ( dom (p ^ <*y*>)) = ( Seg (( len p) + 1)) by FINSEQ_1:def 7;

      ( Seg ( len p)) = ( dom p) & ( Seg (( len p) + 1)) = (( Seg ( len p)) \/ {(( len p) + 1)}) by FINSEQ_1: 9, FINSEQ_1:def 3;

      then

       A12: a in ( dom (p ^ <*y*>)) by A10, A11, XBOOLE_0:def 3;



       A13: (p . a) in {x} by A9, FUNCT_1: 54;

      reconsider a as Element of NAT by A9;

      ((p ^ <*y*>) . a) = (p . a) by A10, FINSEQ_1:def 7;

      hence thesis by A13, A12, FUNCT_1: 54;

    end;

    definition

      let A be non empty set, p be FinSequence of A;

      :: MONOID_1:def7

      func |.p.| -> Multiset of A means

      : Def7: for a be Element of A holds (it . a) = ( card ( dom ( {a} |` p)));

      existence

      proof

        deffunc F( Element of A) = ( card ( dom ( {$1} |` p)));

        consider m be Function of A, NAT such that

         A1: for a be Element of A holds (m . a) = F(a) from FUNCT_2:sch 4;

        m is Multiset of A by Th27;

        hence thesis by A1;

      end;

      uniqueness

      proof

        let m1,m2 be Multiset of A such that

         A2: for a be Element of A holds (m1 . a) = ( card ( dom ( {a} |` p))) and

         A3: for a be Element of A holds (m2 . a) = ( card ( dom ( {a} |` p)));

        now

          let a be Element of A;



          thus (m1 . a) = ( card ( dom ( {a} |` p))) by A2

          .= (m2 . a) by A3;

        end;

        hence thesis by Th32;

      end;

    end

    theorem :: MONOID_1:36

    ( |.( <*> A).| . a) = 0

    proof

      ( dom ( {a} |` {} )) c= ( dom {} ) by FUNCT_1: 56;

      then ( dom ( {a} |` ( <*> A))) = {} ;

      hence thesis by Def7, CARD_1: 27;

    end;

    theorem :: MONOID_1:37



     Th37: |.( <*> A).| = (A --> 0 )

    proof

       A1:

      now

        let x be object;

        assume x in A;

        then

        reconsider a = x as Element of A;



        thus ( |.( <*> A).| . x) = ( card ( dom ( {a} |` {} ))) by Def7

        .= 0 by CARD_1: 27, RELAT_1: 38, RELAT_1: 107;

      end;

      ( dom |.( <*> A).|) = A by Th28;

      hence thesis by A1, FUNCOP_1: 11;

    end;

    theorem :: MONOID_1:38

     |. <*a*>.| = ( chi a)

    proof



       A1: ( rng <*a*>) = {a} by FINSEQ_1: 39;

      now

        let b be Element of A;

        set x = b;



         A2: ( dom <*a*>) = ( Seg 1) & ( card ( Seg 1)) = 1 by FINSEQ_1: 38, FINSEQ_1: 57;

        a <> x implies {x} misses {a} by ZFMISC_1: 11;

        then

         A3: a <> x implies ( {x} /\ {a}) = {} ;



         A4: (( chi a) . a) = 1 & ( {a} |` <*a*>) = <*a*> by A1, Th31;

         <*a*> = (( rng <*a*>) |` <*a*>);

        then ( {x} |` <*a*>) = (( {x} /\ ( rng <*a*>)) |` <*a*>) by RELAT_1: 96;

        then x <> a implies ( {x} |` <*a*>) = {} & (( chi a) . b) = 0 by A1, A3, Th31;

        hence ( |. <*a*>.| . x) = (( chi a) . x) by A2, A4, Def7, CARD_1: 27, RELAT_1: 38;

      end;

      hence thesis by Th32;

    end;

    reserve p,q for FinSequence of A;

    theorem :: MONOID_1:39



     Th39: |.(p ^ <*a*>).| = ( |.p.| [*] ( chi a))

    proof

      now

        reconsider pa = (p ^ <*a*>) as FinSequence of A;

        let b be Element of A;

        ( len p) < (( len p) + 1) & ( dom ( {b} |` p)) c= ( dom p) by FUNCT_1: 56, NAT_1: 13;

        then

         A1: not (( len p) + 1) in ( dom ( {b} |` p)) by FINSEQ_3: 25;



         A2: ( |.(p ^ <*a*>).| . b) = ( card ( dom ( {b} |` pa))) & ( |.p.| . b) = ( card ( dom ( {b} |` p))) by Def7;



         A3: a <> b implies ( dom ( {b} |` (p ^ <*a*>))) = ( dom ( {b} |` p)) & (( chi a) . b) = 0 by Th31, Th35;



         A4: (( |.p.| [*] ( chi a)) . b) = (( |.p.| . b) + (( chi a) . b)) by Th29;

        ( dom ( {a} |` (p ^ <*a*>))) = (( dom ( {a} |` p)) \/ {(( len p) + 1)}) & (( chi a) . a) = 1 by Th31, Th34;

        hence ( |.(p ^ <*a*>).| . b) = (( |.p.| [*] ( chi a)) . b) by A1, A2, A3, A4, CARD_2: 41;

      end;

      hence thesis by Th32;

    end;

    theorem :: MONOID_1:40



     Th40: |.(p ^ q).| = ( |.p.| [*] |.q.|)

    proof

      defpred P[ Nat] means for q st ( len q) = $1 holds |.(p ^ q).| = ( |.p.| [*] |.q.|);



       A1: ( len q) = ( len q);



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

      proof

        let n be Nat such that

         A3: for q st ( len q) = n holds |.(p ^ q).| = ( |.p.| [*] |.q.|);

        let q;

        assume

         A4: ( len q) = (n + 1);

        then q <> {} ;

        then

        consider r be FinSequence, x be object such that

         A5: q = (r ^ <*x*>) by FINSEQ_1: 46;

        ( rng <*x*>) = {x} by FINSEQ_1: 39;

        then {x} c= ( rng q) by A5, FINSEQ_1: 30;

        then

         A6: {x} c= A by XBOOLE_1: 1;

        reconsider r as FinSequence of A by A5, FINSEQ_1: 36;

        ( len <*x*>) = 1 by FINSEQ_1: 40;

        then

         A7: (n + 1) = (( len r) + 1) by A4, A5, FINSEQ_1: 22;

        reconsider x as Element of A by A6, ZFMISC_1: 31;



        thus |.(p ^ q).| = |.((p ^ r) ^ <*x*>).| by A5, FINSEQ_1: 32

        .= ( |.(p ^ r).| [*] ( chi x)) by Th39

        .= (( |.p.| [*] |.r.|) [*] ( chi x)) by A3, A7

        .= ( |.p.| [*] ( |.r.| [*] ( chi x))) by GROUP_1:def 3

        .= ( |.p.| [*] |.q.|) by A5, Th39;

      end;



       A8: P[ 0 ]

      proof

        let q;



         A9: |.( <*> A).| = (A --> 0 ) & (A --> 0 ) = un(MultiSet_over) by Th26, Th37;

        assume ( len q) = 0 ;

        then

         A10: q = {} ;

        then (p ^ q) = p by FINSEQ_1: 34;

        hence thesis by A10, A9, MONOID_0: 16;

      end;

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

      hence thesis by A1;

    end;

    theorem :: MONOID_1:41



     Th41: ( |.(n .--> a).| . a) = n & for b be Element of A st b <> a holds ( |.(n .--> a).| . b) = 0

    proof

      defpred P[ Nat] means ( |.(( In ($1, NAT )) .--> a).| . a) = $1;



       A1: ( 0 .--> a) = {} & {} = ( <*> A) by FINSEQ_2: 58;



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

      proof

        let n be Nat such that

         A3: ( |.(( In (n, NAT )) .--> a).| . a) = n;



        thus ( |.(( In ((n + 1), NAT )) .--> a).| . a) = ( |.((( In (n, NAT )) .--> a) ^ <*a*>).| . a) by FINSEQ_2: 60

        .= (( |.(( In (n, NAT )) .--> a).| [*] ( chi a)) . a) by Th39

        .= (n + (( chi a) . a)) by A3, Th29

        .= (n + 1) by Th31;

      end;

      ((A --> 0 ) . a) = 0 ;

      then

       A4: P[ 0 ] by A1, Th37;

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

      then ( |.(( In (n, NAT )) .--> a).| . a) = n;

      hence ( |.(n .--> a).| . a) = n;

      let b be Element of A such that

       A5: b <> a;

      defpred P[ Nat] means ( |.(( In ($1, NAT )) .--> a).| . b) = 0 ;



       A6: for n be Nat st P[n] holds P[(n + 1)]

      proof

        let n be Nat such that

         A7: ( |.(( In (n, NAT )) .--> a).| . b) = 0 ;



        thus ( |.(( In ((n + 1), NAT )) .--> a).| . b) = ( |.((( In (n, NAT )) .--> a) ^ <*a*>).| . b) by FINSEQ_2: 60

        .= (( |.(( In (n, NAT )) .--> a).| [*] ( chi a)) . b) by Th39

        .= ( 0 + (( chi a) . b)) by A7, Th29

        .= 0 by A5, Th31;

      end;

      ((A --> 0 ) . b) = 0 ;

      then

       A8: P[ 0 ] by A1, Th37;

      for n be Nat holds P[n] from NAT_1:sch 2( A8, A6);

      then P[n];

      hence thesis;

    end;

    reserve fm for Element of ( finite-MultiSet_over A);

    theorem :: MONOID_1:42

     |.p.| is Element of ( finite-MultiSet_over A)

    proof

      defpred P[ FinSequence of A] means |.$1.| is Element of ( finite-MultiSet_over A);

      defpred Q[ Nat] means for p st ( len p) = $1 holds P[p];



       A1: ( len p) = ( len p);



       A2: for n be Nat st Q[n] holds Q[(n + 1)]

      proof

        set M = ( finite-MultiSet_over A);

        let n be Nat such that

         A3: for p st ( len p) = n holds P[p];

        let p;

        assume

         A4: ( len p) = (n + 1);

        then p <> {} ;

        then

        consider r be FinSequence, x be object such that

         A5: p = (r ^ <*x*>) by FINSEQ_1: 46;

        ( rng <*x*>) = {x} by FINSEQ_1: 39;

        then {x} c= ( rng p) by A5, FINSEQ_1: 30;

        then

         A6: {x} c= A by XBOOLE_1: 1;

        reconsider r as FinSequence of A by A5, FINSEQ_1: 36;



         A7: ( len <*x*>) = 1 by FINSEQ_1: 40;

        reconsider x as Element of A by A6, ZFMISC_1: 31;

        (n + 1) = (( len r) + 1) by A4, A5, A7, FINSEQ_1: 22;

        then

        reconsider r9 = |.r.|, a = ( chi x) as Element of M by A3, Th33;

        M is SubStr of ( MultiSet_over A) by MONOID_0: 21;



        then (r9 [*] a) = ( |.r.| [*] ( chi x)) by MONOID_0: 25

        .= |.p.| by A5, Th39;

        hence thesis;

      end;



       A8: Q[ 0 ]

      proof

        let p;

        assume ( len p) = 0 ;

        then p = ( <*> A);



        then |.p.| = (A --> 0 ) by Th37

        .= un(MultiSet_over) by Th26

        .= un(finite-MultiSet_over) by MONOID_0:def 24;

        hence thesis;

      end;

      for n be Nat holds Q[n] from NAT_1:sch 2( A8, A2);

      hence thesis by A1;

    end;

    theorem :: MONOID_1:43

    x is Element of ( finite-MultiSet_over A) implies ex p st x = |.p.|

    proof

      defpred Z[ Nat] means for fm st for V be finite set st V = (fm " ( NAT \ { 0 })) holds ( card V) = $1 holds ex p st fm = |.p.|;

      assume x is Element of ( finite-MultiSet_over A);

      then

      reconsider m = x as Element of ( finite-MultiSet_over A);

       carr(finite-MultiSet_over) c= carr(MultiSet_over) by MONOID_0: 23;

      then m is Multiset of A;

      then

      reconsider V = (m " ( NAT \ { 0 })) as finite set by Def6;



       A1: for V9 be finite set st V9 = (m " ( NAT \ { 0 })) holds ( card V9) = ( card V);



       A2: for n be Nat st Z[n] holds Z[(n + 1)]

      proof

        deffunc F( object) = 0 ;

        let n be Nat such that

         A3: for fm st for V be finite set st V = (fm " ( NAT \ { 0 })) holds ( card V) = n holds ex p st fm = |.p.|;

        let fm such that

         A4: for V be finite set st V = (fm " ( NAT \ { 0 })) holds ( card V) = (n + 1);

        deffunc G( object) = (fm . $1);

        set x = the Element of (fm " ( NAT \ { 0 }));

         carr(finite-MultiSet_over) c= carr(MultiSet_over) by MONOID_0: 23;

        then

        reconsider m = fm as Multiset of A;

        reconsider V = (m " ( NAT \ { 0 })) as finite set by Def6;



         A5: ( card V) = (n + 1) by A4;



         A6: ( dom m) = A by Th28;

        then

        reconsider x as Element of A by A5, CARD_1: 27, FUNCT_1:def 7;

        defpred C[ object] means x = $1;

        consider f be Function such that

         A7: ( dom f) = A & for a be object st a in A holds ( C[a] implies (f . a) = F(a)) & ( not C[a] implies (f . a) = G(a)) from PARTFUN1:sch 1;

        ( rng f) c= NAT

        proof

          let y be object;

          assume y in ( rng f);

          then

          consider z be object such that

           A8: z in ( dom f) and

           A9: y = (f . z) by FUNCT_1:def 3;

          reconsider z as Element of A by A7, A8;

          y = 0 or y = (m . z) by A7, A9;

          hence thesis;

        end;

        then

        reconsider f as Function of A, NAT by A7, FUNCT_2:def 1, RELSET_1: 4;

        reconsider f as Multiset of A by Th27;



         A10: (f " ( NAT \ { 0 })) = ((fm " ( NAT \ { 0 })) \ {x})

        proof

          thus (f " ( NAT \ { 0 })) c= ((fm " ( NAT \ { 0 })) \ {x})

          proof

            let y be object;

            assume

             A11: y in (f " ( NAT \ { 0 }));

            then

            reconsider a = y as Element of A by A7, FUNCT_1:def 7;



             A12: (f . y) in ( NAT \ { 0 }) by A11, FUNCT_1:def 7;

            then not (f . a) in { 0 } by XBOOLE_0:def 5;

            then

             A13: (f . a) <> 0 by TARSKI:def 1;

            then a <> x by A7;

            then

             A14: not a in {x} by TARSKI:def 1;

            (f . a) = (fm . a) by A7, A13;

            then a in (fm " ( NAT \ { 0 })) by A6, A12, FUNCT_1:def 7;

            hence thesis by A14, XBOOLE_0:def 5;

          end;

          let y be object;

          assume

           A15: y in ((fm " ( NAT \ { 0 })) \ {x});

          then

           A16: y in ( dom fm) by FUNCT_1:def 7;



           A17: (fm . y) in ( NAT \ { 0 }) by A15, FUNCT_1:def 7;

           not y in {x} by A15, XBOOLE_0:def 5;

          then y <> x by TARSKI:def 1;

          then (fm . y) = (f . y) by A6, A7, A16;

          hence thesis by A6, A7, A16, A17, FUNCT_1:def 7;

        end;

        then

        reconsider f9 = f as Element of ( finite-MultiSet_over A) by A5, Def6;

        set g = |.((m . x) .--> x).|;



         A18: ( card {x}) = 1 by CARD_1: 30;

        reconsider V9 = (f9 " ( NAT \ { 0 })) as finite set by Def6;

         {x} c= (fm " ( NAT \ { 0 })) by A5, CARD_1: 27, ZFMISC_1: 31;



        then ( card V9) = ((n + 1) - 1) by A5, A10, A18, CARD_2: 44

        .= n;

        then for V be finite set st V = (f9 " ( NAT \ { 0 })) holds ( card V) = n;

        then

        consider p such that

         A19: f = |.p.| by A3;

        take q = (p ^ ((m . x) .--> x));

        now

          let a;



           A20: ( 0 + (m . a)) = (m . a);



           A21: a <> x implies (f . a) = (m . a) & (g . a) = 0 by A7, Th41;

          (f . x) = 0 & (g . x) = (m . x) by A7, Th41;

          hence ((f [*] g) . a) = (m . a) by A20, A21, Th29;

        end;



        hence fm = (f [*] g) by Th32

        .= |.q.| by A19, Th40;

      end;



       A22: Z[ 0 ]

      proof

        set a = the Element of A;

        let fm such that

         A23: for V be finite set st V = (fm " ( NAT \ { 0 })) holds ( card V) = 0 ;

         carr(finite-MultiSet_over) c= carr(MultiSet_over) by MONOID_0: 23;

        then

        reconsider m = fm as Multiset of A;

        reconsider V = (m " ( NAT \ { 0 })) as finite set by Def6;

        ( card V) = 0 by A23;

        then (fm " ( NAT \ { 0 })) = {} ;

        then ( rng fm) misses ( NAT \ { 0 }) by RELAT_1: 138;



        then

         A24: {} = (( rng fm) /\ ( NAT \ { 0 }))

        .= ((( rng fm) /\ NAT ) \ { 0 }) by XBOOLE_1: 49;

        take p = ( <*> A);

        ( rng m) c= NAT ;

        then (( rng fm) /\ NAT ) = ( rng fm) by XBOOLE_1: 28;

        then

         A25: ( rng fm) c= { 0 } by A24, XBOOLE_1: 37;



         A26: ( dom m) = A by Th28;

        then

         A27: (fm . a) in ( rng fm) by FUNCT_1:def 3;

        then (fm . a) = 0 by A25, TARSKI:def 1;

        then { 0 } c= ( rng fm) by A27, ZFMISC_1: 31;

        then ( rng fm) = { 0 } by A25;



        hence fm = (A --> 0 ) by A26, FUNCOP_1: 9

        .= |.p.| by Th37;

      end;

      for n be Nat holds Z[n] from NAT_1:sch 2( A22, A2);

      hence thesis by A1;

    end;

    begin

    reserve a,b,c for Element of D;

    definition

      let D1,D2,D be non empty set, f be Function of [:D1, D2:], D;

      :: MONOID_1:def8

      func f .:^2 -> Function of [:( bool D1), ( bool D2):], ( bool D) means

      : Def8: for x be Element of [:( bool D1), ( bool D2):] holds (it . x) = (f .: [:(x `1 ), (x `2 ):]);

      existence

      proof

        deffunc F( Element of [:( bool D1), ( bool D2):]) = (f .: [:($1 `1 ), ($1 `2 ):]);

        ex f be Function of [:( bool D1), ( bool D2):], ( bool D) st for x be Element of [:( bool D1), ( bool D2):] holds (f . x) = F(x) from FUNCT_2:sch 4;

        hence thesis;

      end;

      uniqueness

      proof

        let F1,F2 be Function of [:( bool D1), ( bool D2):], ( bool D) such that

         A1: for x be Element of [:( bool D1), ( bool D2):] holds (F1 . x) = (f .: [:(x `1 ), (x `2 ):]) and

         A2: for x be Element of [:( bool D1), ( bool D2):] holds (F2 . x) = (f .: [:(x `1 ), (x `2 ):]);

        now

          let x be Element of [:( bool D1), ( bool D2):];



          thus (F1 . x) = (f .: [:(x `1 ), (x `2 ):]) by A1

          .= (F2 . x) by A2;

        end;

        hence thesis by FUNCT_2: 63;

      end;

    end

    theorem :: MONOID_1:44



     Th44: for D1,D2,D be non empty set, f be Function of [:D1, D2:], D holds for X1 be Subset of D1, X2 be Subset of D2 holds ((f .:^2 ) . (X1,X2)) = (f .: [:X1, X2:])

    proof

      let D1,D2,D be non empty set, f be Function of [:D1, D2:], D;

      let X1 be Subset of D1, X2 be Subset of D2;

      ( [X1, X2] `1 ) = X1 & ( [X1, X2] `2 ) = X2;

      hence thesis by Def8;

    end;

    theorem :: MONOID_1:45



     Th45: for D1,D2,D be non empty set, f be Function of [:D1, D2:], D holds for X1 be Subset of D1, X2 be Subset of D2, x1,x2 be set st x1 in X1 & x2 in X2 holds (f . (x1,x2)) in ((f .:^2 ) . (X1,X2))

    proof

      let D1,D2,D be non empty set, f be Function of [:D1, D2:], D;

      let X1 be Subset of D1, X2 be Subset of D2, x1,x2 be set;

      assume that

       A1: x1 in X1 and

       A2: x2 in X2;

      reconsider b = x2 as Element of D2 by A2;

      reconsider a = x1 as Element of D1 by A1;



       A3: ((f .:^2 ) . (X1,X2)) = (f .: [:X1, X2:]) & ( dom f) = [:D1, D2:] by Th44, FUNCT_2:def 1;

       [a, b] in [:X1, X2:] by A1, A2, ZFMISC_1: 87;

      hence thesis by A3, FUNCT_1:def 6;

    end;

    theorem :: MONOID_1:46

    for D1,D2,D be non empty set, f be Function of [:D1, D2:], D holds for X1 be Subset of D1, X2 be Subset of D2 holds ((f .:^2 ) . (X1,X2)) = { (f . (a,b)) where a be Element of D1, b be Element of D2 : a in X1 & b in X2 }

    proof

      let D1,D2,D be non empty set, f be Function of [:D1, D2:], D;

      let X1 be Subset of D1, X2 be Subset of D2;

      set A = { (f . (a,b)) where a be Element of D1, b be Element of D2 : a in X1 & b in X2 };



       A1: ((f .:^2 ) . (X1,X2)) = (f .: [:X1, X2:]) by Th44;

      thus ((f .:^2 ) . (X1,X2)) c= A

      proof

        let x be object;

        assume x in ((f .:^2 ) . (X1,X2));

        then

        consider y be object such that y in ( dom f) and

         A2: y in [:X1, X2:] and

         A3: x = (f . y) by A1, FUNCT_1:def 6;

        consider y1,y2 be object such that

         A4: y1 in X1 and

         A5: y2 in X2 and

         A6: y = [y1, y2] by A2, ZFMISC_1: 84;

        reconsider y2 as Element of D2 by A5;

        reconsider y1 as Element of D1 by A4;

        x = (f . (y1,y2)) by A3, A6;

        hence thesis by A4, A5;

      end;

      let x be object;

      assume x in A;

      then ex a be Element of D1, b be Element of D2 st x = (f . (a,b)) & a in X1 & b in X2;

      hence thesis by Th45;

    end;

    theorem :: MONOID_1:47



     Th47: o is commutative implies (o .: [:X, Y:]) = (o .: [:Y, X:])

    proof

      assume

       A1: (o . (a,b)) = (o . (b,a));

      now

        let X, Y;

        thus (o .: [:X, Y:]) c= (o .: [:Y, X:])

        proof

          let x be object;

          assume x in (o .: [:X, Y:]);

          then

          consider y be object such that

           A2: y in ( dom o) and

           A3: y in [:X, Y:] and

           A4: x = (o . y) by FUNCT_1:def 6;

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

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

          then (y `1 ) in X & (y `2 ) in Y by A3, ZFMISC_1: 87;

          then

           A5: [(y `2 ), (y `1 )] in [:Y, X:] by ZFMISC_1: 87;



           A6: ( dom o) = [:D, D:] & (o . ((y `1 ),(y `2 ))) = (o . ((y `2 ),(y `1 ))) by A1, FUNCT_2:def 1;

          x = (o . ((y `1 ),(y `2 ))) by A4, MCART_1: 21;

          hence thesis by A6, A5, FUNCT_1:def 6;

        end;

      end;

      hence (o .: [:X, Y:]) c= (o .: [:Y, X:]) & (o .: [:Y, X:]) c= (o .: [:X, Y:]);

    end;

    theorem :: MONOID_1:48



     Th48: o is associative implies (o .: [:(o .: [:X, Y:]), Z:]) = (o .: [:X, (o .: [:Y, Z:]):])

    proof



       A1: ( dom o) = [:D, D:] by FUNCT_2:def 1;

      assume

       A2: (o . ((o . (a,b)),c)) = (o . (a,(o . (b,c))));

      thus (o .: [:(o .: [:X, Y:]), Z:]) c= (o .: [:X, (o .: [:Y, Z:]):])

      proof

        let x be object;

        assume x in (o .: [:(o .: [:X, Y:]), Z:]);

        then

        consider y be object such that

         A3: y in ( dom o) and

         A4: y in [:(o .: [:X, Y:]), Z:] and

         A5: x = (o . y) by FUNCT_1:def 6;

        reconsider y as Element of [:D, D:] by A3;



         A6: y = [(y `1 ), (y `2 )] by MCART_1: 21;

        then

         A7: (y `2 ) in Z by A4, ZFMISC_1: 87;

        (y `1 ) in (o .: [:X, Y:]) by A4, A6, ZFMISC_1: 87;

        then

        consider z be object such that

         A8: z in ( dom o) and

         A9: z in [:X, Y:] and

         A10: (y `1 ) = (o . z) by FUNCT_1:def 6;

        reconsider z as Element of [:D, D:] by A8;



         A11: (y `1 ) = (o . ((z `1 ),(z `2 ))) by A10, MCART_1: 21;



         A12: z = [(z `1 ), (z `2 )] by MCART_1: 21;

        then (z `2 ) in Y by A9, ZFMISC_1: 87;

        then [(z `2 ), (y `2 )] in [:Y, Z:] by A7, ZFMISC_1: 87;

        then

         A13: (o . ((z `2 ),(y `2 ))) in (o .: [:Y, Z:]) by A1, FUNCT_1:def 6;

        (z `1 ) in X by A9, A12, ZFMISC_1: 87;

        then

         A14: [(z `1 ), (o . ((z `2 ),(y `2 )))] in [:X, (o .: [:Y, Z:]):] by A13, ZFMISC_1: 87;

        x = (o . ((y `1 ),(y `2 ))) by A5, MCART_1: 21;

        then x = (o . ((z `1 ),(o . ((z `2 ),(y `2 ))))) by A2, A11;

        hence thesis by A1, A14, FUNCT_1:def 6;

      end;

      let x be object;

      assume x in (o .: [:X, (o .: [:Y, Z:]):]);

      then

      consider y be object such that

       A15: y in ( dom o) and

       A16: y in [:X, (o .: [:Y, Z:]):] and

       A17: x = (o . y) by FUNCT_1:def 6;

      reconsider y as Element of [:D, D:] by A15;



       A18: y = [(y `1 ), (y `2 )] by MCART_1: 21;

      then

       A19: (y `1 ) in X by A16, ZFMISC_1: 87;

      (y `2 ) in (o .: [:Y, Z:]) by A16, A18, ZFMISC_1: 87;

      then

      consider z be object such that

       A20: z in ( dom o) and

       A21: z in [:Y, Z:] and

       A22: (y `2 ) = (o . z) by FUNCT_1:def 6;

      reconsider z as Element of [:D, D:] by A20;



       A23: (y `2 ) = (o . ((z `1 ),(z `2 ))) by A22, MCART_1: 21;



       A24: z = [(z `1 ), (z `2 )] by MCART_1: 21;

      then (z `1 ) in Y by A21, ZFMISC_1: 87;

      then [(y `1 ), (z `1 )] in [:X, Y:] by A19, ZFMISC_1: 87;

      then

       A25: (o . ((y `1 ),(z `1 ))) in (o .: [:X, Y:]) by A1, FUNCT_1:def 6;

      (z `2 ) in Z by A21, A24, ZFMISC_1: 87;

      then

       A26: [(o . ((y `1 ),(z `1 ))), (z `2 )] in [:(o .: [:X, Y:]), Z:] by A25, ZFMISC_1: 87;

      x = (o . ((y `1 ),(y `2 ))) by A17, MCART_1: 21;

      then x = (o . ((o . ((y `1 ),(z `1 ))),(z `2 ))) by A2, A23;

      hence thesis by A1, A26, FUNCT_1:def 6;

    end;

    theorem :: MONOID_1:49



     Th49: o is commutative implies (o .:^2 ) is commutative

    proof

      assume

       A1: o is commutative;

      let x,y be Subset of D;



      thus ((o .:^2 ) . (x,y)) = (o .: [:x, y:]) by Th44

      .= (o .: [:y, x:]) by A1, Th47

      .= ((o .:^2 ) . (y,x)) by Th44;

    end;

    theorem :: MONOID_1:50



     Th50: o is associative implies (o .:^2 ) is associative

    proof

      assume

       A1: o is associative;

      let x,y,z be Subset of D;



      thus ((o .:^2 ) . (((o .:^2 ) . (x,y)),z)) = ((o .:^2 ) . ((o .: [:x, y:]),z)) by Th44

      .= (o .: [:(o .: [:x, y:]), z:]) by Th44

      .= (o .: [:x, (o .: [:y, z:]):]) by A1, Th48

      .= ((o .:^2 ) . (x,(o .: [:y, z:]))) by Th44

      .= ((o .:^2 ) . (x,((o .:^2 ) . (y,z)))) by Th44;

    end;

    theorem :: MONOID_1:51



     Th51: a is_a_unity_wrt o implies (o .: [: {a}, X:]) = (D /\ X) & (o .: [:X, {a}:]) = (D /\ X)

    proof

      assume

       A1: a is_a_unity_wrt o;

      thus (o .: [: {a}, X:]) c= (D /\ X)

      proof

        let x be object;

        assume x in (o .: [: {a}, X:]);

        then

        consider y be object such that

         A2: y in ( dom o) and

         A3: y in [: {a}, X:] and

         A4: x = (o . y) by FUNCT_1:def 6;

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



         A5: x = (o . ((y `1 ),(y `2 ))) by A4, MCART_1: 21;



         A6: y = [(y `1 ), (y `2 )] by MCART_1: 21;

        then (y `1 ) in {a} by A3, ZFMISC_1: 87;

        then

         A7: (y `1 ) = a by TARSKI:def 1;



         A8: (o . (a,(y `2 ))) = (y `2 ) by A1, BINOP_1: 3;

        (y `2 ) in X by A3, A6, ZFMISC_1: 87;

        hence thesis by A5, A8, A7, XBOOLE_0:def 4;

      end;



       A9: ( dom o) = [:D, D:] by FUNCT_2:def 1;

      thus (D /\ X) c= (o .: [: {a}, X:])

      proof

        let x be object;



         A10: a in {a} by TARSKI:def 1;

        assume

         A11: x in (D /\ X);

        then

        reconsider d = x as Element of D by XBOOLE_0:def 4;



         A12: x = (o . (a,d)) by A1, BINOP_1: 3

        .= (o . [a, x]);

        x in X by A11, XBOOLE_0:def 4;

        then [a, d] in [: {a}, X:] by A10, ZFMISC_1: 87;

        hence thesis by A9, A12, FUNCT_1:def 6;

      end;

      thus (o .: [:X, {a}:]) c= (D /\ X)

      proof

        let x be object;

        assume x in (o .: [:X, {a}:]);

        then

        consider y be object such that

         A13: y in ( dom o) and

         A14: y in [:X, {a}:] and

         A15: x = (o . y) by FUNCT_1:def 6;

        reconsider y as Element of [:D, D:] by A13;



         A16: x = (o . ((y `1 ),(y `2 ))) by A15, MCART_1: 21;



         A17: y = [(y `1 ), (y `2 )] by MCART_1: 21;

        then (y `2 ) in {a} by A14, ZFMISC_1: 87;

        then

         A18: (y `2 ) = a by TARSKI:def 1;



         A19: (o . ((y `1 ),a)) = (y `1 ) by A1, BINOP_1: 3;

        (y `1 ) in X by A14, A17, ZFMISC_1: 87;

        hence thesis by A16, A19, A18, XBOOLE_0:def 4;

      end;

      thus (D /\ X) c= (o .: [:X, {a}:])

      proof

        let x be object;



         A20: a in {a} by TARSKI:def 1;

        assume

         A21: x in (D /\ X);

        then

        reconsider d = x as Element of D by XBOOLE_0:def 4;



         A22: x = (o . (d,a)) by A1, BINOP_1: 3

        .= (o . [x, a]);

        x in X by A21, XBOOLE_0:def 4;

        then [d, a] in [:X, {a}:] by A20, ZFMISC_1: 87;

        hence thesis by A9, A22, FUNCT_1:def 6;

      end;

    end;

    theorem :: MONOID_1:52



     Th52: a is_a_unity_wrt o implies {a} is_a_unity_wrt (o .:^2 ) & (o .:^2 ) is having_a_unity & ( the_unity_wrt (o .:^2 )) = {a}

    proof

      assume

       A1: a is_a_unity_wrt o;

      now

        let x be Subset of D;



        thus ((o .:^2 ) . ( {a},x)) = (o .: [: {a}, x:]) by Th44

        .= (D /\ x) by A1, Th51

        .= x by XBOOLE_1: 28;



        thus ((o .:^2 ) . (x, {a})) = (o .: [:x, {a}:]) by Th44

        .= (D /\ x) by A1, Th51

        .= x by XBOOLE_1: 28;

      end;

      hence

       A2: {a} is_a_unity_wrt (o .:^2 ) by BINOP_1: 3;

      hence ex A be Subset of D st A is_a_unity_wrt (o .:^2 );

      thus thesis by A2, BINOP_1:def 8;

    end;

    theorem :: MONOID_1:53



     Th53: o is having_a_unity implies (o .:^2 ) is having_a_unity & {( the_unity_wrt o)} is_a_unity_wrt (o .:^2 ) & ( the_unity_wrt (o .:^2 )) = {( the_unity_wrt o)}

    proof

      given a such that

       A1: a is_a_unity_wrt o;

      a = ( the_unity_wrt o) by A1, BINOP_1:def 8;

      hence thesis by A1, Th52;

    end;

    theorem :: MONOID_1:54



     Th54: o is uniquely-decomposable implies (o .:^2 ) is uniquely-decomposable

    proof

      assume that

       A1: o is having_a_unity and

       A2: (o . (a,b)) = ( the_unity_wrt o) implies a = b & b = ( the_unity_wrt o);

      thus (o .:^2 ) is having_a_unity by A1, Th53;

      let A,B be Subset of D such that

       A3: ((o .:^2 ) . (A,B)) = ( the_unity_wrt (o .:^2 ));

      set a = ( the_unity_wrt o);



       A4: ( the_unity_wrt (o .:^2 )) = {a} by A1, Th53;

      set a1 = the Element of A, a2 = the Element of B;

      (o .: [:A, B:]) = ((o .:^2 ) . (A,B)) by Th44;

      then ( dom o) meets [:A, B:] by A3, A4, RELAT_1: 118;

      then (( dom o) /\ [:A, B:]) <> {} ;

      then

       A5: [:A, B:] <> {} ;

      then

       A6: A <> {} by ZFMISC_1: 90;



       A7: B <> {} by A5, ZFMISC_1: 90;

      then

      reconsider a1, a2 as Element of D by A6, TARSKI:def 3;



       A8: {a1} c= A by A6, ZFMISC_1: 31;

      (o . (a1,a2)) in {a} by A3, A4, A6, A7, Th45;

      then

       A9: (o . (a1,a2)) = a by TARSKI:def 1;

      then

       A10: a2 = a by A2;



       A11: A c= {a}

      proof

        let x be object;

        assume

         A12: x in A;

        then

        reconsider c = x as Element of D;

        (o . (c,a2)) in {a} by A3, A4, A7, A12, Th45;

        then (o . (c,a2)) = a by TARSKI:def 1;

        then c = a2 by A2;

        hence thesis by A10, TARSKI:def 1;

      end;



       A13: B c= {a}

      proof

        let x be object;

        assume

         A14: x in B;

        then

        reconsider c = x as Element of D;

        (o . (a1,c)) in {a} by A3, A4, A6, A14, Th45;

        then (o . (a1,c)) = a by TARSKI:def 1;

        then c = a by A2;

        hence thesis by TARSKI:def 1;

      end;



       A15: a1 = a2 by A2, A9;

       {a2} c= B by A7, ZFMISC_1: 31;

      then B = {a} by A10, A13;

      hence thesis by A1, A15, A10, A8, A11, Th53;

    end;

    definition

      let G be non empty multMagma;

      :: MONOID_1:def9

      func bool G -> multMagma equals

      : Def9: multLoopStr (# ( bool the carrier of G), (the multF of G .:^2 ), {( the_unity_wrt the multF of G)} #) if G is unital

      otherwise multMagma (# ( bool the carrier of G), (the multF of G .:^2 ) #);

      correctness ;

    end

    registration

      let G be non empty multMagma;

      cluster ( bool G) -> non empty;

      coherence

      proof

        per cases ;

          suppose G is unital;

          then ( bool G) = multLoopStr (# ( bool the carrier of G), (the multF of G .:^2 ), {( the_unity_wrt the multF of G)} #) by Def9;

          hence the carrier of ( bool G) is non empty;

        end;

          suppose not G is unital;

          then ( bool G) = multMagma (# ( bool the carrier of G), (the multF of G .:^2 ) #) by Def9;

          hence the carrier of ( bool G) is non empty;

        end;

      end;

    end

    definition

      let G be unital non empty multMagma;

      :: original: bool

      redefine

      func bool G -> well-unital strict non empty multLoopStr ;

      coherence

      proof

        set M = multLoopStr (# ( bool carr(G)), ( op(G) .:^2 ), {( the_unity_wrt op(G))} #);

         op(G) is having_a_unity by MONOID_0:def 10;

        then

         A1: {( the_unity_wrt op(G))} is_a_unity_wrt ( op(G) .:^2 ) by Th53;

        ( 1. M) = {( the_unity_wrt op(G))} & ( bool G) = M by Def9;

        hence thesis by A1, MONOID_0:def 21;

      end;

    end

    theorem :: MONOID_1:55



     Th55: the carrier of ( bool G) = ( bool the carrier of G) & the multF of ( bool G) = (the multF of G .:^2 )

    proof

      ( bool G) = multLoopStr (# ( bool carr(G)), ( op(G) .:^2 ), {( the_unity_wrt op(G))} #) or ( bool G) = multMagma (# ( bool the carrier of G), ( op(G) .:^2 ) #) by Def9;

      hence thesis;

    end;

    theorem :: MONOID_1:56

    for G be unital non empty multMagma holds ( 1. ( bool G)) = {( the_unity_wrt the multF of G)}

    proof

      let G be unital non empty multMagma;

      ( bool G) = multLoopStr (# ( bool carr(G)), ( op(G) .:^2 ), {( the_unity_wrt op(G))} #) by Def9;

      hence thesis;

    end;

    theorem :: MONOID_1:57

    for G be non empty multMagma holds (G is commutative implies ( bool G) is commutative) & (G is associative implies ( bool G) is associative) & (G is uniquely-decomposable implies ( bool G) is uniquely-decomposable)

    proof

      let G be non empty multMagma;



       A1: op(bool) = ( op(G) .:^2 ) & carr(bool) = ( bool carr(G)) by Th55;

      thus G is commutative implies ( bool G) is commutative by A1, Th49;

      thus G is associative implies ( bool G) is associative by A1, Th50;

      assume op(G) is uniquely-decomposable;

      hence op(bool) is uniquely-decomposable by A1, Th54;

    end;