The Mizar article:

Monoid of Multisets and Subsets

by
Grzegorz Bancerek

Received December 29, 1992

Copyright (c) 1992 Association of Mizar Users

MML identifier: MONOID_1
[ MML identifier index ]


environ

 vocabulary VECTSP_1, FUNCT_1, FINSEQ_4, RELAT_1, FUNCT_2, PARTFUN1, FINSEQ_2,
      FINSEQ_1, CAT_1, FUNCOP_1, BOOLE, BINOP_1, SETWISEO, ALGSTR_1, MONOID_0,
      LATTICE2, MCART_1, GROUP_1, VECTSP_2, FUNCT_3, FINSET_1, COMPLEX1,
      CARD_1, ARYTM_1, MONOID_1;
 notation TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, NUMBERS, REAL_1, NAT_1,
      RELAT_1, STRUCT_0, FUNCT_1, FINSEQ_1, MONOID_0, FUNCT_2, BINOP_1,
      FUNCOP_1, SETWISEO, FINSET_1, FRAENKEL, FUNCT_3, FINSEQ_2, CARD_1,
      LATTICE2, FUNCT_4, FUNCT_6, VECTSP_1, DOMAIN_1;
 constructors REAL_1, NAT_1, BINOP_1, FUNCOP_1, SETWISEO, FRAENKEL, FUNCT_3,
      LATTICE2, FUNCT_6, MONOID_0, DOMAIN_1, MEMBERED, XBOOLE_0;
 clusters SUBSET_1, FUNCT_1, FINSET_1, MONOID_0, RELAT_1, PRELAMB, STRUCT_0,
      RELSET_1, FINSEQ_1, FUNCOP_1, NAT_1, MEMBERED, ZFMISC_1, XBOOLE_0,
      ORDINAL2;
 requirements NUMERALS, BOOLE, SUBSET, ARITHM;
 definitions TARSKI, BINOP_1, LATTICE2, SETWISEO, MONOID_0, STRUCT_0, XBOOLE_0;
 theorems TARSKI, NAT_1, FINSET_1, FINSEQ_1, BINOP_1, SETWISEO, MCART_1,
      FUNCOP_1, ZFMISC_1, FUNCT_1, FUNCT_2, FUNCT_3, CARD_1, CARD_2, FINSEQ_2,
      FINSEQ_3, FUNCT_5, FUNCT_6, BORSUK_1, MONOID_0, VECTSP_1, GRFUNC_1,
      RELAT_1, RELSET_1, XBOOLE_0, XBOOLE_1, XCMPLX_1;
 schemes NAT_1, FUNCT_2, MONOID_0, PARTFUN1, COMPTS_1;

begin :: Updating

 reserve x,y,z, X,Y,Z for set, n for Nat;

 deffunc op(HGrStr) = the mult of $1;
 deffunc un(multLoopStr) = the unity of $1;

definition let D1,D2,D be non empty set;
 mode Function of D1,D2,D is Function of [:D1,D2:],D;
end;

definition let f be Function, x1,x2,y be set;
 func f..(x1,x2,y) equals:
Def1:
   f..([x1,x2],y);
  correctness;
end;

theorem Th1:
 for f,g being Function, x1,x2,x being set st
  [x1,x2] in dom f & g = f.(x1,x2) & x in dom g holds f..(x1,x2,x) = g.x
  proof let f,g be Function, x1,x2,x be set;
      f..(x1,x2,x) = f..([x1,x2],x) & f.(x1,x2) = f.[x1,x2]
     by Def1,BINOP_1:def 1;
   hence thesis by FUNCT_6:44;
  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;
 redefine func f..(x1,x2,x) -> Element of D;
  coherence
   proof reconsider g = f.(x1,x2) as Element of Funcs(A,D);
       dom f = [:D1,D2:] & dom g = A & [x1,x2] in
 [:D1,D2:] by FUNCT_2:def 1;
     then f..(x1,x2,x) = g.x by Th1;
    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;
 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,
RELSET_1:12;
    hence thesis by FUNCT_2:def 2;
   end;
end;

definition let A be non empty set;
 let n be Nat, x be Element of A;
 redefine func n |-> x -> FinSequence of A;
  coherence by FINSEQ_2:77;
 synonym n .--> x;
end;

definition let D be non empty set, A be set, d be Element of D;
 redefine func A --> d -> Element of Funcs(A,D);
  coherence
   proof
A1:   dom (A --> d) = A & rng (A --> d) c= {d} & {d} c= D
      by FUNCOP_1:19;
     then rng (A --> d) c= D by XBOOLE_1:1;
    hence thesis by A1,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;
 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,RELSET_1:
12;
    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;
 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,RELSET_1:
12;
    hence thesis by FUNCT_2:def 2;
   end;
end;

theorem
   for f,g being Function, X being 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 FUNCT_1:68;
A2:  dom ((f|X)*g) = dom (f*(X|g))
     proof
      thus dom ((f|X)*g) c= dom (f*(X|g))
        proof let x; assume x in dom ((f|X)*g);
then A3:        x in dom g & g.x in dom (f|X) by FUNCT_1:21;
then A4:       g.x in X & g.x in dom f by A1,XBOOLE_0:def 3;
then A5:       x in dom (X|g) by A3,FUNCT_1:85;
          then g.x = (X|g).x by FUNCT_1:85;
         hence thesis by A4,A5,FUNCT_1:21;
        end;
      let x; assume x in dom (f*(X|g));
       then x in dom (X|g) & (X|g).x in dom f by FUNCT_1:21;
then A6:     x in dom g & g.x in X & g.x in dom f by FUNCT_1:85;
       then g.x in dom (f|X) by A1,XBOOLE_0:def 3;
      hence thesis by A6,FUNCT_1:21;
     end;
      now let x; assume x in dom ((f|X)*g);
      then ((f|X)*g).x = (f|X).(g.x) & g.x in dom (f|X) &
      (f*(X|g)).x = f.((X|g).x) & x in dom (X|g) by A2,FUNCT_1:21,22;
      then ((f|X)*g).x = f.(g.x) & (f*(X|g)).x = f.(g.x) by FUNCT_1:70,85;
     hence ((f|X)*g).x = (f*(X|g)).x;
    end;
   hence thesis by A2,FUNCT_1:9;
  end;

scheme NonUniqFuncDEx
  { X() -> set, Y() -> non empty set, P[set,set] }:
 ex f being Function of X(), Y() st for x st x in X() holds P[x,f.x]
  provided
A1:  for x st x in X() ex y being Element of Y() st P[x,y]
  proof
   defpred Q[set,set] means P[$1,$2];
A2:  for x st x in X() ex y st y in Y() & Q[x,y]
     proof let x; assume x in X();
      then consider y being Element of Y() such that
A3:    P[x,y] by A1;
      take y; thus thesis by A3;
     end;
   consider f being Function such that
A4:  dom f = X() & rng f c= Y() & for x st x in X() holds Q[x,f.x]
     from NonUniqBoundFuncEx(A2);
   reconsider f as Function of X(), Y() by A4,FUNCT_2:def 1,RELSET_1:11;
   take f; thus thesis by A4;
  end;

begin :: Monoid of functions into a semigroup

definition let D1,D2,D be non empty set;
 let f be Function of D1,D2,D;
 let A be set;
 func (f,D).:A -> Function of Funcs(A,D1), Funcs(A,D2), Funcs(A,D) means:
Def2:
  for f1 being Element of Funcs(A,D1) for f2 being 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 being Function of Funcs(A,D1), Funcs(A,D2), Funcs(A,D)
    such that
A1:   for f1 being Element of Funcs(A,D1)
     for f2 being Element of Funcs(A,D2) holds
      b.[f1,f2] = G(f1,f2) from Lambda2D;
    take b; let f1 be Element of Funcs(A,D1), f2 be Element of Funcs(A,D2);
    thus b.(f1,f2) = b.[f1,f2] by BINOP_1:def 1 .= f.:(f1,f2) 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 being Element of Funcs(A,D1) for f2 being Element of Funcs(A,D2)
      holds o1.(f1,f2) = f.:(f1,f2) and
A3:  for f1 being Element of Funcs(A,D1) for f2 being 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 by BINOP_1:2;
   end;
end;

theorem
   for D1,D2,D being non empty set for f being Function of D1,D2,D
  for A being set, f1 being (Function of A,D1), f2 being Function of A,D2
   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;
   let x such that
A1:  x in A;
A2:  dom f1 = A & rng f1 c= D1 & dom f2 = A & rng f2 c= D2
    by FUNCT_2:def 1,RELSET_1:12;
   then reconsider f1 as Element of Funcs(A,D1) by FUNCT_2:def 2;
   reconsider f2 as Element of Funcs(A,D2) by A2,FUNCT_2:def 2;
A3:  ((f,D).:A).(f1,f2) = f.:(f1,f2) & dom (f.:
(f1,f2)) = A & [f1,f2] = [f1,f2] &
    dom ((f,D).:A) = [:Funcs(A,D1), Funcs(A,D2):] by Def2,FUNCT_2:def 1;
    then (f.:(f1,f2)).x = f.(f1.x,f2.x) by A1,FUNCOP_1:28;
   hence thesis by A1,A3,Th1;
  end;

reserve A for set, D for non empty set, a,b,c,l,r for Element of D,
 o,o' for BinOp of D, f,g,h for Function of A,D;

theorem Th4:
 o is commutative implies o.:(f,g) = o.:(g,f)
  proof assume
