:: Monoids
::  by Grzegorz Bancerek
::
:: Received December 29, 1992
:: Copyright (c) 1992-2021 Association of Mizar Users
::           (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.

environ

 vocabularies STRUCT_0, ALGSTR_0, BINOP_1, SUBSET_1, FUNCT_1, FINSEQ_1,
      RELAT_1, ORDINAL4, XBOOLE_0, ALGSTR_1, SETWISEO, FUNCOP_1, ZFMISC_1,
      GROUP_1, FINSEQOP, MESFUNC1, VECTSP_1, TARSKI, REALSET1, MCART_1,
      NUMBERS, BINOP_2, REAL_1, ARYTM_3, CARD_1, GR_CY_1, INT_1, PARTFUN1,
      FUNCT_2, MONOID_0;
 notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, ORDINAL1, NUMBERS, XCMPLX_0,
      XREAL_0, XTUPLE_0, MCART_1, DOMAIN_1, BINOP_2, REALSET1, STRUCT_0,
      RELAT_1, FINSEQOP, FUNCT_1, FINSEQ_1, PARTFUN1, FUNCT_2, BINOP_1,
      FINSEQ_2, INT_1, GROUP_1, VECTSP_1, SETWISEO, FUNCOP_1, GR_CY_1,
      ALGSTR_0;
 constructors RELAT_2, PARTFUN1, BINOP_1, SETWISEO, BINOP_2, FINSEQOP,
      REALSET1, VECTSP_2, GR_CY_1, RELSET_1, XTUPLE_0, NUMBERS;
 registrations XBOOLE_0, SUBSET_1, RELAT_1, FUNCT_1, ORDINAL1, PARTFUN1,
      FUNCT_2, NUMBERS, BINOP_2, MEMBERED, FINSEQ_1, REALSET1, STRUCT_0,
      GROUP_1, ALGSTR_0, GR_CY_1, XREAL_0, NAT_1;
 requirements NUMERALS, BOOLE, SUBSET, ARITHM;


begin :: Updating

reserve x,y,X,Y for set;

definition
  let G be 1-sorted;
  mode BinOp of G is BinOp of the carrier of G;
end;

definition
  let IT be 1-sorted;
  attr IT is constituted-Functions means
:: MONOID_0:def 1

  for a being Element of IT holds a is Function;
  attr IT is constituted-FinSeqs means
:: MONOID_0:def 2

  for a being Element of IT holds a is FinSequence;
end;

registration
  cluster constituted-Functions for 1-sorted;
  cluster constituted-FinSeqs for 1-sorted;
end;

registration
  let X be constituted-Functions 1-sorted;
  cluster -> Function-like Relation-like for Element of X;
end;

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

registration
  let X be constituted-FinSeqs 1-sorted;
  cluster -> FinSequence-like for Element of X;
end;

definition
  let D be set, p,q be FinSequence of D;
  redefine func p^q -> Element of D*;
end;

notation
  let g,f be Function;
  synonym f(*)g for f*g;
end;

definition
  let D be non empty set;
  let IT be BinOp of D;
  attr IT is left-invertible means
:: MONOID_0:def 3
  for a,b being Element of D ex l being Element of D st IT.(l,a) = b;
  attr IT is right-invertible means
:: MONOID_0:def 4
  for a,b being Element of D ex r being Element of D st IT.(a,r) = b;
  attr IT is invertible means
:: MONOID_0:def 5

  for a,b being Element of D ex r,l being
  Element of D st IT.(a,r) = b & IT.(l,a) = b;
  attr IT is left-cancelable means
:: MONOID_0:def 6
  for a,b,c being Element of D st IT.(a,b) = IT.(a,c) holds b = c;
  attr IT is right-cancelable means
:: MONOID_0:def 7
  for a,b,c being Element of D st IT.(b,a) = IT.(c,a) holds b = c;
  attr IT is cancelable means
:: MONOID_0:def 8
  for a,b,c being Element of D st IT.(a,b) = IT.(a
  ,c) or IT.(b,a) = IT.(c,a) holds b = c;
  attr IT is uniquely-decomposable means
:: MONOID_0:def 9
  IT is having_a_unity & for a,b being
Element of D st IT.(a,b) = the_unity_wrt IT holds a = b & b = the_unity_wrt IT;
end;

theorem :: MONOID_0:1
  for D be non empty set, f being BinOp of D holds f is invertible
  iff f is left-invertible right-invertible;

theorem :: MONOID_0:2
  for D be non empty set, f being BinOp of D holds f is cancelable
  iff f is left-cancelable right-cancelable;

theorem :: MONOID_0:3
  for f being BinOp of {x} holds f = (x,x) .--> x & f is
  having_a_unity & f is commutative & f is associative & f is idempotent & f is
  invertible cancelable uniquely-decomposable;

begin :: Semigroups

reserve G for non empty multMagma,
  D for non empty set,
  a,b,c,r,l for Element of G;

definition
  let IT be non empty multMagma;
  redefine attr IT is unital means
:: MONOID_0:def 10

  the multF of IT is having_a_unity;
end;

definition
  let G;
  redefine attr G is commutative means
:: MONOID_0:def 11

  the multF of G is commutative;
  redefine attr G is associative means
:: MONOID_0:def 12

  the multF of G is associative;
end;

definition
  let IT be non empty multMagma;
  attr IT is idempotent means
:: MONOID_0:def 13
  the multF of IT is idempotent;
  attr IT is left-invertible means
:: MONOID_0:def 14
  the multF of IT is left-invertible;
  attr IT is right-invertible means
:: MONOID_0:def 15
  the multF of IT is right-invertible;
  attr IT is invertible means
:: MONOID_0:def 16

  the multF of IT is invertible;
  attr IT is left-cancelable means
:: MONOID_0:def 17
  the multF of IT is left-cancelable;
  attr IT is right-cancelable means
:: MONOID_0:def 18
  the multF of IT is right-cancelable;
  attr IT is cancelable means
:: MONOID_0:def 19
  the multF of IT is cancelable;
  attr IT is uniquely-decomposable means
:: MONOID_0:def 20

  the multF of IT is uniquely-decomposable;
end;

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

theorem :: MONOID_0:4
  G is unital implies the_unity_wrt the multF of G is_a_unity_wrt
  the multF of G;

theorem :: MONOID_0:5
  G is unital iff for a holds (the_unity_wrt the multF of G)*a = a & a*(
  the_unity_wrt the multF of G) = a;

theorem :: MONOID_0:6
  G is unital iff ex a st for b holds a*b = b & b*a = b;

theorem :: MONOID_0:7
  G is idempotent iff for a holds a*a = a;

theorem :: MONOID_0:8
  G is left-invertible iff for a,b ex l st l*a = b;

theorem :: MONOID_0:9
  G is right-invertible iff for a,b ex r st a*r = b;

theorem :: MONOID_0:10
  G is invertible iff for a,b ex r,l st a*r = b & l*a = b;

theorem :: MONOID_0:11
  G is left-cancelable iff for a,b,c st a*b = a*c holds b = c;

theorem :: MONOID_0:12
  G is right-cancelable iff for a,b,c st b*a = c*a holds b = c;

theorem :: MONOID_0:13
  G is cancelable iff for a,b,c st a*b = a*c or b*a = c*a holds b = c;

theorem :: MONOID_0:14
  G is uniquely-decomposable iff the multF of G is having_a_unity
& for a,b being Element of G st a*b = the_unity_wrt the multF of G holds a = b
  & b = the_unity_wrt the multF of G;

theorem :: MONOID_0:15
  G is associative implies (G is invertible iff G is unital & the
  multF of G is having_an_inverseOp);

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

registration
  cluster invertible -> left-invertible right-invertible for
non empty multMagma;
  cluster left-invertible right-invertible -> invertible for
non empty multMagma;
  cluster cancelable -> left-cancelable right-cancelable for
non empty multMagma;
  cluster left-cancelable right-cancelable -> cancelable for
non empty multMagma;
  cluster associative invertible -> unital cancelable for
non empty multMagma;
end;

begin

reserve M for non empty multLoopStr;

definition
  let IT be non empty multLoopStr;
  redefine attr IT is well-unital means
:: MONOID_0:def 21

  1.IT is_a_unity_wrt the multF of IT;
end;

theorem :: MONOID_0:16
  M is well-unital iff for a being Element of M holds (1.M)*a = a & a*(1.M) = a
;

theorem :: MONOID_0:17
  for M being non empty multLoopStr st M is well-unital holds 1.M
  = the_unity_wrt the multF of M;

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

definition
  mode Monoid is well-unital associative non empty multLoopStr;
end;

definition
  let G be multMagma;
  mode MonoidalExtension of G -> multLoopStr means
:: MONOID_0:def 22

    the multMagma of it = the multMagma of G;
end;

registration
  let G be non empty multMagma;
  cluster -> non empty for MonoidalExtension of G;
end;

theorem :: MONOID_0:18
  for M being MonoidalExtension of G holds the carrier of M = the
carrier of G & the multF of M = the multF of G & for a,b being Element of M, a9
  ,b9 being Element of G st a = a9 & b = b9 holds a*b = a9*b9;

registration
  let G be multMagma;
  cluster strict for MonoidalExtension of G;
end;

theorem :: MONOID_0:19
  for G being non empty multMagma, M being MonoidalExtension of G
  holds (G is unital implies M is unital) & (G is commutative implies M is
  commutative) & (G is associative implies M is associative) & (G is invertible
  implies M is invertible) & (G is uniquely-decomposable implies M is
  uniquely-decomposable) & (G is cancelable implies M is cancelable);

registration
  let G be constituted-Functions multMagma;
  cluster -> constituted-Functions for MonoidalExtension of G;
end;

registration
  let G be constituted-FinSeqs multMagma;
  cluster -> constituted-FinSeqs for MonoidalExtension of G;
end;

registration
  let G be unital non empty multMagma;
  cluster -> unital for MonoidalExtension of G;
end;

registration
  let G be associative non empty multMagma;
  cluster -> associative for MonoidalExtension of G;
end;

registration
  let G be commutative non empty multMagma;
  cluster -> commutative for MonoidalExtension of G;
end;

registration
  let G be invertible non empty multMagma;
  cluster -> invertible for MonoidalExtension of G;
end;

registration
  let G be cancelable non empty multMagma;
  cluster -> cancelable for MonoidalExtension of G;
end;

registration
  let G be uniquely-decomposable non empty multMagma;
  cluster -> uniquely-decomposable for MonoidalExtension of G;
end;

registration
  let G be unital non empty multMagma;
  cluster well-unital strict for MonoidalExtension of G;
end;

theorem :: MONOID_0:20
  for G being unital non empty multMagma for M1,M2 being
  well-unital strict MonoidalExtension of G holds M1 = M2;

begin :: Subsystems

definition
  let G be multMagma;
  mode SubStr of G -> multMagma means
:: MONOID_0:def 23

    the multF of it c= the multF of G;
end;

registration
  let G be multMagma;
  cluster strict for SubStr of G;
end;

registration
  let G be non empty multMagma;
  cluster strict non empty for SubStr of G;
end;

registration
  let G be unital non empty multMagma;
  cluster unital associative commutative cancelable idempotent invertible
    uniquely-decomposable strict for non empty SubStr of G;
end;

definition
  let G be multMagma;
  mode MonoidalSubStr of G -> multLoopStr means
:: MONOID_0:def 24

    the multF of it c= the
    multF of G & for M being multLoopStr st G = M holds 1.it = 1.M;
end;

registration
  let G be multMagma;
  cluster strict for MonoidalSubStr of G;
end;

registration
  let G be non empty multMagma;
  cluster strict non empty for MonoidalSubStr of G;
end;

definition
  let M be multLoopStr;
  redefine mode MonoidalSubStr of M means
:: MONOID_0:def 25

    the multF of it c= the multF of M & 1.it = 1.M;
end;

registration
  let G be well-unital non empty multLoopStr;
  cluster well-unital associative commutative cancelable idempotent invertible
    uniquely-decomposable strict for non empty MonoidalSubStr of G;
end;

theorem :: MONOID_0:21
  for G being multMagma, M being MonoidalSubStr of G holds M is SubStr of G;

definition
  let G be multMagma, M be MonoidalExtension of G;
  redefine mode SubStr of M -> SubStr of G;
end;

definition
  let G1 be multMagma, G2 be SubStr of G1;
  redefine mode SubStr of G2 -> SubStr of G1;
end;

definition
  let G1 be multMagma, G2 be MonoidalSubStr of G1;
  redefine mode SubStr of G2 -> SubStr of G1;
end;

definition
  let G be multMagma, M be MonoidalSubStr of G;
  redefine mode MonoidalSubStr of M -> MonoidalSubStr of G;
end;

theorem :: MONOID_0:22
  G is SubStr of G & M is MonoidalSubStr of M;

reserve H for non empty SubStr of G,
  N for non empty MonoidalSubStr of G;

theorem :: MONOID_0:23
  the carrier of H c= the carrier of G & the carrier of N c= the carrier of G;

theorem :: MONOID_0:24
  for G being non empty multMagma, H being non empty SubStr of G
  holds the multF of H = (the multF of G)||the carrier of H;

theorem :: MONOID_0:25
  for a,b being Element of H, a9,b9 being Element of G st a = a9 &
  b = b9 holds a*b = a9*b9;

theorem :: MONOID_0:26
  for H1,H2 being non empty SubStr of G st the carrier of H1 = the
  carrier of H2 holds the multMagma of H1 = the multMagma of H2;

theorem :: MONOID_0:27
  for H1,H2 being non empty MonoidalSubStr of M st the carrier of H1 =
  the carrier of H2 holds the multLoopStr of H1 = the multLoopStr of H2;

theorem :: MONOID_0:28
  for H1,H2 being non empty SubStr of G st the carrier of H1 c=
  the carrier of H2 holds H1 is SubStr of H2;

theorem :: MONOID_0:29
  for H1,H2 being non empty MonoidalSubStr of M st the carrier of H1 c=
  the carrier of H2 holds H1 is MonoidalSubStr of H2;

theorem :: MONOID_0:30
  G is unital & the_unity_wrt the multF of G in the carrier of H
implies H is unital & the_unity_wrt the multF of G = the_unity_wrt the multF of
  H;

theorem :: MONOID_0:31
  for M being well-unital non empty multLoopStr for N being non
  empty MonoidalSubStr of M holds N is well-unital;

theorem :: MONOID_0:32
  G is commutative implies H is commutative;

theorem :: MONOID_0:33
  G is associative implies H is associative;

theorem :: MONOID_0:34
  G is idempotent implies H is idempotent;

theorem :: MONOID_0:35
  G is cancelable implies H is cancelable;

theorem :: MONOID_0:36
  the_unity_wrt the multF of G in the carrier of H & G is
  uniquely-decomposable implies H is uniquely-decomposable;

theorem :: MONOID_0:37
  for M being well-unital uniquely-decomposable non empty
  multLoopStr for N being non empty MonoidalSubStr of M holds N is
  uniquely-decomposable;

registration
  let G be constituted-Functions non empty multMagma;
  cluster -> constituted-Functions for non empty SubStr of G;
  cluster -> constituted-Functions for non empty MonoidalSubStr of G;
end;

registration
  let G be constituted-FinSeqs non empty multMagma;
  cluster -> constituted-FinSeqs for non empty SubStr of G;
  cluster -> constituted-FinSeqs for non empty MonoidalSubStr of G;
end;

registration
  let M be well-unital non empty multLoopStr;
  cluster -> well-unital for non empty MonoidalSubStr of M;
end;

registration
  let G be commutative non empty multMagma;
  cluster -> commutative for non empty SubStr of G;
  cluster -> commutative for non empty MonoidalSubStr of G;
end;

registration
  let G be associative non empty multMagma;
  cluster -> associative for non empty SubStr of G;
  cluster -> associative for non empty MonoidalSubStr of G;
end;

registration
  let G be idempotent non empty multMagma;
  cluster -> idempotent for non empty SubStr of G;
  cluster -> idempotent for non empty MonoidalSubStr of G;
end;

registration
  let G be cancelable non empty multMagma;
  cluster -> cancelable for non empty SubStr of G;
  cluster -> cancelable for non empty MonoidalSubStr of G;
end;

registration
  let M be well-unital uniquely-decomposable non empty multLoopStr;
  cluster -> uniquely-decomposable for non empty MonoidalSubStr of M;
end;

scheme :: MONOID_0:sch 1
  SubStrEx2 {G() -> non empty multMagma, P[object]}
 : ex H being strict non empty
SubStr of G() st for x being Element of G()
 holds x in the carrier of H iff P[x]
provided
 for x,y being Element of G() holds P[x] & P[y] implies P[x*y] and
 ex x being Element of G() st P[x];

scheme :: MONOID_0:sch 2
  MonoidalSubStrEx2 {G() -> non empty multLoopStr, P[set]}: ex M being strict
  non empty MonoidalSubStr of G() st for x being Element of G() holds x in the
  carrier of M iff P[x]
provided
 for x,y being Element of G() holds P[x] & P[y] implies P[x*y] and
 P[1.G()];

notation
  let G be multMagma, a,b be Element of G;
  synonym a [*] b for a*b;
end;

begin :: Monoids on Nats

definition
  func <REAL,+> -> non empty multMagma equals
:: MONOID_0:def 26
  multMagma(#REAL, addreal#);
end;

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

theorem :: MONOID_0:38
  x is Element of <REAL,+> iff x is Element of REAL;

theorem :: MONOID_0:39
  for N being non empty SubStr of <REAL,+> for a,b being Element
  of N, x,y being Real st a = x & b = y holds a*b = x+y;

theorem :: MONOID_0:40
  for N being unital non empty SubStr of <REAL,+> holds
  the_unity_wrt the multF of N = 0;

registration
  let G be unital non empty multMagma;
  cluster associative invertible -> unital cancelable Group-like for non empty
    SubStr of G;
end;


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

:: corollary
:: INT.Group is unital commutative associative cancelable invertible;

theorem :: MONOID_0:41
  for G being strict non empty SubStr of <REAL,+> holds G = INT.Group
  iff the carrier of G = INT;

theorem :: MONOID_0:42
  x is Element of INT.Group iff x is Integer;

definition
  func <NAT,+> -> unital uniquely-decomposable strict non empty SubStr of
  INT.Group means
:: MONOID_0:def 27

  the carrier of it = NAT;
end;

:: corollary
:: <NAT,+> is unital commutative associative cancelable uniquely-decomposable;

definition
  func <NAT,+,0> -> well-unital strict non empty MonoidalExtension of <NAT,+>
   means
:: MONOID_0:def 28
  not contradiction;
end;

:: corollary
:: <NAT,+,0> is
::   well-unital commutative associative cancelable uniquely-decomposable;

definition
  redefine func addnat equals
:: MONOID_0:def 29
  the multF of <NAT,+>;
end;

theorem :: MONOID_0:43
  <NAT,+> = multMagma(#NAT,addnat#);

theorem :: MONOID_0:44
  x is Element of <NAT,+,0> iff x is Element of NAT;

theorem :: MONOID_0:45
  for n1,n2 being Element of NAT, m1,m2 being Element of <NAT,+,0> st n1
  = m1 & n2 = m2 holds m1*m2 = n1+n2;

theorem :: MONOID_0:46
  <NAT,+,0> = multLoopStr(#NAT,addnat,0#);

theorem :: MONOID_0:47
  addnat = addreal||NAT & addnat = addint||NAT;

theorem :: MONOID_0:48
  0 is_a_unity_wrt addnat & addnat is uniquely-decomposable;

definition
  func <REAL,*> -> unital commutative associative strict non empty multMagma
  equals
:: MONOID_0:def 30
  multMagma(#REAL,multreal#);
end;

theorem :: MONOID_0:49
  x is Element of <REAL,*> iff x is Element of REAL;

theorem :: MONOID_0:50
  for N being non empty SubStr of <REAL,*> for a,b being Element
  of N, x,y being Real st a = x & b = y holds a*b = x*y;

theorem :: MONOID_0:51
  for N being unital non empty SubStr of <REAL,*> holds the_unity_wrt
  the multF of N = 0 or the_unity_wrt the multF of N = 1;

definition
  func <NAT,*> -> unital uniquely-decomposable strict non empty SubStr of
  <REAL,*> means
:: MONOID_0:def 31

  the carrier of it = NAT;
end;

:: corollary
:: <NAT,*> is unital commutative associative uniquely-decomposable;

definition
  func <NAT,*,1> -> well-unital strict non empty MonoidalExtension of <NAT,*>
   means
:: MONOID_0:def 32
  not contradiction;
end;

:: corollary
:: <NAT,*,1> is well-unital commutative associative uniquely-decomposable;

definition
  redefine func multnat equals
:: MONOID_0:def 33
  the multF of <NAT,*>;
end;

theorem :: MONOID_0:52
  <NAT,*> = multMagma(#NAT,multnat#);

theorem :: MONOID_0:53
  for n1,n2 being Element of NAT, m1,m2 being Element of <NAT,*> st n1 =
  m1 & n2 = m2 holds m1*m2 = n1*n2;

theorem :: MONOID_0:54
  the_unity_wrt the multF of <NAT,*> = 1;

theorem :: MONOID_0:55
  for n1,n2 being Element of NAT, m1,m2 being Element of <NAT,*,1> st n1
  = m1 & n2 = m2 holds m1*m2 = n1*n2;

theorem :: MONOID_0:56
  <NAT,*,1> = multLoopStr(#NAT,multnat,1#);

theorem :: MONOID_0:57
  multnat = multreal||NAT;

theorem :: MONOID_0:58
  1 is_a_unity_wrt multnat & multnat is uniquely-decomposable;

begin :: Monoid of finite sequences

definition
  let D be non empty set;
  func D*+^ -> unital associative cancelable uniquely-decomposable
  constituted-FinSeqs strict non empty multMagma means
:: MONOID_0:def 34

  the carrier of it = D* & for p,q being Element of it holds p [*] q = p^q;
end;

definition
  let D;
  func D*+^+<0> -> well-unital strict non empty MonoidalExtension of D*+^
  means
:: MONOID_0:def 35
  not contradiction;
  func D-concatenation -> BinOp of D* equals
:: MONOID_0:def 36
  the multF of D*+^;
end;

theorem :: MONOID_0:59
  D*+^ = multMagma(#D*, D-concatenation#);

theorem :: MONOID_0:60
  the_unity_wrt the multF of D*+^ = {};

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

theorem :: MONOID_0:62
  for a,b being Element of D*+^+<0> holds a [*] b = a^b;

theorem :: MONOID_0:63
  for F being non empty SubStr of D*+^ for p,q being Element of F
  holds p[*]q = p^q;

theorem :: MONOID_0:64
  for F being unital non empty SubStr of D*+^ holds the_unity_wrt the
  multF of F = {};

theorem :: MONOID_0:65
  for F being non empty SubStr of D*+^ st {} is Element of F holds F is
  unital & the_unity_wrt the multF of F = {};

theorem :: MONOID_0:66
  for A,B being non empty set st A c= B holds A*+^ is SubStr of B*+^;

theorem :: MONOID_0:67
  D-concatenation is having_a_unity & the_unity_wrt (D-concatenation) =
  {} & D-concatenation is associative;

begin :: Monoids of mappings

definition
  let X be set;
  func GPFuncs X -> constituted-Functions strict multMagma means
:: MONOID_0:def 37

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

registration
  let X be set;
  cluster GPFuncs X -> unital associative non empty;
end;

definition
  let X be set;
  func MPFuncs X -> well-unital strict non empty MonoidalExtension of GPFuncs
  X means
:: MONOID_0:def 38
  not contradiction;
  func X-composition -> BinOp of PFuncs(X,X) equals
:: MONOID_0:def 39
  the multF of GPFuncs X;
end;

:: corollary
:: MPFuncs X is constituted-Functions strict Monoid;

theorem :: MONOID_0:68
  x is Element of GPFuncs X iff x is PartFunc of X,X;

theorem :: MONOID_0:69
  the_unity_wrt the multF of GPFuncs X = id X;

theorem :: MONOID_0:70
  for F being non empty SubStr of GPFuncs X for f,g being Element
  of F holds f [*] g = g (*) f;

theorem :: MONOID_0:71
  for F being non empty SubStr of GPFuncs X st id X is Element of
  F holds F is unital & the_unity_wrt the multF of F = id X;

theorem :: MONOID_0:72
  Y c= X implies GPFuncs Y is SubStr of GPFuncs X;

definition
  let X be set;
  func GFuncs X -> strict SubStr of GPFuncs X means
:: MONOID_0:def 40

  the carrier of it = Funcs(X,X);
end;

registration
  let X be set;
  cluster GFuncs X -> unital non empty;
end;

:: corollary
:: GFuncs X is unital associative constituted-Functions;

definition
  let X be set;
  func MFuncs X -> well-unital strict MonoidalExtension of GFuncs X means
:: MONOID_0:def 41
  not contradiction;
end;

:: corollary
:: GFuncs X is constituted-Functions Monoid;

theorem :: MONOID_0:73
  x is Element of GFuncs X iff x is Function of X,X;

theorem :: MONOID_0:74
  the multF of GFuncs X = (X-composition)||Funcs(X,X);

theorem :: MONOID_0:75
  the_unity_wrt the multF of GFuncs X = id X;

theorem :: MONOID_0:76
  the carrier of MFuncs X = Funcs(X,X) & the multF of MFuncs X = (X
  -composition)||Funcs(X,X) & 1.MFuncs X = id X;

definition
  let X be set;
  func GPerms X -> strict non empty SubStr of GFuncs X
  means
:: MONOID_0:def 42

  for f being Element of GFuncs X holds f in the carrier of it iff
  f is Permutation of X;
end;

registration
  let X be set;
  cluster GPerms X -> unital invertible;
end;

:: corollary
:: GPerms X is constituted-Functions Group;

theorem :: MONOID_0:77
  x is Element of GPerms X iff x is Permutation of X;

theorem :: MONOID_0:78
  the_unity_wrt the multF of GPerms X = id X & 1_GPerms X = id X;

theorem :: MONOID_0:79
  for f being Element of GPerms X holds f" = (f qua Function)";

:: 2005.05.13, A.T.

theorem :: MONOID_0:80
  for S being 1-sorted st the carrier of S is functional holds S is
  constituted-Functions;

theorem :: MONOID_0:81
  for G be non empty multMagma, D be non empty Subset of G st
  for x,y being Element of D holds x*y in D
 ex H being strict non empty SubStr of G st the carrier of H = D;

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