A1:  o.(a,b) = o.(b,a);
A2:  dom (o.:(f,g)) = A & dom (o.:(g,f)) = A &
    dom f = A & rng f c= D & dom g = A & rng g c= D by FUNCT_2:def 1,RELSET_1:
12;
      now let x; assume
A3:    x in A; then f.x in rng f & g.x in rng g by A2,FUNCT_1:def 5;
     then reconsider a = f.x, b = g.x as Element of D by A2;
     thus (o.:(f,g)).x = o.(a,b) by A2,A3,FUNCOP_1:28 .= o.(b,a) by A1
        .= (o.:(g,f)).x by A2,A3,FUNCOP_1:28;
    end;
   hence thesis by A2,FUNCT_1:9;
  end;

theorem Th5:
 o is associative implies o.:(o.:(f,g),h) = o.:(f,o.:(g,h))
  proof assume
A1:  o.(o.(a,b),c) = o.(a,o.(b,c));
A2:  dom (o.:(f,g)) = A & dom (o.:(g,h)) = A &
    dom (o.:(o.:(f,g),h)) = A & dom (o.:(f,o.:(g,h))) = A &
    dom f = A & rng f c= D & dom g = A & rng g c= D &
    dom h = A & rng h c= D by FUNCT_2:def 1,RELSET_1:12;
      now let x; assume
A3:    x in A;
      then f.x in rng f & g.x in rng g & h.x in rng h by A2,FUNCT_1:def 5;
     then reconsider a = f.x, b = g.x, c = h.x as Element of D by A2;
     thus (o.:(o.:(f,g),h)).x = o.((o.:(f,g)).x,c) by A2,A3,FUNCOP_1:28
        .= o.(o.(a,b),c) by A2,A3,FUNCOP_1:28
        .= o.(a,o.(b,c)) by A1
        .= o.(a,(o.:(g,h)).x) by A2,A3,FUNCOP_1:28
        .= (o.:(f,o.:(g,h))).x by A2,A3,FUNCOP_1:28;
    end;
   hence thesis by A2,FUNCT_1:9;
  end;

theorem Th6:
 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 (o[;](a,f)) = A & dom (o[:](f,a)) = A & dom f = A & rng f c= D
     by FUNCT_2:def 1,RELSET_1:12;
      now let x; assume
A3:    x in A; then f.x in rng f by A2,FUNCT_1:def 5;
     then reconsider b = f.x as Element of D by A2;
     thus (o[;](a,f)).x = o.(a,b) by A2,A3,FUNCOP_1:42 .= f.x by A1,BINOP_1:11
;
    end;
   hence o[;](a,f) = f by A2,FUNCT_1:9;
      now let x; assume
A4:    x in A; then f.x in rng f by A2,FUNCT_1:def 5;
     then reconsider b = f.x as Element of D by A2;
     thus (o[:](f,a)).x = o.(b,a) by A2,A4,FUNCOP_1:35 .= f.x by A1,BINOP_1:11
;
    end;
   hence o[:](f,a) = f by A2,FUNCT_1:9;
  end;

theorem Th7:
 o is idempotent implies o.:(f,f) = f
  proof assume
A1:  o.(a,a) = a;
A2:  dom f = A & dom (o.:(f,f)) = A by FUNCT_2:def 1;
      now let x; assume
A3:    x in A; then reconsider a = f.x as Element of D by FUNCT_2:7;
     thus o.:(f,f).x = o.(a,a) by A2,A3,FUNCOP_1:28 .= f.x by A1;
    end;
   hence thesis by A2,FUNCT_1:9;
  end;

theorem Th8:
 o is commutative implies (o,D).:A is commutative
  proof assume
A1:  o is commutative;
   let f,g be Element of Funcs(A,D);
   set h = (o,D).:A;
   thus h.(f,g) = o.:(f, g) by Def2 .= o.:(g, f) by A1,Th4 .= h.(g,f) by Def2;
  end;

theorem Th9:
 o is associative implies (o,D).:A is associative
  proof assume
A1:  o is associative;
   let f,g,h be Element of Funcs(A,D);
   set F = (o,D).:A;
   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,Th5
      .= F.(f,o.:(g,h)) by Def2
      .= F.(f,F.(g,h)) by Def2;
  end;

theorem Th10:
 a is_a_unity_wrt o implies A --> a is_a_unity_wrt (o,D).:A
  proof assume
A1:  a is_a_unity_wrt o;
   set e = A --> a; set F = (o,D).:A;
      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:41
                 .= f by A1,Th6;
     thus F.(f,e) = o.:(f,e) by Def2 .= o[:](f,a) by A2,FUNCOP_1:34
                 .= f by A1,Th6;
    end;
   hence thesis by BINOP_1:11;
  end;

theorem Th11:
 o has_a_unity implies the_unity_wrt (o,D).:A = A --> the_unity_wrt o &
   (o,D).:A has_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,Th10,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,Th10;
  end;

theorem Th12:
 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,Th7;
  end;

theorem Th13:
 o is invertible implies (o,D).:A is invertible
  proof assume
A1:  for a,b ex r,l st o.(a,r) = b & o.(l,a) = b;
   let f,g be Element of Funcs(A,D);
   defpred P[set,set] means o.(f.$1,$2) = g.$1;
A2:  for x st x in A ex c st P[x,c]
     proof let x; assume
         x in A; then reconsider a = f.x, b = g.x as Element of D by FUNCT_2:7
;
      consider r,l such that
A3:    o.(a,r) = b & o.(l,a) = b by A1;
      take r; thus thesis by A3;
     end;
   defpred Q[set,set] means o.($2,f.$1) = g.$1;
A4:  for x st x in A ex c st Q[x,c]
     proof let x; assume
         x in A; then reconsider a = f.x, b = g.x as Element of D by FUNCT_2:7;
      consider r,l such that
A5:    o.(a,r) = b & o.(l,a) = b by A1;
      take l; thus thesis by A5;
     end;
   consider h1 being Function of A,D such that
A6:  for x st x in A holds P[x,h1.x] from NonUniqFuncDEx(A2);
   consider h2 being Function of A,D such that
A7:  for x st x in A holds Q[x,h2.x] from NonUniqFuncDEx(A4);
      dom h1 = A & dom h2 = A & rng h1 c= D & rng h2 c= D by FUNCT_2:def 1,
RELSET_1:12;
   then reconsider h1, h2 as Element of Funcs(A,D) by FUNCT_2:def 2;
   take h1, h2;
A8:  dom (o.:(f,h1)) = A & dom (o.:(h2,f)) = A & dom g = A &
    o.:(f,h1) = ((o,D).:A).(f,h1) & o.:(h2,f) = ((o,D).:A).(h2,f)
     by Def2,FUNCT_2:def 1;
      now let x; assume
A9:    x in A;
     hence o.:(f,h1).x = o.(f.x,h1.x) by A8,FUNCOP_1:28 .= g.x by A6,A9;
    end;
   hence ((o,D).:A).(f,h1) = g by A8,FUNCT_1:9;
      now let x; assume
A10:    x in A;
     hence o.:(h2,f).x = o.(h2.x,f.x) by A8,FUNCOP_1:28 .= g.x by A7,A10;
    end;
   hence ((o,D).:A).(h2,f) = g by A8,FUNCT_1:9;
  end;

theorem Th14:
 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:  (o,D).:A.(f,g) = o.:(f,g) & (o,D).:A.(g,f) = o.:(g,f) &
    (o,D).:A.(f,h) = o.:(f,h) & (o,D).:A.(h,f) = o.:(h,f) by Def2;
A4:  A = dom (o.:(f,g)) & A = dom (o.:(g,f)) & A = dom (o.:(f,h)) &
    A = dom (o.:(h,f)) & dom g = A & dom h = A by FUNCT_2:def 1;
      now let x; assume
A5:    x in A;
     then reconsider a = f.x, b = g.x, c = h.x as Element of D by FUNCT_2:7;
        o.:(f,g).x = o.(a,b) & o.:(f,h).x = o.(a,c) & o.:(g,f).x = o.(b,a) &
      o.:(h,f).x = o.(c,a) by A4,A5,FUNCOP_1:28;
     hence g.x = h.x by A1,A2,A3;
    end;
   hence thesis by A4,FUNCT_1:9;
  end;

theorem Th15:
 o is uniquely-decomposable implies (o,D).:A is uniquely-decomposable
  proof assume
A1:  o has_a_unity & for a,b st o.(a,b) = the_unity_wrt o holds
     a = b & b = the_unity_wrt o;
   hence (o,D).:A has_a_unity by Th11;
   let f,g be Element of Funcs(A,D) such that
A2:  (o,D).:A.(f,g) = the_unity_wrt (o,D).:A;
A3:  (o,D).:A.(f,g) = o.:(f,g) & the_unity_wrt (o,D).:A = A --> the_unity_wrt o
     by A1,Def2,Th11;
A4:  dom (A --> the_unity_wrt o) = A & dom f = A & dom g = A &
    dom (o.:(f,g)) = A by FUNCT_2:def 1;
      now let x; assume
A5:    x in A; then reconsider a = f.x, b = g.x as Element of D by FUNCT_2:7
;
        (o.:(f,g)).x = o.(a,b) & (A --> the_unity_wrt o).x = the_unity_wrt o
       by A4,A5,FUNCOP_1:13,28;
     hence f.x = g.x by A1,A2,A3;
    end;
   hence f = g by A4,FUNCT_1:9;
      now let x; assume
A6:    x in A; then reconsider a = f.x, b = g.x as Element of D by FUNCT_2:7
;
        (o.:(f,g)).x = o.(a,b) & (A --> the_unity_wrt o).x = the_unity_wrt o
       by A4,A6,FUNCOP_1:13,28;
     hence g.x = (A --> the_unity_wrt o).x by A1,A2,A3;
    end;
   hence thesis by A3,A4,FUNCT_1:9;
  end;

theorem
   o absorbs o' implies (o,D).:A absorbs (o',D).:A
  proof assume
A1:  o.(a,o'.(a,b)) = a;
   let f,g be Element of Funcs(A,D);
A2:  ((o',D).:A).(f,g) = o'.:(f,g) & ((o,D).:A).(f,o'.:(f,g)) = o.:(f,o'.:
(f,g))
     by Def2;
A3:  dom f = A & dom g = A & dom (o'.:(f,g)) = A & dom (o.:(f,o'.:(f,g))) = A
     by FUNCT_2:def 1;
      now let x; assume
A4:    x in A;
     then reconsider a = f.x, b = g.x as Element of D by FUNCT_2:7;
        (o.:(f,o'.:(f,g))).x = o.(a,(o'.:(f,g)).x) & (o'.:(f,g)).x = o'.(a,b)
       by A3,A4,FUNCOP_1:28;
     hence f.x = (o.:(f,o'.:(f,g))).x by A1;
    end;
   hence thesis by A2,A3,FUNCT_1:9;
  end;

theorem Th17:
 for D1, D2, D, E1, E2, E being non empty set, o1 being Function of D1, D2, D,
   o2 being Function of E1, E2, E st o1 <= o2 holds (o1,D).:A <= (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;
   assume A1: o1 <= o2;
then A2:  dom o1 c= dom o2 & dom o1 = [:D1,D2:] & dom o2 = [:E1,E2:] &
    dom (o1,D).:A = [:Funcs(A,D1),Funcs(A,D2):] &
    dom (o2,E).:A = [:Funcs(A,E1),Funcs(A,E2):] &
    for x st x in dom o1 holds o1.x = o2.x by FUNCT_2:def 1,GRFUNC_1:8;
    then D1 c= E1 & D2 c= E2 by BORSUK_1:7;
then A3:  Funcs(A,D1) c= Funcs(A,E1) & Funcs(A,D2) c= Funcs(A,E2) by FUNCT_5:63
;
then A4:  dom (o1,D).:A c= dom (o2,E).:A by A2,ZFMISC_1:119;
      now let x; assume x in dom (o1,D).:A;
     then reconsider y = x as Element of [:Funcs(A,D1),Funcs(A,D2):] by FUNCT_2
:def 1;
     reconsider f1 = y`1 as Element of Funcs(A,D1);
     reconsider g1 = y`1 as Element of Funcs(A,E1) by A3,TARSKI:def 3;
     reconsider f2 = y`2 as Element of Funcs(A,D2);
     reconsider g2 = y`2 as Element of Funcs(A,E2) by A3,TARSKI:def 3;
A5:    ((o1,D).:A).(f1,f2) = o1.:(f1,f2) & ((o2,E).:A).(g1,g2) = o2.:(g1,g2) &
      rng f1 c= D1 & rng f2 c= D2 & dom f1 = A & dom f2 = A &
      dom (o2.:(g1,g2)) = A & dom (o1.:(f1,f2)) = A by Def2,FUNCT_2:def 1,
RELSET_1:12;
        now let z be set; assume z in A;
then A6:      (o2.:(g1,g2)).z = o2.(g1.z,g2.z) & (o1.:(f1,f2)).z = o1.(f1.z,f2.
z) &
        o1.(f1.z,f2.z) = o1.[f1.z,f2.z] & o2.(f1.z,f2.z) = o2.[f1.z,f2.z] &
        f1.z in rng f1 & f2.z in rng f2
         by A5,BINOP_1:def 1,FUNCOP_1:28,FUNCT_1:def 5;
        then [f1.z,f2.z] in dom o1 by A2,A5,ZFMISC_1:106;
       hence (o2.:(g1,g2)).z = (o1.:(f1,f2)).z by A1,A6,GRFUNC_1:8;
      end;
      then ((o1,D).:A).(f1,f2) = ((o1,D).:A).[f1,f2] & [f1,f2] = x &
      ((o2,E).:A).(g1,g2) = ((o2,E).:A).[g1,g2] &
      o2.:(g1,g2) = o1.:(f1,f2) by A5,BINOP_1:def 1,FUNCT_1:9,MCART_1:23;
     hence ((o1,D).:A).x = ((o2,E).:A).x by A5;
    end;
   hence thesis by A4,GRFUNC_1:8;
  end;

definition let G be non empty HGrStr; let A be set;
 func .:(G,A) -> HGrStr equals:
Def3:
   multLoopStr (# Funcs(A, the carrier of G),
   (the mult of G,the carrier of G).:A,
   (A --> the_unity_wrt the mult of G)#) if G is unital otherwise
   HGrStr (# Funcs(A, the carrier of G),
   (the mult of G,the carrier of G).:A #);
  correctness;
end;

definition let G be non empty HGrStr; 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 mult of G,the carrier of G).:A,
   (A --> the_unity_wrt the mult of G)#) by Def3;
   hence the carrier of .:(G,A) is non empty;
   suppose G is not unital;
    then .:(G,A) = HGrStr (# Funcs(A, the carrier of G),
   (the mult of G,the carrier of G).:A #) by Def3;
   hence the carrier of .:(G,A) is non empty;
  end;
end;

reserve G for non empty HGrStr;

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

theorem Th18:
 the carrier of .:(G,X) = Funcs(X, the carrier of G) &
 the mult of .:(G,X) = (the mult of G, the carrier of G).:X
  proof
      (G is unital implies
      .:(G,X) = multLoopStr(#Funcs(X, carr(G)),
      (op(G),carr(G)).:X,
      (X --> the_unity_wrt op(G))#)) &
    (not G is unital implies
      .:(G,X) = HGrStr(#Funcs(X, carr(G)),
      (op(G),carr(G)).:X#)) &
    (G is unital or not G is unital) by Def3;
   hence thesis;
  end;

theorem
   x is Element of .:
(G,X) iff x is Function of X, the carrier of G
  proof
A1:  carr(.:(G,X)) = Funcs(X, carr(G)) by Th18;
      x is Element of .:(G,X)
    implies x is Element of Funcs(X, carr(G)) by Th18;
   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);
      dom f = X & rng f c= carr(G) by FUNCT_2:def 1,RELSET_1:12;
   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 Th18;
  hence thesis;
 end;

definition let G be non empty HGrStr, A be set;
 cluster .:(G,A) -> constituted-Functions;
  coherence by Lm1;
end;

theorem Th20:
 for f being 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 Th18; f = f;
   hence thesis by FUNCT_2:def 1,RELSET_1:12;
  end;

theorem Th21:
 for f,g being Element of .:(G,X) st
  for x 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 Th20;
   hence thesis by FUNCT_1:9;
  end;

definition let G be non empty HGrStr, A be non empty set;
 let f be Element of .:(G,A);
 cluster rng f -> non empty;
  coherence
   proof consider a being Element of A;
     rng f c= carr(G) & dom f = A by Th20; then f.a in rng f by FUNCT_1:def 5;
    hence thesis;
   end;
 let a be Element of A;
 redefine func f.a -> Element of G;
  coherence
   proof
A1:   rng f c= carr(G) & dom f = A by Th20; then f.a in rng f by FUNCT_1:def 5
;
    hence thesis by A1;
   end;
end;

theorem Th22:
 for f1,f2 being Element of .:(G,D), a being 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 Th18;
      op(.:(G,D)) = (op(G),carr(G)).:D & f1*f2 = op(.:(G,D)).(f1,f2)
     by Th18,VECTSP_1:def 10;
    then dom (op(G).:(g1,g2)) = D & f1*f2 = op(G).:(g1,g2) by Def2,FUNCT_2:def
1;
   hence (f1*f2).a = op(G).(f1.a,f2.a) by FUNCOP_1:28
                  .= (f1.a)*(f2.a) by VECTSP_1:def 10;
  end;

definition let G be unital (non empty HGrStr); let A be set;
 redefine func .:(G,A) -> well-unital constituted-Functions strict
  (non empty multLoopStr);
  coherence
   proof op(G) has_a_unity by MONOID_0:def 10;
    then consider a being Element of G such that
A1:   a is_a_unity_wrt op(G) by SETWISEO:def 2;
A2:   a = the_unity_wrt op(G) &
     .:(G,A) = multLoopStr(#Funcs(A, carr(G)),
     (op(G),carr(G)).:A,
     (A --> the_unity_wrt op(G))#) by A1,Def3,BINOP_1:def 8;
       A --> a is_a_unity_wrt (op(G),carr(G)).:A by A1,Th10;
    hence thesis by A2,MONOID_0:def 21;
   end;
end;

theorem Th23:
 for G being unital (non empty HGrStr) holds
   the unity of .:(G,X) = X --> the_unity_wrt the mult of G
  proof let G be unital (non empty HGrStr);
      .:(G,X) = multLoopStr(#Funcs(X, carr(G)), (op(G), carr(G)).:X,
    (X --> the_unity_wrt op(G))#) by Def3;
   hence thesis;
  end;

theorem Th24:
 for G being non empty HGrStr, A being 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(.:(G,A)) = (op(G), carr(G)).:A & carr(.:(G,A)) = Funcs(A, carr(G))
     by Th18;
   thus G is commutative implies .:(G,A) is commutative
     proof assume op(G) is commutative;
      hence op(.:(G,A)) is commutative by A1,Th8;
     end;
   thus G is associative implies .:(G,A) is associative
     proof assume op(G) is associative;
      hence op(.:(G,A)) is associative by A1,Th9;
     end;
   thus G is idempotent implies .:(G,A) is idempotent
     proof assume op(G) is idempotent;
      hence op(.:(G,A)) is idempotent by A1,Th12;
     end;
   thus G is invertible implies .:(G,A) is invertible
    proof assume op(G) is invertible;
     hence op(.:(G,A)) is invertible by A1,Th13;
    end;
   thus G is cancelable implies .:(G,A) is cancelable
     proof assume op(G) is cancelable;
      hence op(.:(G,A)) is cancelable by A1,Th14;
     end;
   assume op(G) is uniquely-decomposable;
   hence op(.:(G,A)) is uniquely-decomposable by A1,Th15;
  end;

theorem
   for H being non empty SubStr of G holds .:(H,X) is SubStr of .:(G,X)
  proof let H be non empty SubStr of G;
      op(H) <= op(G) & op(.:(G,X)) = (op(G), carr(G)).:X &
    op(.:(H,X)) = (op(H), carr(H)).:X by Th18,MONOID_0:def 23;
   hence op(.:(H,X)) <= op(.:(G,X)) by Th17;
  end;

theorem
   for G being unital (non empty HGrStr), H being non empty SubStr of G st
  the_unity_wrt the mult of G in the carrier of H holds
   .:(H,X) is MonoidalSubStr of .:(G,X)
  proof let G be unital (non empty HGrStr), H be non empty SubStr of G; assume
A1:  the_unity_wrt the mult of G in carr(H);
   then reconsider G' = G, H' = H as unital (non empty HGrStr) by MONOID_0:32;
A2:  op(H) <= op(G) & op(.:(G,X)) = (op(G), carr(G)).:X &
    the unity of .:(G',X) = X --> the_unity_wrt op(G) &
    the unity of .:(H',X) = X --> the_unity_wrt op(H) &
    the_unity_wrt op(H') = the_unity_wrt op(G') &
    op(.:(H,X)) = (op(H), carr(H)).:X
     by A1,Th18,Th23,MONOID_0:32,def 23;
    then op(.:(H,X)) <= op(.:(G,X)) by Th17;
   hence thesis by A2,MONOID_0:def 25;
  end;

definition
 let G be unital associative commutative
          cancelable uniquely-decomposable (non empty HGrStr);
 let A be set;
 redefine func .:(G,A) -> commutative cancelable uniquely-decomposable
                constituted-Functions strict Monoid;
  coherence
   proof
     .:(G,A) is commutative cancelable by Th24;
    hence thesis by Th24;
   end;
end;

begin :: Monoid of multisets over a set

definition let A be set;
 func MultiSet_over A -> commutative cancelable uniquely-decomposable
                         constituted-Functions strict Monoid equals:
Def4:
   .:(<NAT,+,0>, A);
  correctness;
end;

theorem Th27:
 the carrier of MultiSet_over X = Funcs(X,NAT) &
 the mult of MultiSet_over X = (addnat,NAT).:X &
 the unity of MultiSet_over X = X --> 0
  proof
      the HGrStr of <NAT,+,0> = <NAT,+> & MultiSet_over X = .:(<NAT,+,0>, X) &
    the_unity_wrt op(<NAT,+>) = 0 by Def4,MONOID_0:44,def 22;
   hence thesis by Th18,Th23,MONOID_0:52;
  end;

definition let A be set;
 mode Multiset of A is Element of MultiSet_over A;
end;

theorem Th28:
 x is Multiset of X iff x is Function of X,NAT
  proof A1:  x is Multiset of X iff x is Element of Funcs(X,NAT) by Th27;
      now let x be Function of X,NAT;
        dom x = X & rng x c= NAT by FUNCT_2:def 1,RELSET_1:12;
     hence x is Element of Funcs(X,NAT) by FUNCT_2:def 2;
    end;
   hence thesis by A1;
  end;

theorem Th29:
 for m being 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 Th28;
   hence thesis by FUNCT_2:def 1,RELSET_1:12;
  end;

definition let A be non empty set;
 let m be Multiset of A;
 redefine func rng m -> non empty Subset of NAT;
  coherence
   proof consider a being Element of A;
     A1: MultiSet_over A = .:(<NAT,+,0>, A) & carr(<NAT,+,0>) = NAT
      by Def4,MONOID_0:52;
then rng m c= NAT & dom m = A by Th20; then m.a in rng m by FUNCT_1:def 5;
    hence thesis by A1,Th20;
   end;
 let a be Element of A;

 func m.a -> Nat;
  coherence
   proof
       MultiSet_over A = .:(<NAT,+,0>, A) & carr(<NAT,+,0>) = NAT
      by Def4,MONOID_0:52;
then A2:   rng m c= NAT & dom m = A by Th20; then m.a in rng m by FUNCT_1:def 5
;
    hence thesis by A2;
   end;
end;

theorem Th30:
 for m1,m2 being Multiset of D, a being Element of D holds
   (m1 [*] m2).a = (m1.a)+(m2.a)
  proof let m1,m2 be Multiset of D, a be Element of D;
   reconsider N = <NAT,+,0> as non empty HGrStr;
   reconsider f1 = m1, f2 = m2 as Element of .:(N,D) by Def4;
   thus (m1 [*] m2).a = (f1 [*] f2).a by Def4 .= (f1.a)*(f2.a) by Th22
                   .= (m1.a)+(m2.a) by MONOID_0:51;
  end;

theorem Th31:
 chi(Y,X) is Multiset of X
  proof
A1:  dom chi(Y,X) = X & rng chi(Y,X) c= {0,1} &
    carr(MultiSet_over X) = Funcs(X,NAT) by Th27,FUNCT_3:48,def 3;
    then rng chi(Y,X) c= NAT by XBOOLE_1:1;
   hence thesis by A1,FUNCT_2:def 2;
  end;

definition let Y,X;
 redefine func chi(Y,X) -> Multiset of X;
  coherence by Th31;
end;

definition let X; let n be Nat;
 redefine func X --> n -> Multiset of X;
  coherence
   proof thus X --> n is Multiset of X by Th28; end;
end;

definition let A be non empty set, a be Element of A;
 func chi a -> Multiset of A equals:
Def5:
   chi({a},A);
  coherence;
end;

theorem Th32:
 for A being non empty set, a,b being 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;
      chi a = chi({a},A) & a in {a} & (b <> a implies not b in {a})
     by Def5,TARSKI:def 1;
   hence thesis by 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 Th33:
 (for a holds m1.a = m2.a) implies m1 = m2
  proof assume for a holds m1.a = m2.a;
    then (for x st x in A holds m1.x = m2.x) & MultiSet_over A = .:(<NAT,+,0>,
A)
     by Def4;
   hence thesis by Th21;
  end;

definition let A be set;
 func finite-MultiSet_over A ->
  strict non empty MonoidalSubStr of MultiSet_over A means:
Def6:
  for f being Multiset of A holds
   f in the carrier of it iff f"(NAT\{0}) is finite;
  existence
   proof
    defpred P[set] means ex f being Function of A,NAT
            st $1 = f & f"(NAT\{0}) is finite;
A1:   for a,b being Multiset of A holds P[a] & P[b] implies
      P[a [*] b]
      proof let a,b be Multiset of A;
       given f being Function of A,NAT such that
A2:     a = f & f"(NAT\{0}) is finite;
       given g being Function of A,NAT such that
A3:     b = g & g"(NAT\{0}) is finite;
       reconsider h = a [*] b as Function of A,NAT by Th28;
       take h;
A4:     (f"(NAT\{0})) \/ (g"(NAT\{0})) is finite by A2,A3,FINSET_1:14;
A5:     dom h = A & dom f = A & dom g = A & rng f c= NAT & rng g c= NAT
         by FUNCT_2:def 1,RELSET_1:12;
          h"(NAT\{0}) c= (f"(NAT\{0})) \/ (g"(NAT\{0}))
         proof let x; assume A6: x in h"(NAT\{0});
then A7:        x in A & h.x in NAT\{0} by FUNCT_1:def 13;
             f.x in rng f & g.x in rng g by A5,A6,FUNCT_1:def 5;
          then reconsider n = f.x, m = g.x as Nat by A5;
             h.x = n+m & not h.x in {0} by A2,A3,A7,Th30,XBOOLE_0:def 4;
           then n <> 0 or m <> 0 by 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 4;
           then x in f"(NAT\{0}) or x in g"(NAT\{0}) by A5,A6,FUNCT_1:def 13;
          hence thesis by XBOOLE_0:def 2;
         end;
       hence thesis by A4,FINSET_1:13;
      end;
    reconsider e = A --> 0 as Function of A,NAT by Th28;
A8:  dom e = A & rng e c= {0} & {0} c= NAT by FUNCOP_1:19;
A9:  now consider x being Element of e"(NAT\{0});
      assume e"(NAT\{0}) <> {};
       then x in A & e.x in NAT\{0} by A8,FUNCT_1:def 13;
       then e.x = 0 & not e.x in {0} by FUNCOP_1:13,XBOOLE_0:def 4;
      hence contradiction by TARSKI:def 1;
     end;
       e = un(MultiSet_over A) by Th27;
then A10: P[the unity of MultiSet_over A] by A9;
    consider M being strict non empty MonoidalSubStr of MultiSet_over A
    such that
A11:   for a being Multiset of A holds a in the carrier of M iff P[a]
       from MonoidalSubStrEx2(A1,A10);
    reconsider M as strict non empty MonoidalSubStr of MultiSet_over A;
    take M;
    let f be Multiset of A; reconsider g = f as Function of A,NAT by Th28;
    thus f in carr(M) implies f"(NAT\{0}) is finite
      proof assume f in carr(M);
        then ex g being Function of A,NAT st f = g & g"(NAT\{0}) is finite by
A11;
       hence thesis;
      end;
    assume f"(NAT\{0}) is finite;
     then g"(NAT\{0}) is finite;
    hence thesis by A11;
   end;
  uniqueness
   proof let M1,M2 be strict non empty MonoidalSubStr of MultiSet_over A
    such that
A12:  for f being Multiset of A holds
      f in carr(M1) iff f"(NAT\{0}) is finite and
A13:  for f being Multiset of A holds
      f in carr(M2) iff f"(NAT\{0}) is finite;
    set M = MultiSet_over A;
A14:  carr(M1) c= carr(M) & carr(M2) c= carr(M) & carr(M) = Funcs(A,NAT)
      by Th27,MONOID_0:25;
       carr(M1) = carr(M2)
      proof
       thus carr(M1) c= carr(M2)
         proof let x; assume
A15:        x in carr(M1);
          then reconsider f = x as Multiset of A by A14;
             f"(NAT\{0}) is finite by A12,A15;
          hence thesis by A13;
         end;
       let x; assume
A16:     x in carr(M2);
       then reconsider f = x as Multiset of A by A14;
          f"(NAT\{0}) is finite by A13,A16;
       hence thesis by A12;
      end;
    hence thesis by MONOID_0:29;
   end;
end;

theorem Th34:
 chi a is Element of finite-MultiSet_over A
  proof
      (chi a)"(NAT\{0}) c= {a}
     proof let x; assume x in (chi a)"(NAT\{0});
then A1:     x in dom chi a & (chi a).x in NAT\{0} & dom chi a = A
        by Th29,FUNCT_1:def 13;
      then reconsider y = x as Element of A;
         not (chi a).y in {0} by A1,XBOOLE_0:def 4;
       then (chi a).y <> 0 by TARSKI:def 1;
       then y = a by Th32;
      hence thesis by TARSKI:def 1;
     end;
    then (chi a)"(NAT\{0}) is finite by FINSET_1:13;
   hence thesis by Def6;
  end;

theorem Th35:
 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 set; assume a in dom ({x}|(p^<*x*>));
then A1:     a in dom (p^<*x*>) & (p^<*x*>).a in {x} by FUNCT_1:86;
then a in Seg (len p+len <*x*>) & len <*x*> = 1 by FINSEQ_1:57,def 7
;
       then a in Seg len p \/ {len p+1} & Seg len p = dom p
         by FINSEQ_1:11,def 3;
then A2:     a in dom p or a in {len p+1} by XBOOLE_0:def 2;
      reconsider a as Nat by A1;
         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 A1,FUNCT_1:86;
      hence thesis by A2,XBOOLE_0:def 2;
     end;
   let a be set; assume a in dom ({x}|p) \/ {len p+1};
    then a in dom ({x}|p) or a in {len p+1} by XBOOLE_0:def 2;
then A3:  a in dom p & p.a in {x} or a in {len p+1} & a = len p+1 & x in {x}
     by FUNCT_1:86,TARSKI:def 1;
      len <*x*> = 1 by FINSEQ_1:57;
then A4:  Seg len p = dom p & dom (p^<*x*>) = Seg (len p+1) &
    Seg (len p+1) = Seg len p \/ {len p+1} & (p^<*x*>).(len p+1) = x
     by FINSEQ_1:11,59,def 3,def 7;
then A5:  a in dom (p^<*x*>) by A3,XBOOLE_0:def 2;
   reconsider a as Nat by A3;
      a in dom p implies (p^<*x*>).a = p.a by FINSEQ_1:def 7;
   hence thesis by A3,A4,A5,FUNCT_1:86;
  end;

theorem Th36:
 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 set; assume a in dom ({x}|(p^<*y*>));
then A2:     a in dom (p^<*y*>) & (p^<*y*>).a in {x} by FUNCT_1:86;
then a in Seg (len p+len <*y*>) & len <*y*> = 1 by FINSEQ_1:57,def 7
;
       then a in Seg len p \/ {len p+1} & Seg len p = dom p
         by FINSEQ_1:11,def 3;
then A3:     a in dom p or a in {len p+1} by XBOOLE_0:def 2;
      reconsider a as Nat by A2;
A4:
       (p^<*y*>).(len p+1) = y & not y in {x} by A1,FINSEQ_1:59,TARSKI:def 1;
       then (p^<*y*>).a = p.a by A2,A3,FINSEQ_1:def 7,TARSKI:def 1;
      hence thesis by A2,A3,A4,FUNCT_1:86,TARSKI:def 1;
     end;
   let a be set; assume a in dom ({x}|p);
then A5:  a in dom p & p.a in {x} by FUNCT_1:86;
      len <*y*> = 1 by FINSEQ_1:57;
  then Seg len p = dom p & dom (p^<*y*>) = Seg (len p+1) &
    Seg (len p+1) = Seg len p \/ {len p+1} & (p^<*y*>).(len p+1) = y
     by FINSEQ_1:11,59,def 3,def 7;
then A6:  a in dom (p^<*y*>) by A5,XBOOLE_0:def 2;
   reconsider a as Nat by A5;
      (p^<*y*>).a = p.a by A5,FINSEQ_1:def 7;
   hence thesis by A5,A6,FUNCT_1:86;
  end;

definition let A be set, F be finite Relation;
 cluster A|F -> finite;
 coherence
  proof
      A|F c= F by RELAT_1:117;
   hence thesis by FINSET_1:13;
  end;
end;

definition let A be non empty set, p be FinSequence of A;
 func |.p.| -> Multiset of A means:
Def7:
  for a being Element of A holds it.a = card dom ({a}|p);
  existence
   proof
     deffunc F(Element of A)=card dom ({$1}|p);
     consider m being Function of A,NAT such that
A1:   for a being Element of A holds m.a = F(a) from LambdaD;
       m is Multiset of A by Th28;
    hence thesis by A1;
   end;
  uniqueness
   proof let m1, m2 be Multiset of A such that
A2:  for a being Element of A holds m1.a = card dom ({a}|p) and
A3:  for a being 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 Th33;
   end;
end;

theorem
   |.<*> A.|.a = 0
  proof <*> A = {} & dom {} = {} & dom ({a}|{}) c= dom {}
     by FUNCT_1:89;
    then dom ({a}|<*> A) = {} by XBOOLE_1:3;
   hence thesis by Def7,CARD_1:78;
  end;

theorem Th38:
 |.<*> A.| = A --> 0
  proof
A1:  dom |.<*>A.| = A by Th29;
      now let x; assume x in A; then reconsider a = x as Element of A;
     thus |.<*>A.|.x = card dom ({a}|{}) by Def7
         .= 0 by CARD_1:78,RELAT_1:60,138;
    end;
   hence thesis by A1,FUNCOP_1:17;
  end;

theorem
   |.<*a*>.| = chi a
  proof
A1:  rng <*a*> = {a} by FINSEQ_1:56;
      now let b be Element of A; set x = b;
A2:    <*a*> = (rng<*a*>)|<*a*> by RELAT_1:125;
        a <> x implies {x} misses {a} by ZFMISC_1:17;
      then {x}|<*a*> = ({x}/\rng<*a*>)|<*a*> & (a <> x implies {x}/\{a} = {})
       by A2,RELAT_1:127,XBOOLE_0:def 7;
    then dom <*a*> = Seg 1 & card Seg 1 = 1 & (chi a).a = 1 &
      {a}|<*a*> = <*a*> & (x <> a implies {x}|<*a*> = {} & (chi a).b = 0)
       by A1,Th32,FINSEQ_1:55,78,RELAT_1:125,137;
     hence |.<*a*>.|.x = (chi a).x by Def7,CARD_1:78,RELAT_1:60;
    end;
   hence thesis by Th33;
  end;

reserve p,q for FinSequence of A;

theorem Th40:
 |.p^<*a*>.| = |.p.| [*] chi a
  proof
      now let b be Element of A;
      reconsider pa = p^<*a*> as FinSequence of A;
        len p < len p+1 by NAT_1:38;
      then not len p+1 in dom p & dom p is finite &
       dom ({b}|p) c= dom p by FINSEQ_3:27,FUNCT_1:89;
      then not len p+1 in dom ({b}|p) & dom ({b}|p) is finite;
      then |.p^<*a*>.|.b = card dom ({b}|pa) & |.p.|.b = card dom ({b}|p) &
      dom ({a}|(p^<*a*>)) = dom ({a}|p) \/ {len p+1} & (chi a).a = 1 &
      (a <> b implies dom ({b}|(p^<*a*>)) = dom ({b}|p) & (chi a).b = 0) &
      card (dom ({b}|p) \/ {len p+1}) = (card dom ({b}|p))+1 &
      (b = a or b <> a) & (|.p.| [*] chi a).b = (|.p.|.b) + ((chi a).b)
       by Def7,Th30,Th32,Th35,Th36,CARD_2:54;
     hence |.p^<*a*>.|.b = (|.p.| [*] chi a).b;
    end;
   hence thesis by Th33;
  end;

theorem Th41:
 |.p^q.| = |.p.|[*]|.q.|
  proof
  defpred P[Nat] means for q st len q = $1 holds |.p^q.| = |.p.|[*]|.q.|;
A1: P[0]
     proof let q; assume len q = 0;
       then q = {} by FINSEQ_1:25;
       then p^q = p & q = <*> A & |.<*>A.| = A-->0 & A-->0 = un(MultiSet_over
A)
        by Th27,Th38,FINSEQ_1:47;
      hence thesis by MONOID_0:18;
     end;
A2:  for n st P[n] holds P[n+1]
     proof let n such that
A3:    for q st len q = n holds |.p^q.| = |.p.|[*]|.q.|;
      let q; assume
A4:    len q = n+1;
       then q <> {} by FINSEQ_1:25;
      then consider r being FinSequence, x being set such that
A5:    q = r^<*x*> by FINSEQ_1:63;
      reconsider r as FinSequence of A by A5,FINSEQ_1:50;
         len <*x*> = 1 by FINSEQ_1:57;
       then n+1 = len r+1 by A4,A5,FINSEQ_1:35;
then A6:    len r = n by XCMPLX_1:2;
         rng <*x*> = {x} by FINSEQ_1:56;
       then {x} c= rng q & rng q c= A by A5,FINSEQ_1:43,def 4;
       then {x} c= A by XBOOLE_1:1;
      then reconsider x as Element of A by ZFMISC_1:37;
      thus |.p^q.| = |.p^r^<*x*>.| by A5,FINSEQ_1:45
         .= |.p^r.|[*] chi x by Th40
         .= |.p.|[*]|.r.|[*] chi x by A3,A6
         .= |.p.|[*](|.r.|[*] chi x) by VECTSP_1:def 16
         .= |.p.|[*]|.q.| by A5,Th40;
     end;

A7:  for n holds P[n] from Ind(A1,A2);
      len q = len q;
   hence thesis by A7;
  end;

theorem Th42:
 |.n .--> a.|.a = n &
   for b being Element of A st b <> a holds |.n .--> a.|.b = 0
  proof
    defpred P[Nat] means |.$1 .--> a.|.a = $1;
A1:  (A-->0).a = 0 & 0.-->a = {} & {} = <*>A
     by FINSEQ_2:72,FUNCOP_1:13;
then A2: P[0] by Th38;
A3:  for n st P[n] holds P[n+1]
     proof let n such that
A4:    |.n .--> a.|.a = n;
      thus |.(n+1) .--> a.|.a = |.(n .--> a)^<*a*>.|.a by FINSEQ_2:74
            .= (|.n .--> a.|[*]chi a).a by Th40
            .= n+(chi a).a by A4,Th30 .= n+1 by Th32;
     end;
      for n holds P[n] from Ind(A2,A3);
   hence |.n .--> a.|.a = n;
   let b be Element of A such that
A5:  b <> a;
    defpred P[Nat] means |.$1 .--> a.|.b = 0;
      (A-->0).b = 0 by FUNCOP_1:13;
then A6: P[0] by A1,Th38;
A7:  for n st P[n] holds P[(n+1)]
     proof let n such that
A8:    |.n .--> a.|.b = 0;
      thus |.(n+1) .--> a.|.b = |.(n .--> a)^<*a*>.|.b by FINSEQ_2:74
            .= (|.n .--> a.|[*]chi a).b by Th40
            .= 0+(chi a).b by A8,Th30 .= 0 by A5,Th32;
     end;
      for n holds P[n] from Ind(A6,A7);
   hence thesis;
  end;

reserve fm for Element of finite-MultiSet_over A;

theorem
   |.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:  Q[0]
     proof let p; assume len p = 0; then p = <*> A by FINSEQ_1:32;
       then |.p.| = A --> 0 by Th38 .= un(MultiSet_over A) by Th27
            .= un(finite-MultiSet_over A) by MONOID_0:def 24;
      hence thesis;
     end;
A2:  for n st Q[n] holds Q[n+1]
     proof let n such that
A3:    for p st len p = n holds P[p];
      let p; assume
A4:    len p = n+1;
       then p <> {} by FINSEQ_1:25;
      then consider r being FinSequence, x being set such that
A5:    p = r^<*x*> by FINSEQ_1:63;
      reconsider r as FinSequence of A by A5,FINSEQ_1:50;
         len <*x*> = 1 by FINSEQ_1:57;
       then n+1 = len r+1 by A4,A5,FINSEQ_1:35;
then A6:    len r = n by XCMPLX_1:2;
         rng <*x*> = {x} by FINSEQ_1:56;
       then {x} c= rng p & rng p c= A by A5,FINSEQ_1:43,def 4;
       then {x} c= A by XBOOLE_1:1;
      then reconsider x as Element of A by ZFMISC_1:37;
      set M = finite-MultiSet_over A;
      reconsider r' = |.r.|, a = chi x as Element of M
      by A3,A6,Th34;
         M is SubStr of MultiSet_over A by MONOID_0:23;
       then r'[*]a = |.r.|[*]chi x by MONOID_0:27 .= |.p.| by A5,Th40;
      hence thesis;
     end;
A7:  for n holds Q[n] from Ind(A1,A2);
      len p = len p;
   hence thesis by A7;
  end;

theorem
   x is Element of finite-MultiSet_over A implies
 ex p st x = |.p.|
  proof
    defpred Z[Nat] means for fm st for V being finite set
    st V = fm"(NAT\{0}) holds card V = $1
     ex p st fm = |.p.|;
A1:  Z[0]
     proof let fm such that
A2:    for V being finite set st V = fm"(NAT\{0}) holds card V = 0;
      take p = <*> A;
         carr(finite-MultiSet_over A) c= carr(MultiSet_over A)
        by MONOID_0:25;
      then reconsider m = fm as Multiset of A by TARSKI:def 3;
      reconsider V = m"(NAT\{0}) as finite set by Def6;
         card V = 0 by A2;
       then fm"(NAT\{0}) = {} by CARD_2:59;
       then rng fm misses (NAT\{0}) by RELAT_1:173;
then A3:    {} = rng fm /\ (NAT\{0}) by XBOOLE_0:def 7
        .= (rng fm /\ NAT)\{0} by XBOOLE_1:49;
         rng m c= NAT;
       then rng fm /\ NAT = rng fm by XBOOLE_1:28;
then A4:    rng fm c= {0} & dom m = A by A3,Th29,XBOOLE_1:37;
      consider a;
A5:    fm.a in rng fm by A4,FUNCT_1:def 5
; then fm.a = 0 by A4,TARSKI:def 1;
       then {0} c= rng fm by A5,ZFMISC_1:37;
       then rng fm = {0} by A4,XBOOLE_0:def 10;
      hence fm = A --> 0 by A4,FUNCOP_1:15 .= |.p.| by Th38;
     end;
A6:  for n st Z[n] holds Z[n+1]
     proof let n such that
A7:    for fm st
        for V being finite set st V = fm"(NAT\{0}) holds card V = n
         ex p st fm = |.p.|;
      let fm such that
A8:    for V being finite set st V = fm"(NAT\{0}) holds card V = n+1;
         carr(finite-MultiSet_over A) c= carr(MultiSet_over A)
        by MONOID_0:25;
      then reconsider m = fm as Multiset of A by TARSKI:def 3;
      consider x being Element of fm"(NAT\{0});
      reconsider V = m"(NAT\{0}) as finite set by Def6;
A9:   card V = n+1 by A8;
then A10:   x in dom fm & fm.x in NAT\{0} & dom m = A by Th29,CARD_1:47,FUNCT_1
:def 13;
      then reconsider x as Element of A;
      defpred C[set] means x = $1;
      deffunc F(set) = 0;
      deffunc G(set) = fm.$1;
      consider f being Function such that
A11:    dom f = A & for a being set st a in A holds (C[a] implies f.a = F(a)) &
        (not C[a] implies f.a = G(a)) from LambdaC;
         rng f c= NAT
        proof let y; assume y in rng f;
         then consider z being set such that
A12:       z in dom f & y = f.z by FUNCT_1:def 5;
         reconsider z as Element of A by A11,A12;
            z = x or z <> x; then y = 0 or y = m.z by A11,A12;
         hence thesis;
        end;
      then reconsider f as Function of A,NAT by A11,FUNCT_2:def 1,RELSET_1:11;
      reconsider f as Multiset of A by Th28;
A13:    f"(NAT\{0}) = (fm"(NAT\{0}))\{x}
        proof
         thus f"(NAT\{0}) c= (fm"(NAT\{0}))\{x}
          proof let y; assume A14: y in f"(NAT\{0});
then A15:         y in dom f & f.y in NAT\{0} by FUNCT_1:def 13;
           reconsider a = y as Element of A by A11,A14,FUNCT_1:def 13;
              not f.a in {0} by A15,XBOOLE_0:def 4;
            then f.a <> 0 by TARSKI:def 1;
            then a <> x by A11;
then A16:         not a in {x} & f.a = fm.a by A11,TARSKI:def 1;
            then a in fm"(NAT\{0}) by A10,A15,FUNCT_1:def 13;
           hence thesis by A16,XBOOLE_0:def 4;
          end;
         let y; assume y in (fm"(NAT\{0}))\{x};
          then y in fm"(NAT\{0}) & not y in {x} by XBOOLE_0:def 4;
then A17:       y in dom fm & fm.y in NAT\{0} & y <> x by FUNCT_1:def 13,TARSKI
:def 1
;
          then fm.y = f.y by A10,A11;
         hence thesis by A10,A11,A17,FUNCT_1:def 13;
        end;
       then f"(NAT\{0}) is finite by A9,FINSET_1:16;
      then reconsider f' = f as Element of finite-MultiSet_over
A
      by Def6;
      reconsider V' = f'"(NAT\{0}) as finite set by Def6;
         {x} c= fm"(NAT\{0}) & card {x} = 1 by A9,CARD_1:47,79,ZFMISC_1:37;
       then card V' = n+1-1 by A9,A13,CARD_2:63
         .= n+(1-1) by XCMPLX_1:29 .= n;
       then for V being finite set st V = f'"(NAT\{0}) holds card V = n;
      then consider p such that
A18:    f = |.p.| by A7;
      take q = p^((m.x) .--> x);
       set g = |.(m.x) .--> x.|;
         now let a;
A19:      f.x = 0 & g.x = m.x & 0 + m.a = m.a & m.a + 0 = m.a
          by A11,Th42;
           a <> x implies f.a = m.a & g.a = 0 by A11,Th42;
        hence (f[*]g).a = m.a by A19,Th30;
       end;
      hence fm = f[*]g by Th33 .= |.q.| by A18,Th41;
     end;
A20:  for n holds Z[n] from Ind(A1,A6);
   assume x is Element of finite-MultiSet_over A;
   then reconsider m = x as Element of finite-MultiSet_over A;
      carr(finite-MultiSet_over A) c= carr(MultiSet_over A)
     by MONOID_0:25;
    then m is Multiset of A by TARSKI:def 3;
   then reconsider V = m"(NAT\{0}) as finite set by Def6;
      for V' being finite set st V' = m"(NAT\{0}) holds card V' = card V;
   hence thesis by A20;
  end;

begin :: Monoid of subsets of a semigroup

reserve a,b,c for Element of D;

definition let D1,D2,D be non empty set, f be Function of D1,D2,D;
 func f.:^2 -> Function of bool D1, bool D2, bool D means:
Def8:
  for x being 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 being Function of bool D1,bool D2,bool D st
        for x being Element of [:bool D1, bool D2:] holds f.x = F(x)
     from LambdaD;
     hence thesis;
   end;
  uniqueness
   proof let F1,F2 be Function of bool D1, bool D2, bool D such that
A1:  for x being Element of [:bool D1, bool D2:] holds
      F1.x = f.:[:x`1,x`2:] and
A2:  for x being 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:113;
   end;
end;

theorem Th45:
 for D1,D2,D being non empty set, f being Function of D1,D2,D
  for X1 being Subset of D1, X2 being 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;
A1:  [X1,X2]`1 = X1 & [X1,X2]`2 = X2 by MCART_1:7;
   thus (f.:^2).(X1,X2) = (f.:^2).[X1,X2] by BINOP_1:def 1
        .= f.:[:X1,X2:] by A1,Def8;
  end;

theorem Th46:
 for D1,D2,D being non empty set, f being Function of D1,D2,D
  for X1 being Subset of D1, X2 being Subset of D2, x1,x2 being 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
A1:  x1 in X1 & x2 in X2;
   then reconsider a = x1 as Element of D1;
   reconsider b = x2 as Element of D2 by A1;
A2:  (f.:^2).(X1,X2) = f.:[:X1,X2:] by Th45;
      f.(a,b) = f.[a,b] & [a,b] in [:X1,X2:] & dom f = [:D1,D2:]
    by A1,BINOP_1:def 1,FUNCT_2:def 1,ZFMISC_1:106;
   hence thesis by A2,FUNCT_1:def 12;
  end;

theorem
   for D1,D2,D being non empty set, f being Function of D1,D2,D
  for X1 being Subset of D1, X2 being Subset of D2 holds
   (f.:^2).(X1,X2) =
   {f.(a,b) where a is Element of D1, b is 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 is Element of D1, b is Element of D2:
            a in X1 & b in X2};
A1:  (f.:^2).(X1,X2) = f.:[:X1,X2:] & X1 c= D1 & X2 c= D2 by Th45;
   thus (f.:^2).(X1,X2) c= A
     proof let x; assume x in f.:^2.(X1,X2);
      then consider y such that
A2:     y in dom f & y in [:X1,X2:] & x = f.y by A1,FUNCT_1:def 12;
      consider y1,y2 being set such that
A3:     y1 in X1 & y2 in X2 & y = [y1,y2] by A2,ZFMISC_1:103;
      reconsider y1 as Element of D1 by A3;
      reconsider y2 as Element of D2 by A3;
         x = f.(y1,y2) by A2,A3,BINOP_1:def 1;
      hence thesis by A3;
     end;
   let x; assume x in A;
    then ex a being Element of D1, b being Element of D2 st
     x = f.(a,b) & a in X1 & b in X2;
   hence thesis by Th46;
  end;

theorem Th48:
 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; assume x in o.:[:X,Y:];
        then consider y such that
A2:       y in dom o & y in [:X,Y:] & x = o.y by FUNCT_1:def 12;
A3:       dom o = [:D,D:] by FUNCT_2:def 1;
        reconsider y as Element of [:D,D:] by A2,FUNCT_2:def 1;
           y = [y`1,y`2] by MCART_1:23;
         then y`1 in X & y`2 in Y & x = o.(y`1,y`2) & o.(y`1,y`2) = o.(y`2,y`1
)
          by A1,A2,BINOP_1:def 1,ZFMISC_1:106;
         then [y`2,y`1] in [:D,D:] & [y`2,y`1] in [:Y,X:] & x = o.[y`2,y`1]
          by BINOP_1:def 1,ZFMISC_1:106;
        hence thesis by A3,FUNCT_1:def 12;
       end;
    end;
   hence o.:[:X,Y:] c= o.:[:Y,X:] & o.:[:Y,X:] c= o.:[:X,Y:];
  end;

theorem Th49:
 o is associative implies o.:[:o.:[:X,Y:],Z:] = o.:[:X,o.:[:Y,Z:]:]
  proof assume
A1:  o.(o.(a,b),c) = o.(a,o.(b,c));
A2:  dom o = [:D,D:] by FUNCT_2:def 1;
   thus o.:[:o.:[:X,Y:],Z:] c= o.:[:X,o.:[:Y,Z:]:]
     proof let x; assume x in o.:[:o.:[:X,Y:],Z:];
      then consider y such that
A3:     y in dom o & y in [:o.:[:X,Y:],Z:] & x = o.y by FUNCT_1:def 12;
      reconsider y as Element of [:D,D:] by A3,FUNCT_2:def 1;
         y = [y`1,y`2] by MCART_1:23;
then A4:     y`1 in o.:[:X,Y:] & y`2 in Z & x = o.(y`1,y`2)
        by A3,BINOP_1:def 1,ZFMISC_1:106;
      then consider z such that
A5:     z in dom o & z in [:X,Y:] & y`1 = o.z by FUNCT_1:def 12;
      reconsider z as Element of [:D,D:] by A5,FUNCT_2:def 1;
         z = [z`1,z`2] by MCART_1:23;
then A6:     z`1 in X & z`2 in Y & y`1 = o.(z`1,z`2)
        by A5,BINOP_1:def 1,ZFMISC_1:106;
       then x = o.(z`1,o.(z`2,y`2)) & o.(z`2,y`2) = o.[z`2,y`2] &
       [z`2,y`2] in [:Y,Z:] by A1,A4,BINOP_1:def 1,ZFMISC_1:106;
then A7:     o.(z`2,y`2) in o.:[:Y,Z:] & x = o.[z`1,o.(z`2,y`2)]
        by A2,BINOP_1:def 1,FUNCT_1:def 12;
       then [z`1,o.(z`2,y`2)] in [:X,o.:[:Y,Z:]:] by A6,ZFMISC_1:106;
      hence thesis by A2,A7,FUNCT_1:def 12;
     end;
   let x; assume x in o.:[:X,o.:[:Y,Z:]:];
   then consider y such that
A8:  y in dom o & y in [:X,o.:[:Y,Z:]:] & x = o.y by FUNCT_1:def 12;
   reconsider y as Element of [:D,D:] by A8,FUNCT_2:def 1;
      y = [y`1,y`2] by MCART_1:23;
then A9:  y`2 in o.:[:Y,Z:] & y`1 in X & x = o.(y`1,y`2)
     by A8,BINOP_1:def 1,ZFMISC_1:106;
   then consider z such that
A10:  z in dom o & z in [:Y,Z:] & y`2 = o.z by FUNCT_1:def 12;
   reconsider z as Element of [:D,D:] by A10,FUNCT_2:def 1;
      z = [z`1,z`2] by MCART_1:23;
then A11:  z`1 in Y & z`2 in Z & y`2 = o.(z`1,z`2)
     by A10,BINOP_1:def 1,ZFMISC_1:106;
    then x = o.(o.(y`1,z`1),z`2) & o.(y`1,z`1) = o.[y`1,z`1] &
    [y`1,z`1] in [:X,Y:] by A1,A9,BINOP_1:def 1,ZFMISC_1:106;
then A12:  o.(y`1,z`1) in o.:[:X,Y:] & x = o.[o.(y`1,z`1),z`2]
     by A2,BINOP_1:def 1,FUNCT_1:def 12;
    then [o.(y`1,z`1),z`2] in [:o.:[:X,Y:],Z:] by A11,ZFMISC_1:106;
   hence thesis by A2,A12,FUNCT_1:def 12;
  end;

theorem Th50:
 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 Th45
     .= o.:[:y,x:] by A1,Th48 .= (o.:^2).(y,x) by Th45;
  end;

theorem Th51:
 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 Th45
     .= o.:[:o.:[:x,y:],z:] by Th45
     .= o.:[:x,o.:[:y,z:]:] by A1,Th49
     .= (o.:^2).(x,o.:[:y,z:]) by Th45
     .= (o.:^2).(x,(o.:^2).(y,z)) by Th45;
  end;

theorem Th52:
 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;
A2:  dom o = [:D,D:] by FUNCT_2:def 1;
   thus o.:[:{a},X:] c= D /\ X
     proof let x; assume x in o.:[:{a},X:];
      then consider y such that
A3:     y in dom o & y in [:{a},X:] & x = o.y by FUNCT_1:def 12;
      reconsider y as Element of [:D,D:] by A3,FUNCT_2:def 1;
A4:     y = [y`1,y`2] by MCART_1:23;
       then y`1 in {a} & y`2 in X by A3,ZFMISC_1:106;
       then x = o.(y`1,y`2) & o.(a,y`2) = y`2 & y`1 = a & y`2 in D /\ X
        by A1,A3,A4,BINOP_1:11,def 1,TARSKI:def 1,XBOOLE_0:def 3;
      hence thesis;
     end;
   thus D /\ X c= o.:[:{a},X:]
     proof let x; assume A5: x in D /\ X;
then A6:     x in D & x in X by XBOOLE_0:def 3;
      reconsider d = x as Element of D by A5,XBOOLE_0:def 3;
A7:     x = o.(a,d) by A1,BINOP_1:11 .= o.[a,x] by BINOP_1:def 1;
         a in {a} by TARSKI:def 1;
       then [a,d] in [:{a},X:] by A6,ZFMISC_1:106;
      hence thesis by A2,A7,FUNCT_1:def 12;
     end;
   thus o.:[:X,{a}:] c= D /\ X
     proof let x; assume x in o.:[:X,{a}:];
      then consider y such that
A8:     y in dom o & y in [:X,{a}:] & x = o.y by FUNCT_1:def 12;
      reconsider y as Element of [:D,D:] by A8,FUNCT_2:def 1;
A9:     y = [y`1,y`2] by MCART_1:23;
       then y`2 in {a} & y`1 in X by A8,ZFMISC_1:106;
       then x = o.(y`1,y`2) & o.(y`1,a) = y`1 & y`2 = a & y`1 in D /\ X
        by A1,A8,A9,BINOP_1:11,def 1,TARSKI:def 1,XBOOLE_0:def 3;
      hence thesis;
     end;
   thus D /\ X c= o.:[:X,{a}:]
     proof let x; assume A10: x in D /\ X;
then A11:     x in D & x in X by XBOOLE_0:def 3;
      reconsider d = x as Element of D by A10,XBOOLE_0:def 3;
A12:     x = o.(d,a) by A1,BINOP_1:11 .= o.[x,a] by BINOP_1:def 1;
         a in {a} by TARSKI:def 1;
       then [d,a] in [:X,{a}:] by A11,ZFMISC_1:106;
      hence thesis by A2,A12,FUNCT_1:def 12;
     end;
  end;

theorem Th53:
 a is_a_unity_wrt o implies {a} is_a_unity_wrt o.:^2 &
  o.:^2 has_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 Th45 .= D /\ x by A1,Th52
       .= x by XBOOLE_1:28;
     thus (o.:^2).(x,{a}) = o.:[:x,{a}:] by Th45 .= D /\ x by A1,Th52
       .= x by XBOOLE_1:28;
    end;
   hence
A2:  {a} is_a_unity_wrt o.:^2 by BINOP_1:11;
   hence ex A being Subset of D st A is_a_unity_wrt o.:^2;
   thus thesis by A2,BINOP_1:def 8;
  end;

theorem Th54:
 o has_a_unity implies o.:^2 has_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} is_a_unity_wrt o.:^2 & o.:^2 has_a_unity & a = the_unity_wrt o &
    the_unity_wrt o.:^2 = {a} by A1,Th53,BINOP_1:def 8;
   hence thesis;
  end;

theorem Th55:
 o is uniquely-decomposable implies o.:^2 is uniquely-decomposable
  proof assume that
A1:  o has_a_unity and
A2:  o.(a,b) = the_unity_wrt o implies a = b & b = the_unity_wrt o;
   thus o.:^2 has_a_unity by A1,Th54;
   set a = the_unity_wrt o;
   let A,B be Subset of D such that
A3:  (o.:^2).(A,B) = the_unity_wrt o.:^2;
A4:  the_unity_wrt o.:^2 = {a} & o.:[:A,B:] = (o.:^2).(A,B) & a in {a}
     by A1,Th45,Th54,TARSKI:def 1;
    then dom o meets [:A,B:] by A3,RELAT_1:151;
    then dom o /\ [:A,B:] <> {} by XBOOLE_0:def 7;
    then [:A,B:] <> {};
then A5:  A <> {} & B <> {} & A c= D & B c= D by ZFMISC_1:113;
   consider a1 being Element of A, a2 being Element of B;
   reconsider a1,a2 as Element of D by A5,TARSKI:def 3;
      o.(a1,a2) in {a} by A3,A4,A5,Th46;
    then o.(a1,a2) = a by TARSKI:def 1;
then A6:  a1 = a2 & a2 = a & {a1} c= A & {a2} c= B by A2,A5,ZFMISC_1:37;
A7:  A c= {a}
     proof let x; assume
A8:    x in A; then reconsider c = x as Element of D;
         o.(c,a2) in {a} by A3,A4,A5,A8,Th46;
       then o.(c,a2) = a by TARSKI:def 1;
       then c = a2 by A2;
      hence thesis by A6,TARSKI:def 1;
     end;
      B c= {a}
     proof let x; assume
A9:    x in B; then reconsider c = x as Element of D;
         o.(a1,c) in {a} by A3,A4,A5,A9,Th46;
       then o.(a1,c) = a by TARSKI:def 1;
       then c = a by A2;
      hence thesis by TARSKI:def 1;
     end;
    then A = {a} & B = {a} by A6,A7,XBOOLE_0:def 10;
   hence thesis by A1,Th54;
  end;

definition let G be non empty HGrStr;
 func bool G -> HGrStr equals:
Def9:
   multLoopStr(#bool the carrier of G, (the mult of G).:^2,
     {the_unity_wrt the mult of G}#) if G is unital otherwise
   HGrStr(#bool the carrier of G, (the mult of G).:^2#);
  correctness;
end;

definition let G be non empty HGrStr;
 cluster bool G -> non empty;
 coherence
  proof
   per cases;
   suppose G is unital;
    then bool G = multLoopStr(#bool the carrier of G, (the mult of G).:^2,
     {the_unity_wrt the mult of G}#) by Def9;
    hence the carrier of bool G is non empty;
   suppose G is not unital;
    then bool G = HGrStr(#bool the carrier of G, (the mult of G).:^2#) by Def9
;
    hence the carrier of bool G is non empty;
  end;
end;

definition let G be unital (non empty HGrStr);
 redefine func bool G -> well-unital strict (non empty multLoopStr);
  coherence
   proof op(G) has_a_unity by MONOID_0:def 10;
     then bool G = multLoopStr(#bool carr(G), op(G).:^2,{the_unity_wrt op(G)}
#) &
     {the_unity_wrt op(G)} is_a_unity_wrt op(G).:^2 by Def9,Th54;
    hence thesis by MONOID_0:def 21;
   end;
end;

theorem Th56:
 the carrier of bool G = bool the carrier of G &
 the mult of bool G = (the mult of G).:^2
  proof G is unital or not G is unital;
    then bool G = multLoopStr(#bool carr(G), op(G).:^2,{the_unity_wrt op(G)}#)
or
    bool G = HGrStr(#bool the carrier of G, op(G).:^2#) by Def9;
   hence thesis;
  end;

theorem
   for G being unital (non empty HGrStr) holds
   the unity of bool G = {the_unity_wrt the mult of G}
  proof let G be unital (non empty HGrStr);
      bool G = multLoopStr(#bool carr(G), op(G).:^2,{the_unity_wrt op(G)}#)
     by Def9;
   hence thesis;
  end;

theorem
   for G being non empty HGrStr 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 HGrStr;
A1:  op(bool G) = op(G).:^2 & carr(bool G) = bool carr(G) by Th56;
   thus G is commutative implies bool G is commutative
    proof assume op(G) is commutative;
     hence op(bool G) is commutative by A1,Th50;
    end;
   thus G is associative implies bool G is associative
    proof assume op(G) is associative;
     hence op(bool G) is associative by A1,Th51;
    end;
   assume op(G) is uniquely-decomposable;
   hence op(bool G) is uniquely-decomposable by A1,Th55;
  end;


Back to top