:: MONOID_0 semantic presentation

begin

    deffunc H1( 1-sorted ) ->  set = the carrier of $1;

deffunc H2( multMagma ) ->  Element of bool [:[: the carrier of $1, the carrier of $1:], the carrier of $1:] = the multF of $1;

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

definition
let IT be 1-sorted ;
attrIT is constituted-Functions  means :Def1: :: MONOID_0:def 1
 for a being Element of IT holds a is Function;
attrIT is constituted-FinSeqs  means :Def2: :: MONOID_0:def 2
 for a being Element of IT holds a is FinSequence;
end;

:: deftheorem Def1 defines constituted-Functions MONOID_0:def_1_:_
 for IT being 1-sorted holds
( IT is constituted-Functions iff for a being Element of IT holds a is Function );

:: deftheorem Def2 defines constituted-FinSeqs MONOID_0:def_2_:_
 for IT being 1-sorted holds
( IT is constituted-FinSeqs iff for a being Element of IT holds a is FinSequence );

registration
cluster constituted-Functions for 1-sorted ;
existence
 ex b1 being 1-sorted st b1 is constituted-Functions
proof
set f = the Function;
take X = 1-sorted(# { the Function} #); ::_thesis: X is constituted-Functions
let a be Element of X; :: according to MONOID_0:def_1 ::_thesis: a is Function
thus  a is Function ; ::_thesis: verum
end;
cluster constituted-FinSeqs for 1-sorted ;
existence
 ex b1 being 1-sorted st b1 is constituted-FinSeqs
proof
set f = the FinSequence;
take X = 1-sorted(# { the FinSequence} #); ::_thesis: X is constituted-FinSeqs
let a be Element of X; :: according to MONOID_0:def_2 ::_thesis: a is FinSequence
thus  a is FinSequence by TARSKI:def_1; ::_thesis: verum
end;
end;

registration
let X be constituted-Functions 1-sorted ;
cluster  ->  Relation-like Function-like for Element of the carrier of X;
coherence
 for b1 being Element of X holds
( b1 is Function-like & b1 is Relation-like ) by Def1;
end;

registration
cluster constituted-FinSeqs  ->  constituted-Functions for 1-sorted ;
coherence
 for b1 being 1-sorted st b1 is constituted-FinSeqs holds
b1 is constituted-Functions
proof
let X be 1-sorted ; ::_thesis: ( X is constituted-FinSeqs implies X is constituted-Functions )
assume A1: X is constituted-FinSeqs ; ::_thesis: X is constituted-Functions
let a be Element of H1(X); :: according to MONOID_0:def_1 ::_thesis: a is Function
thus  a is Function by A1, Def2; ::_thesis: verum
end;
end;

registration
let X be constituted-FinSeqs 1-sorted ;
cluster  ->  FinSequence-like for Element of the carrier of X;
coherence
 for b1 being Element of X holds b1 is FinSequence-like by Def2;
end;

definition
let D be set ;
let p, q be FinSequence of D;
:: original: ^
redefine funcp ^ q ->  Element of D * ;
coherence
 p ^ q is Element of D *
proof
thus  p ^ q is Element of D * by FINSEQ_1:def_11; ::_thesis: verum
end;
end;

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

definition
let D be non empty set ;
let IT be BinOp of D;
attrIT 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;
attrIT 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;
attrIT is invertible  means :Def5: :: 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 );
attrIT 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;
attrIT 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;
attrIT 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;
attrIT 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;

:: deftheorem  defines left-invertible MONOID_0:def_3_:_
 for D being non empty set
for IT being BinOp of D holds
( IT is left-invertible iff for a, b being Element of D ex l being Element of D st IT . (l,a) = b );

:: deftheorem  defines right-invertible MONOID_0:def_4_:_
 for D being non empty set
for IT being BinOp of D holds
( IT is right-invertible iff for a, b being Element of D ex r being Element of D st IT . (a,r) = b );

:: deftheorem Def5 defines invertible MONOID_0:def_5_:_
 for D being non empty set
for IT being BinOp of D holds
( IT is invertible iff for a, b being Element of D ex r, l being Element of D st
( IT . (a,r) = b & IT . (l,a) = b ) );

:: deftheorem  defines left-cancelable MONOID_0:def_6_:_
 for D being non empty set
for IT being BinOp of D holds
( IT is left-cancelable iff for a, b, c being Element of D st IT . (a,b) = IT . (a,c) holds
b = c );

:: deftheorem  defines right-cancelable MONOID_0:def_7_:_
 for D being non empty set
for IT being BinOp of D holds
( IT is right-cancelable iff for a, b, c being Element of D st IT . (b,a) = IT . (c,a) holds
b = c );

:: deftheorem  defines cancelable MONOID_0:def_8_:_
 for D being non empty set
for IT being BinOp of D holds
( IT is cancelable iff 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 );

:: deftheorem  defines uniquely-decomposable MONOID_0:def_9_:_
 for D being non empty set
for IT being BinOp of D holds
( IT is uniquely-decomposable iff ( 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 ) ) ) );

theorem Th1: :: MONOID_0:1
for D being non empty set
for f being BinOp of D holds
( f is invertible iff ( f is left-invertible & f is right-invertible ) )
proof
let D be non empty set ; ::_thesis: for f being BinOp of D holds
( f is invertible iff ( f is left-invertible & f is right-invertible ) )
let f be BinOp of D; ::_thesis: ( f is invertible iff ( f is left-invertible & f is right-invertible ) )
thus  ( f is invertible implies ( f is left-invertible & f is right-invertible ) ) ::_thesis: ( f is left-invertible & f is right-invertible implies f is invertible )
proof
assume A1: for a, b being Element of D ex r, l being Element of D st
( f . (a,r) = b & f . (l,a) = b ) ; :: according to MONOID_0:def_5 ::_thesis: ( f is left-invertible & f is right-invertible )
now__::_thesis:_for_a,_b_being_Element_of_D_ex_l_being_Element_of_D_st_f_._(l,a)_=_b
let a, b be Element of D; ::_thesis: ex l being Element of D st f . (l,a) = b
consider r, l being Element of D such that
 f . (a,r) = b and
A2: f . (l,a) = b by A1;
take l = l; ::_thesis: f . (l,a) = b
thus  f . (l,a) = b by A2; ::_thesis: verum
end;
hence  for a, b being Element of D ex l being Element of D st f . (l,a) = b ; :: according to MONOID_0:def_3 ::_thesis: f is right-invertible
let a, b be Element of D; :: according to MONOID_0:def_4 ::_thesis: ex r being Element of D st f . (a,r) = b
consider r, l being Element of D such that
A3: f . (a,r) = b and
 f . (l,a) = b by A1;
take  r ; ::_thesis: f . (a,r) = b
thus  f . (a,r) = b by A3; ::_thesis: verum
end;
assume that
A4: for a, b being Element of D ex l being Element of D st f . (l,a) = b and
A5: for a, b being Element of D ex r being Element of D st f . (a,r) = b ; :: according to MONOID_0:def_3,MONOID_0:def_4 ::_thesis: f is invertible
let a, b be Element of D; :: according to MONOID_0:def_5 ::_thesis: ex r, l being Element of D st
( f . (a,r) = b & f . (l,a) = b )
consider l being Element of D such that
A6: f . (l,a) = b by A4;
consider r being Element of D such that
A7: f . (a,r) = b by A5;
take  r ; ::_thesis: ex l being Element of D st
( f . (a,r) = b & f . (l,a) = b )
take  l ; ::_thesis: ( f . (a,r) = b & f . (l,a) = b )
thus  ( f . (a,r) = b & f . (l,a) = b ) by A6, A7; ::_thesis: verum
end;

theorem Th2: :: MONOID_0:2
for D being non empty set
for f being BinOp of D holds
( f is cancelable iff ( f is left-cancelable & f is right-cancelable ) )
proof
let D be non empty set ; ::_thesis: for f being BinOp of D holds
( f is cancelable iff ( f is left-cancelable & f is right-cancelable ) )
let f be BinOp of D; ::_thesis: ( f is cancelable iff ( f is left-cancelable & f is right-cancelable ) )
thus  ( f is cancelable implies ( f is left-cancelable & f is right-cancelable ) ) ::_thesis: ( f is left-cancelable & f is right-cancelable implies f is cancelable )
proof
assume A1: for a, b, c being Element of D st ( f . (a,b) = f . (a,c) or f . (b,a) = f . (c,a) ) holds
b = c ; :: according to MONOID_0:def_8 ::_thesis: ( f is left-cancelable & f is right-cancelable )
hence  for a, b, c being Element of D st f . (a,b) = f . (a,c) holds
b = c ; :: according to MONOID_0:def_6 ::_thesis: f is right-cancelable
thus  for a, b, c being Element of D st f . (b,a) = f . (c,a) holds
b = c by A1; :: according to MONOID_0:def_7 ::_thesis: verum
end;
assume  ( ( for a, b, c being Element of D st f . (a,b) = f . (a,c) holds
b = c ) & ( for a, b, c being Element of D st f . (b,a) = f . (c,a) holds
b = c ) ) ; :: according to MONOID_0:def_6,MONOID_0:def_7 ::_thesis: f is cancelable
hence  for a, b, c being Element of D st ( f . (a,b) = f . (a,c) or f . (b,a) = f . (c,a) ) holds
b = c ; :: according to MONOID_0:def_8 ::_thesis: verum
end;

theorem Th3: :: MONOID_0:3
for x being set
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 & f is cancelable & f is uniquely-decomposable )
proof
let x be set ; ::_thesis: 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 & f is cancelable & f is uniquely-decomposable )
let f be BinOp of {x}; ::_thesis: ( f = (x,x) .--> x & f is having_a_unity & f is commutative & f is associative & f is idempotent & f is invertible & f is cancelable & f is uniquely-decomposable )
reconsider a = x as Element of {x} by TARSKI:def_1;
A1: [:{x},{x}:] = {[x,x]} by ZFMISC_1:29;
A2: now__::_thesis:_for_y_being_set_st_y_in_{[x,x]}_holds_
f_._y_=_((x,x)_.-->_x)_._y
let y be set ; ::_thesis: ( y in {[x,x]} implies f . y = ((x,x) .--> x) . y )
assume A3: y in {[x,x]} ; ::_thesis: f . y = ((x,x) .--> x) . y
then reconsider b = y as Element of [:{x},{x}:] by ZFMISC_1:29;
thus f . y = f . b
.= x by TARSKI:def_1
.= ((x,x) .--> x) . y by A3, FUNCOP_1:7 ; ::_thesis: verum
end;
 ( dom f = [:{x},{x}:] & dom ((x,x) .--> x) = {[x,x]} ) by FUNCT_2:def_1;
hence  f = (x,x) .--> x by A1, A2, FUNCT_1:2; ::_thesis: ( f is having_a_unity & f is commutative & f is associative & f is idempotent & f is invertible & f is cancelable & f is uniquely-decomposable )
A4: now__::_thesis:_for_a,_b_being_Element_of_{x}_holds_a_=_b
let a, b be Element of {x}; ::_thesis: a = b
 a = x by TARSKI:def_1;
hence  a = b by TARSKI:def_1; ::_thesis: verum
end;
then  for b being Element of {x} holds
( f . (a,b) = b & f . (b,a) = b ) ;
then A5: a is_a_unity_wrt f by BINOP_1:3;
hence  ex a being Element of {x} st a is_a_unity_wrt f ; :: according to SETWISEO:def_2 ::_thesis: ( f is commutative & f is associative & f is idempotent & f is invertible & f is cancelable & f is uniquely-decomposable )
thus  for a, b being Element of {x} holds f . (a,b) = f . (b,a) by A4; :: according to BINOP_1:def_2 ::_thesis: ( f is associative & f is idempotent & f is invertible & f is cancelable & f is uniquely-decomposable )
thus  for a, b, c being Element of {x} holds f . (a,(f . (b,c))) = f . ((f . (a,b)),c) by A4; :: according to BINOP_1:def_3 ::_thesis: ( f is idempotent & f is invertible & f is cancelable & f is uniquely-decomposable )
thus  for a being Element of {x} holds f . (a,a) = a by A4; :: according to BINOP_1:def_4 ::_thesis: ( f is invertible & f is cancelable & f is uniquely-decomposable )
thus  for a, b being Element of {x} ex r, l being Element of {x} st
( f . (a,r) = b & f . (l,a) = b ) :: according to MONOID_0:def_5 ::_thesis: ( f is cancelable & f is uniquely-decomposable )
proof
let a, b be Element of {x}; ::_thesis: ex r, l being Element of {x} st
( f . (a,r) = b & f . (l,a) = b )
take  a ; ::_thesis: ex l being Element of {x} st
( f . (a,a) = b & f . (l,a) = b )
take  a ; ::_thesis: ( f . (a,a) = b & f . (a,a) = b )
thus  ( f . (a,a) = b & f . (a,a) = b ) by A4; ::_thesis: verum
end;
thus  for a, b, c being Element of {x} st ( f . (a,b) = f . (a,c) or f . (b,a) = f . (c,a) ) holds
b = c by A4; :: according to MONOID_0:def_8 ::_thesis: f is uniquely-decomposable
thus  ex a being Element of {x} st a is_a_unity_wrt f by A5; :: according to SETWISEO:def_2,MONOID_0:def_9 ::_thesis: for a, b being Element of {x} st f . (a,b) = the_unity_wrt f holds
( a = b & b = the_unity_wrt f )
let a, b be Element of {x}; ::_thesis: ( f . (a,b) = the_unity_wrt f implies ( a = b & b = the_unity_wrt f ) )
thus  ( f . (a,b) = the_unity_wrt f implies ( a = b & b = the_unity_wrt f ) ) by A4; ::_thesis: verum
end;

begin


definition
let IT be non empty multMagma ;
redefine attr IT is unital  means :Def10: :: MONOID_0:def 10
 the multF of IT is having_a_unity ;
compatibility
 ( IT is unital iff the multF of IT is having_a_unity )
proof
thus  ( IT is unital implies the multF of IT is having_a_unity ) ; ::_thesis: ( the multF of IT is having_a_unity implies IT is unital )
given x being Element of IT such that A1: x is_a_unity_wrt the multF of IT ; :: according to SETWISEO:def_2 ::_thesis: IT is unital
take  x ; :: according to GROUP_1:def_1 ::_thesis: for b1 being Element of the carrier of IT holds
( b1 [*] x = b1 & x [*] b1 = b1 )
let h be Element of IT; ::_thesis: ( h [*] x = h & x [*] h = h )
thus  ( h [*] x = h & x [*] h = h ) by A1, BINOP_1:3; ::_thesis: verum
end;
end;

:: deftheorem Def10 defines unital MONOID_0:def_10_:_
 for IT being non empty multMagma holds
( IT is unital iff the multF of IT is having_a_unity );

definition
let G be non empty multMagma ;
redefine attr G is commutative  means :Def11: :: MONOID_0:def 11
 the multF of G is commutative ;
compatibility
 ( G is commutative iff the multF of G is commutative )
proof
thus  ( G is commutative implies the multF of G is commutative ) ::_thesis: ( the multF of G is commutative implies G is commutative )
proof
assume A1: for a, b being Element of G holds a * b = b * a ; :: according to GROUP_1:def_12 ::_thesis: the multF of G is commutative
let a be Element of G; :: according to BINOP_1:def_2 ::_thesis: for b1 being Element of the carrier of G holds the multF of G . (a,b1) = the multF of G . (b1,a)
let b be Element of G; ::_thesis: the multF of G . (a,b) = the multF of G . (b,a)
 ( H2(G) . (a,b) = a * b & H2(G) . (b,a) = b * a ) ;
hence  the multF of G . (a,b) = the multF of G . (b,a) by A1; ::_thesis: verum
end;
assume A2: for a, b being Element of G holds H2(G) . (a,b) = H2(G) . (b,a) ; :: according to BINOP_1:def_2 ::_thesis: G is commutative
let a be Element of G; :: according to GROUP_1:def_12 ::_thesis: for b1 being Element of the carrier of G holds a [*] b1 = b1 [*] a
let b be Element of G; ::_thesis: a [*] b = b [*] a
thus  a [*] b = b [*] a by A2; ::_thesis: verum
end;
redefine attr G is associative  means :Def12: :: MONOID_0:def 12
 the multF of G is associative ;
compatibility
 ( G is associative iff the multF of G is associative )
proof
thus  ( G is associative implies the multF of G is associative ) ; ::_thesis: ( the multF of G is associative implies G is associative )
assume A3: for a, b, c being Element of G holds H2(G) . (a,(H2(G) . (b,c))) = H2(G) . ((H2(G) . (a,b)),c) ; :: according to BINOP_1:def_3 ::_thesis: G is associative
let a be Element of G; :: according to GROUP_1:def_3 ::_thesis: for b1, b2 being Element of the carrier of G holds (a [*] b1) [*] b2 = a [*] (b1 [*] b2)
let b, c be Element of G; ::_thesis: (a [*] b) [*] c = a [*] (b [*] c)
thus  (a [*] b) [*] c = a [*] (b [*] c) by A3; ::_thesis: verum
end;
end;

:: deftheorem Def11 defines commutative MONOID_0:def_11_:_
 for G being non empty multMagma holds
( G is commutative iff the multF of G is commutative );

:: deftheorem Def12 defines associative MONOID_0:def_12_:_
 for G being non empty multMagma holds
( G is associative iff the multF of G is associative );

definition
let IT be non empty multMagma ;
attrIT is idempotent  means :: MONOID_0:def 13
 the multF of IT is idempotent ;
attrIT is left-invertible  means :: MONOID_0:def 14
 the multF of IT is left-invertible ;
attrIT is right-invertible  means :: MONOID_0:def 15
 the multF of IT is right-invertible ;
attrIT is invertible  means :Def16: :: MONOID_0:def 16
 the multF of IT is invertible ;
attrIT is left-cancelable  means :: MONOID_0:def 17
 the multF of IT is left-cancelable ;
attrIT is right-cancelable  means :: MONOID_0:def 18
 the multF of IT is right-cancelable ;
attrIT is cancelable  means :: MONOID_0:def 19
 the multF of IT is cancelable ;
attrIT is uniquely-decomposable  means :Def20: :: MONOID_0:def 20
 the multF of IT is uniquely-decomposable ;
end;

:: deftheorem  defines idempotent MONOID_0:def_13_:_
 for IT being non empty multMagma holds
( IT is idempotent iff the multF of IT is idempotent );

:: deftheorem  defines left-invertible MONOID_0:def_14_:_
 for IT being non empty multMagma holds
( IT is left-invertible iff the multF of IT is left-invertible );

:: deftheorem  defines right-invertible MONOID_0:def_15_:_
 for IT being non empty multMagma holds
( IT is right-invertible iff the multF of IT is right-invertible );

:: deftheorem Def16 defines invertible MONOID_0:def_16_:_
 for IT being non empty multMagma holds
( IT is invertible iff the multF of IT is invertible );

:: deftheorem  defines left-cancelable MONOID_0:def_17_:_
 for IT being non empty multMagma holds
( IT is left-cancelable iff the multF of IT is left-cancelable );

:: deftheorem  defines right-cancelable MONOID_0:def_18_:_
 for IT being non empty multMagma holds
( IT is right-cancelable iff the multF of IT is right-cancelable );

:: deftheorem  defines cancelable MONOID_0:def_19_:_
 for IT being non empty multMagma holds
( IT is cancelable iff the multF of IT is cancelable );

:: deftheorem Def20 defines uniquely-decomposable MONOID_0:def_20_:_
 for IT being non empty multMagma holds
( IT is uniquely-decomposable iff the multF of IT is uniquely-decomposable );

registration
cluster non empty strict unital associative commutative constituted-Functions constituted-FinSeqs idempotent invertible cancelable uniquely-decomposable for multMagma ;
existence
 ex b1 being non empty multMagma st
( b1 is unital & b1 is commutative & b1 is associative & b1 is cancelable & b1 is idempotent & b1 is invertible & b1 is uniquely-decomposable & b1 is constituted-Functions & b1 is constituted-FinSeqs & b1 is strict )
proof
set p = the FinSequence;
set o = the BinOp of { the FinSequence};
take G = multMagma(# { the FinSequence}, the BinOp of { the FinSequence} #); ::_thesis: ( G is unital & G is commutative & G is associative & G is cancelable & G is idempotent & G is invertible & G is uniquely-decomposable & G is constituted-Functions & G is constituted-FinSeqs & G is strict )
thus  ( H2(G) is having_a_unity & H2(G) is commutative & H2(G) is associative & H2(G) is cancelable & H2(G) is idempotent & H2(G) is invertible & H2(G) is uniquely-decomposable ) by Th3; :: according to MONOID_0:def_10,MONOID_0:def_11,MONOID_0:def_12,MONOID_0:def_13,MONOID_0:def_16,MONOID_0:def_19,MONOID_0:def_20 ::_thesis: ( G is constituted-Functions & G is constituted-FinSeqs & G is strict )
thus  ( ( for x being Element of G holds x is Function ) & ( for x being Element of G holds x is FinSequence ) ) by TARSKI:def_1; :: according to MONOID_0:def_1,MONOID_0:def_2 ::_thesis: G is strict
thus  G is strict ; ::_thesis: verum
end;
end;

theorem Th4: :: MONOID_0:4
for G being non empty multMagma st G is unital holds
the_unity_wrt the multF of G is_a_unity_wrt the multF of G
proof
let G be non empty multMagma ; ::_thesis: ( G is unital implies the_unity_wrt the multF of G is_a_unity_wrt the multF of G )
given a being Element of G such that A1: a is_a_unity_wrt H2(G) ; :: according to SETWISEO:def_2,MONOID_0:def_10 ::_thesis: the_unity_wrt the multF of G is_a_unity_wrt the multF of G
thus  the_unity_wrt the multF of G is_a_unity_wrt the multF of G by A1, BINOP_1:def_8; ::_thesis: verum
end;

theorem :: MONOID_0:5
for G being non empty multMagma holds
( G is unital iff for a being Element of G holds
( (the_unity_wrt the multF of G) * a = a & a * (the_unity_wrt the multF of G) = a ) )
proof
let G be non empty multMagma ; ::_thesis: ( G is unital iff for a being Element of G holds
( (the_unity_wrt the multF of G) * a = a & a * (the_unity_wrt the multF of G) = a ) )
set u = the_unity_wrt the multF of G;
thus  ( G is unital implies for b being Element of G holds
( (the_unity_wrt the multF of G) * b = b & b * (the_unity_wrt the multF of G) = b ) ) ::_thesis: ( ( for a being Element of G holds
( (the_unity_wrt the multF of G) * a = a & a * (the_unity_wrt the multF of G) = a ) ) implies G is unital )
proof
given a being Element of G such that A1: a is_a_unity_wrt H2(G) ; :: according to SETWISEO:def_2,MONOID_0:def_10 ::_thesis: for b being Element of G holds
( (the_unity_wrt the multF of G) * b = b & b * (the_unity_wrt the multF of G) = b )
let b be Element of G; ::_thesis: ( (the_unity_wrt the multF of G) * b = b & b * (the_unity_wrt the multF of G) = b )
 the_unity_wrt the multF of G = a by A1, BINOP_1:def_8;
hence  ( (the_unity_wrt the multF of G) * b = b & b * (the_unity_wrt the multF of G) = b ) by A1, BINOP_1:3; ::_thesis: verum
end;
assume A2: for b being Element of G holds
( (the_unity_wrt the multF of G) * b = b & b * (the_unity_wrt the multF of G) = b ) ; ::_thesis: G is unital
take a = the_unity_wrt the multF of G; :: according to SETWISEO:def_2,MONOID_0:def_10 ::_thesis: a is_a_unity_wrt the multF of G
thus  a is_a_left_unity_wrt the multF of G :: according to BINOP_1:def_7 ::_thesis: a is_a_right_unity_wrt the multF of G
proof
let b be Element of G; :: according to BINOP_1:def_16 ::_thesis: the multF of G . (a,b) = b
 a * b = b by A2;
hence  the multF of G . (a,b) = b ; ::_thesis: verum
end;
let b be Element of G; :: according to BINOP_1:def_17 ::_thesis: the multF of G . (b,a) = b
 b * a = b by A2;
hence  the multF of G . (b,a) = b ; ::_thesis: verum
end;

theorem Th6: :: MONOID_0:6
for G being non empty multMagma holds
( G is unital iff ex a being Element of G st
for b being Element of G holds
( a * b = b & b * a = b ) )
proof
let G be non empty multMagma ; ::_thesis: ( G is unital iff ex a being Element of G st
for b being Element of G holds
( a * b = b & b * a = b ) )
thus  ( G is unital implies ex a being Element of G st
for b being Element of G holds
( a * b = b & b * a = b ) ) ::_thesis: ( ex a being Element of G st
for b being Element of G holds
( a * b = b & b * a = b ) implies G is unital )
proof
given a being Element of G such that A1: a is_a_unity_wrt the multF of G ; :: according to SETWISEO:def_2,MONOID_0:def_10 ::_thesis: ex a being Element of G st
for b being Element of G holds
( a * b = b & b * a = b )
take  a ; ::_thesis: for b being Element of G holds
( a * b = b & b * a = b )
let b be Element of G; ::_thesis: ( a * b = b & b * a = b )
 ( a is_a_left_unity_wrt H2(G) & a is_a_right_unity_wrt the multF of G ) by A1, BINOP_1:def_7;
hence  ( a * b = b & b * a = b ) by BINOP_1:def_5, BINOP_1:def_6; ::_thesis: verum
end;
given a being Element of G such that A2: for b being Element of G holds
( a * b = b & b * a = b ) ; ::_thesis: G is unital
take  a ; :: according to SETWISEO:def_2,MONOID_0:def_10 ::_thesis: a is_a_unity_wrt the multF of G
thus  a is_a_left_unity_wrt the multF of G :: according to BINOP_1:def_7 ::_thesis: a is_a_right_unity_wrt the multF of G
proof
let b be Element of G; :: according to BINOP_1:def_16 ::_thesis: the multF of G . (a,b) = b
 a * b = b by A2;
hence  the multF of G . (a,b) = b ; ::_thesis: verum
end;
let b be Element of G; :: according to BINOP_1:def_17 ::_thesis: the multF of G . (b,a) = b
 b * a = b by A2;
hence  the multF of G . (b,a) = b ; ::_thesis: verum
end;

Lm1:  for G being non empty multMagma holds
( G is commutative iff for a, b being Element of G holds a * b = b * a )
proof
let G be non empty multMagma ; ::_thesis: ( G is commutative iff for a, b being Element of G holds a * b = b * a )
thus  ( G is commutative implies for a, b being Element of G holds a * b = b * a ) ::_thesis: ( ( for a, b being Element of G holds a * b = b * a ) implies G is commutative )
proof
assume A1: for a, b being Element of G holds H2(G) . (a,b) = H2(G) . (b,a) ; :: according to BINOP_1:def_2,MONOID_0:def_11 ::_thesis: for a, b being Element of G holds a * b = b * a
let a, b be Element of G; ::_thesis: a * b = b * a
thus  a * b = b * a by A1; ::_thesis: verum
end;
assume A2: for a, b being Element of G holds a * b = b * a ; ::_thesis: G is commutative
let a be Element of G; :: according to BINOP_1:def_2,MONOID_0:def_11 ::_thesis: for b1 being Element of the carrier of G holds the multF of G . (a,b1) = the multF of G . (b1,a)
let b be Element of G; ::_thesis: the multF of G . (a,b) = the multF of G . (b,a)
 ( H2(G) . (a,b) = a * b & H2(G) . (b,a) = b * a ) ;
hence  the multF of G . (a,b) = the multF of G . (b,a) by A2; ::_thesis: verum
end;

Lm2:  for G being non empty multMagma holds
( G is associative iff for a, b, c being Element of G holds (a * b) * c = a * (b * c) )
proof
let G be non empty multMagma ; ::_thesis: ( G is associative iff for a, b, c being Element of G holds (a * b) * c = a * (b * c) )
thus  ( G is associative implies for a, b, c being Element of G holds (a * b) * c = a * (b * c) ) ::_thesis: ( ( for a, b, c being Element of G holds (a * b) * c = a * (b * c) ) implies G is associative )
proof
assume A1: for a, b, c being Element of G holds H2(G) . (a,(H2(G) . (b,c))) = H2(G) . ((H2(G) . (a,b)),c) ; :: according to BINOP_1:def_3,MONOID_0:def_12 ::_thesis: for a, b, c being Element of G holds (a * b) * c = a * (b * c)
let a, b, c be Element of G; ::_thesis: (a * b) * c = a * (b * c)
thus  (a * b) * c = a * (b * c) by A1; ::_thesis: verum
end;
assume A2: for a, b, c being Element of G holds (a * b) * c = a * (b * c) ; ::_thesis: G is associative
let a be Element of G; :: according to BINOP_1:def_3,MONOID_0:def_12 ::_thesis: for b1, b2 being Element of the carrier of G holds the multF of G . (a,( the multF of G . (b1,b2))) = the multF of G . (( the multF of G . (a,b1)),b2)
let b, c be Element of G; ::_thesis: the multF of G . (a,( the multF of G . (b,c))) = the multF of G . (( the multF of G . (a,b)),c)
 ( H2(G) . ((a * b),c) = (a * b) * c & H2(G) . (a,(b * c)) = a * (b * c) ) ;
hence  the multF of G . (a,( the multF of G . (b,c))) = the multF of G . (( the multF of G . (a,b)),c) by A2; ::_thesis: verum
end;

theorem Th7: :: MONOID_0:7
for G being non empty multMagma holds
( G is idempotent iff for a being Element of G holds a * a = a )
proof
let G be non empty multMagma ; ::_thesis: ( G is idempotent iff for a being Element of G holds a * a = a )
thus  ( G is idempotent implies for a being Element of G holds a * a = a ) ::_thesis: ( ( for a being Element of G holds a * a = a ) implies G is idempotent )
proof
assume A1: for a being Element of G holds H2(G) . (a,a) = a ; :: according to BINOP_1:def_4,MONOID_0:def_13 ::_thesis: for a being Element of G holds a * a = a
let a be Element of G; ::_thesis: a * a = a
thus  a * a = a by A1; ::_thesis: verum
end;
assume A2: for a being Element of G holds a * a = a ; ::_thesis: G is idempotent
let a be Element of G; :: according to BINOP_1:def_4,MONOID_0:def_13 ::_thesis: the multF of G . (a,a) = a
thus H2(G) . (a,a) = a * a
.= a by A2 ; ::_thesis: verum
end;

theorem :: MONOID_0:8
for G being non empty multMagma holds
( G is left-invertible iff for a, b being Element of G ex l being Element of G st l * a = b )
proof
let G be non empty multMagma ; ::_thesis: ( G is left-invertible iff for a, b being Element of G ex l being Element of G st l * a = b )
thus  ( G is left-invertible implies for a, b being Element of G ex l being Element of G st l * a = b ) ::_thesis: ( ( for a, b being Element of G ex l being Element of G st l * a = b ) implies G is left-invertible )
proof
assume A1: for a, b being Element of G ex l being Element of G st H2(G) . (l,a) = b ; :: according to MONOID_0:def_3,MONOID_0:def_14 ::_thesis: for a, b being Element of G ex l being Element of G st l * a = b
let a, b be Element of G; ::_thesis: ex l being Element of G st l * a = b
consider l being Element of G such that
A2: H2(G) . (l,a) = b by A1;
take  l ; ::_thesis: l * a = b
thus  l * a = b by A2; ::_thesis: verum
end;
assume A3: for a, b being Element of G ex l being Element of G st l * a = b ; ::_thesis: G is left-invertible
let a be Element of G; :: according to MONOID_0:def_3,MONOID_0:def_14 ::_thesis: for b being Element of the carrier of G ex l being Element of the carrier of G st the multF of G . (l,a) = b
let b be Element of G; ::_thesis: ex l being Element of the carrier of G st the multF of G . (l,a) = b
consider l being Element of G such that
A4: l * a = b by A3;
take  l ; ::_thesis: the multF of G . (l,a) = b
thus  the multF of G . (l,a) = b by A4; ::_thesis: verum
end;

theorem :: MONOID_0:9
for G being non empty multMagma holds
( G is right-invertible iff for a, b being Element of G ex r being Element of G st a * r = b )
proof
let G be non empty multMagma ; ::_thesis: ( G is right-invertible iff for a, b being Element of G ex r being Element of G st a * r = b )
thus  ( G is right-invertible implies for a, b being Element of G ex r being Element of G st a * r = b ) ::_thesis: ( ( for a, b being Element of G ex r being Element of G st a * r = b ) implies G is right-invertible )
proof
assume A1: for a, b being Element of G ex r being Element of G st H2(G) . (a,r) = b ; :: according to MONOID_0:def_4,MONOID_0:def_15 ::_thesis: for a, b being Element of G ex r being Element of G st a * r = b
let a, b be Element of G; ::_thesis: ex r being Element of G st a * r = b
consider r being Element of G such that
A2: H2(G) . (a,r) = b by A1;
take  r ; ::_thesis: a * r = b
thus  a * r = b by A2; ::_thesis: verum
end;
assume A3: for a, b being Element of G ex r being Element of G st a * r = b ; ::_thesis: G is right-invertible
let a be Element of G; :: according to MONOID_0:def_4,MONOID_0:def_15 ::_thesis: for b being Element of the carrier of G ex r being Element of the carrier of G st the multF of G . (a,r) = b
let b be Element of G; ::_thesis: ex r being Element of the carrier of G st the multF of G . (a,r) = b
consider r being Element of G such that
A4: a * r = b by A3;
take  r ; ::_thesis: the multF of G . (a,r) = b
thus  the multF of G . (a,r) = b by A4; ::_thesis: verum
end;

theorem Th10: :: MONOID_0:10
for G being non empty multMagma holds
( G is invertible iff for a, b being Element of G ex r, l being Element of G st
( a * r = b & l * a = b ) )
proof
let G be non empty multMagma ; ::_thesis: ( G is invertible iff for a, b being Element of G ex r, l being Element of G st
( a * r = b & l * a = b ) )
thus  ( G is invertible implies for a, b being Element of G ex r, l being Element of G st
( a * r = b & l * a = b ) ) ::_thesis: ( ( for a, b being Element of G ex r, l being Element of G st
( a * r = b & l * a = b ) ) implies G is invertible )
proof
assume A1: for a, b being Element of G ex r, l being Element of G st
( H2(G) . (a,r) = b & H2(G) . (l,a) = b ) ; :: according to MONOID_0:def_5,MONOID_0:def_16 ::_thesis: for a, b being Element of G ex r, l being Element of G st
( a * r = b & l * a = b )
let a, b be Element of G; ::_thesis: ex r, l being Element of G st
( a * r = b & l * a = b )
consider r, l being Element of G such that
A2: ( H2(G) . (a,r) = b & H2(G) . (l,a) = b ) by A1;
take  r ; ::_thesis: ex l being Element of G st
( a * r = b & l * a = b )
take  l ; ::_thesis: ( a * r = b & l * a = b )
thus  ( a * r = b & l * a = b ) by A2; ::_thesis: verum
end;
assume A3: for a, b being Element of G ex r, l being Element of G st
( a * r = b & l * a = b ) ; ::_thesis: G is invertible
let a be Element of G; :: according to MONOID_0:def_5,MONOID_0:def_16 ::_thesis: for b being Element of the carrier of G ex r, l being Element of the carrier of G st
( the multF of G . (a,r) = b & the multF of G . (l,a) = b )
let b be Element of G; ::_thesis: ex r, l being Element of the carrier of G st
( the multF of G . (a,r) = b & the multF of G . (l,a) = b )
consider r, l being Element of G such that
A4: ( a * r = b & l * a = b ) by A3;
take  r ; ::_thesis: ex l being Element of the carrier of G st
( the multF of G . (a,r) = b & the multF of G . (l,a) = b )
take  l ; ::_thesis: ( the multF of G . (a,r) = b & the multF of G . (l,a) = b )
thus  ( the multF of G . (a,r) = b & the multF of G . (l,a) = b ) by A4; ::_thesis: verum
end;

theorem :: MONOID_0:11
for G being non empty multMagma holds
( G is left-cancelable iff for a, b, c being Element of G st a * b = a * c holds
b = c )
proof
let G be non empty multMagma ; ::_thesis: ( G is left-cancelable iff for a, b, c being Element of G st a * b = a * c holds
b = c )
thus  ( G is left-cancelable implies for a, b, c being Element of G st a * b = a * c holds
b = c ) ::_thesis: ( ( for a, b, c being Element of G st a * b = a * c holds
b = c ) implies G is left-cancelable )
proof
assume A1: for a, b, c being Element of G st H2(G) . (a,b) = H2(G) . (a,c) holds
b = c ; :: according to MONOID_0:def_6,MONOID_0:def_17 ::_thesis: for a, b, c being Element of G st a * b = a * c holds
b = c
let a, b, c be Element of G; ::_thesis: ( a * b = a * c implies b = c )
thus  ( a * b = a * c implies b = c ) by A1; ::_thesis: verum
end;
assume A2: for a, b, c being Element of G st a * b = a * c holds
b = c ; ::_thesis: G is left-cancelable
let a be Element of G; :: according to MONOID_0:def_6,MONOID_0:def_17 ::_thesis: for b, c being Element of the carrier of G st the multF of G . (a,b) = the multF of G . (a,c) holds
b = c
let b, c be Element of G; ::_thesis: ( the multF of G . (a,b) = the multF of G . (a,c) implies b = c )
 ( a * b = H2(G) . (a,b) & a * c = H2(G) . (a,c) ) ;
hence  ( the multF of G . (a,b) = the multF of G . (a,c) implies b = c ) by A2; ::_thesis: verum
end;

theorem :: MONOID_0:12
for G being non empty multMagma holds
( G is right-cancelable iff for a, b, c being Element of G st b * a = c * a holds
b = c )
proof
let G be non empty multMagma ; ::_thesis: ( G is right-cancelable iff for a, b, c being Element of G st b * a = c * a holds
b = c )
thus  ( G is right-cancelable implies for a, b, c being Element of G st b * a = c * a holds
b = c ) ::_thesis: ( ( for a, b, c being Element of G st b * a = c * a holds
b = c ) implies G is right-cancelable )
proof
assume A1: for a, b, c being Element of G st H2(G) . (b,a) = H2(G) . (c,a) holds
b = c ; :: according to MONOID_0:def_7,MONOID_0:def_18 ::_thesis: for a, b, c being Element of G st b * a = c * a holds
b = c
let a, b, c be Element of G; ::_thesis: ( b * a = c * a implies b = c )
thus  ( b * a = c * a implies b = c ) by A1; ::_thesis: verum
end;
assume A2: for a, b, c being Element of G st b * a = c * a holds
b = c ; ::_thesis: G is right-cancelable
let a be Element of G; :: according to MONOID_0:def_7,MONOID_0:def_18 ::_thesis: for b, c being Element of the carrier of G st the multF of G . (b,a) = the multF of G . (c,a) holds
b = c
let b, c be Element of G; ::_thesis: ( the multF of G . (b,a) = the multF of G . (c,a) implies b = c )
 ( b * a = H2(G) . (b,a) & c * a = H2(G) . (c,a) ) ;
hence  ( the multF of G . (b,a) = the multF of G . (c,a) implies b = c ) by A2; ::_thesis: verum
end;

theorem Th13: :: MONOID_0:13
for G being non empty multMagma holds
( G is cancelable iff for a, b, c being Element of G st ( a * b = a * c or b * a = c * a ) holds
b = c )
proof
let G be non empty multMagma ; ::_thesis: ( G is cancelable iff for a, b, c being Element of G st ( a * b = a * c or b * a = c * a ) holds
b = c )
thus  ( G is cancelable implies for a, b, c being Element of G st ( a * b = a * c or b * a = c * a ) holds
b = c ) ::_thesis: ( ( for a, b, c being Element of G st ( a * b = a * c or b * a = c * a ) holds
b = c ) implies G is cancelable )
proof
assume A1: for a, b, c being Element of G st ( H2(G) . (a,b) = H2(G) . (a,c) or H2(G) . (b,a) = H2(G) . (c,a) ) holds
b = c ; :: according to MONOID_0:def_8,MONOID_0:def_19 ::_thesis: for a, b, c being Element of G st ( a * b = a * c or b * a = c * a ) holds
b = c
let a, b, c be Element of G; ::_thesis: ( ( a * b = a * c or b * a = c * a ) implies b = c )
thus  ( ( a * b = a * c or b * a = c * a ) implies b = c ) by A1; ::_thesis: verum
end;
assume A2: for a, b, c being Element of G st ( a * b = a * c or b * a = c * a ) holds
b = c ; ::_thesis: G is cancelable
let a be Element of G; :: according to MONOID_0:def_8,MONOID_0:def_19 ::_thesis: for b, c being Element of the carrier of G st ( the multF of G . (a,b) = the multF of G . (a,c) or the multF of G . (b,a) = the multF of G . (c,a) ) holds
b = c
let b, c be Element of G; ::_thesis: ( ( the multF of G . (a,b) = the multF of G . (a,c) or the multF of G . (b,a) = the multF of G . (c,a) ) implies b = c )
A3: ( b * a = H2(G) . (b,a) & c * a = H2(G) . (c,a) ) ;
 ( a * b = H2(G) . (a,b) & a * c = H2(G) . (a,c) ) ;
hence  ( ( the multF of G . (a,b) = the multF of G . (a,c) or the multF of G . (b,a) = the multF of G . (c,a) ) implies b = c ) by A2, A3; ::_thesis: verum
end;

theorem Th14: :: MONOID_0:14
for G being non empty multMagma holds
( 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 ) ) ) )
proof
let G be non empty multMagma ; ::_thesis: ( 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 ) ) ) )
thus  ( G is uniquely-decomposable implies ( H2(G) is having_a_unity & ( for a, b being Element of G st a * b = the_unity_wrt H2(G) holds
( a = b & b = the_unity_wrt the multF of G ) ) ) ) ::_thesis: ( 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 ) ) implies G is uniquely-decomposable )
proof
assume that
A1: H2(G) is having_a_unity and
A2: for a, b being Element of G st H2(G) . (a,b) = the_unity_wrt H2(G) holds
( a = b & b = the_unity_wrt H2(G) ) ; :: according to MONOID_0:def_9,MONOID_0:def_20 ::_thesis: ( H2(G) is having_a_unity & ( for a, b being Element of G st a * b = the_unity_wrt H2(G) holds
( a = b & b = the_unity_wrt the multF of G ) ) )
thus  H2(G) is having_a_unity by A1; ::_thesis: for a, b being Element of G st a * b = the_unity_wrt H2(G) holds
( a = b & b = the_unity_wrt the multF of G )
let a, b be Element of G; ::_thesis: ( a * b = the_unity_wrt H2(G) implies ( a = b & b = the_unity_wrt the multF of G ) )
thus  ( a * b = the_unity_wrt H2(G) implies ( a = b & b = the_unity_wrt the multF of G ) ) by A2; ::_thesis: verum
end;
assume that
A3: H2(G) is having_a_unity and
A4: for a, b being Element of G st a * b = the_unity_wrt H2(G) holds
( a = b & b = the_unity_wrt H2(G) ) ; ::_thesis: G is uniquely-decomposable
thus  H2(G) is having_a_unity by A3; :: according to MONOID_0:def_9,MONOID_0:def_20 ::_thesis: for a, b being Element of the carrier of G st the multF of G . (a,b) = the_unity_wrt the multF of G holds
( a = b & b = the_unity_wrt the multF of G )
let a, b be Element of G; ::_thesis: ( the multF of G . (a,b) = the_unity_wrt the multF of G implies ( a = b & b = the_unity_wrt the multF of G ) )
 a * b = H2(G) . (a,b) ;
hence  ( the multF of G . (a,b) = the_unity_wrt the multF of G implies ( a = b & b = the_unity_wrt the multF of G ) ) by A4; ::_thesis: verum
end;

theorem Th15: :: MONOID_0:15
for G being non empty multMagma st G is associative holds
( G is invertible iff ( G is unital & the multF of G is having_an_inverseOp ) )
proof
let G be non empty multMagma ; ::_thesis: ( G is associative implies ( G is invertible iff ( G is unital & the multF of G is having_an_inverseOp ) ) )
assume A1: G is associative ; ::_thesis: ( G is invertible iff ( G is unital & the multF of G is having_an_inverseOp ) )
thus  ( G is invertible implies ( G is unital & H2(G) is having_an_inverseOp ) ) ::_thesis: ( G is unital & the multF of G is having_an_inverseOp implies G is invertible )
proof
set e = the Element of G;
assume A2: G is invertible ; ::_thesis: ( G is unital & H2(G) is having_an_inverseOp )
then consider x, y being Element of G such that
A3: the Element of G * x = the Element of G and
A4: y * the Element of G = the Element of G by Th10;
A5: now__::_thesis:_for_a_being_Element_of_G_holds_
(_y_*_a_=_a_&_a_*_x_=_a_)
let a be Element of G; ::_thesis: ( y * a = a & a * x = a )
A6: ex b, c being Element of G st
( the Element of G * b = a & c * the Element of G = a ) by A2, Th10;
hence  y * a = a by A1, A4, Lm2; ::_thesis: a * x = a
thus  a * x = a by A1, A3, A6, Lm2; ::_thesis: verum
end;
then A7: ( y * x = x & y * x = y ) ;
hence  G is unital by A5, Th6; ::_thesis: H2(G) is having_an_inverseOp
defpred S1[ Element of G, Element of G] means ( $1 * $2 = x & $2 * $1 = x );
A8: for a being Element of G ex b being Element of G st S1[a,b]
proof
let a be Element of G; ::_thesis: ex b being Element of G st S1[a,b]
consider b, c being Element of G such that
A9: ( a * b = x & c * a = x ) by A2, Th10;
take  b ; ::_thesis: S1[a,b]
 ( c * (a * b) = (c * a) * b & x * b = b ) by A1, A5, A7, Lm2;
hence  S1[a,b] by A5, A9; ::_thesis: verum
end;
 ex f being Function of the carrier of G, the carrier of G st
for x being Element of G holds S1[x,f . x] from FUNCT_2:sch_3(A8);
then consider u being UnOp of H1(G) such that
A10: for a being Element of G holds S1[a,u . a] ;
now__::_thesis:_for_b_being_Element_of_G_holds_
(_H2(G)_._(x,b)_=_b_&_H2(G)_._(b,x)_=_b_)
let b be Element of G; ::_thesis: ( H2(G) . (x,b) = b & H2(G) . (b,x) = b )
 ( x * b = H2(G) . (x,b) & b * x = H2(G) . (b,x) ) ;
hence  ( H2(G) . (x,b) = b & H2(G) . (b,x) = b ) by A5, A7; ::_thesis: verum
end;
then  x is_a_unity_wrt H2(G) by BINOP_1:3;
then A11: x = the_unity_wrt H2(G) by BINOP_1:def_8;
take  u ; :: according to FINSEQOP:def_2 ::_thesis: u is_an_inverseOp_wrt H2(G)
let a be Element of G; :: according to FINSEQOP:def_1 ::_thesis: ( H2(G) . (a,(u . a)) = the_unity_wrt H2(G) & H2(G) . ((u . a),a) = the_unity_wrt H2(G) )
 ( H2(G) . (a,(u . a)) = a * (u . a) & H2(G) . ((u . a),a) = (u . a) * a ) ;
hence  ( H2(G) . (a,(u . a)) = the_unity_wrt H2(G) & H2(G) . ((u . a),a) = the_unity_wrt H2(G) ) by A10, A11; ::_thesis: verum
end;
assume A12: H2(G) is having_a_unity ; :: according to MONOID_0:def_10 ::_thesis: ( not the multF of G is having_an_inverseOp or G is invertible )
given u being UnOp of H1(G) such that A13: u is_an_inverseOp_wrt H2(G) ; :: according to FINSEQOP:def_2 ::_thesis: G is invertible
let a be Element of G; :: according to MONOID_0:def_5,MONOID_0:def_16 ::_thesis: for b being Element of the carrier of G ex r, l being Element of the carrier of G st
( the multF of G . (a,r) = b & the multF of G . (l,a) = b )
let c be Element of G; ::_thesis: ex r, l being Element of the carrier of G st
( the multF of G . (a,r) = c & the multF of G . (l,a) = c )
take l = (u . a) * c; ::_thesis: ex l being Element of the carrier of G st
( the multF of G . (a,l) = c & the multF of G . (l,a) = c )
take r = c * (u . a); ::_thesis: ( the multF of G . (a,l) = c & the multF of G . (r,a) = c )
thus H2(G) . (a,l) = a * l
.= (a * (u . a)) * c by A1, Lm2
.= H2(G) . ((the_unity_wrt H2(G)),c) by A13, FINSEQOP:def_1
.= c by A12, SETWISEO:15 ; ::_thesis: the multF of G . (r,a) = c
thus H2(G) . (r,a) = r * a
.= c * ((u . a) * a) by A1, Lm2
.= H2(G) . (c,(the_unity_wrt H2(G))) by A13, FINSEQOP:def_1
.= c by A12, SETWISEO:15 ; ::_thesis: verum
end;

Lm3:  for G being non empty multMagma holds
( G is invertible iff ( G is left-invertible & G is right-invertible ) )
proof
let G be non empty multMagma ; ::_thesis: ( G is invertible iff ( G is left-invertible & G is right-invertible ) )
thus  ( G is invertible implies ( G is left-invertible & G is right-invertible ) ) ::_thesis: ( G is left-invertible & G is right-invertible implies G is invertible )
proof
assume  H2(G) is invertible ; :: according to MONOID_0:def_16 ::_thesis: ( G is left-invertible & G is right-invertible )
hence  ( H2(G) is left-invertible & H2(G) is right-invertible ) by Th1; :: according to MONOID_0:def_14,MONOID_0:def_15 ::_thesis: verum
end;
assume  ( H2(G) is left-invertible & H2(G) is right-invertible ) ; :: according to MONOID_0:def_14,MONOID_0:def_15 ::_thesis: G is invertible
hence  H2(G) is invertible by Th1; :: according to MONOID_0:def_16 ::_thesis: verum
end;

Lm4:  for G being non empty multMagma holds
( G is cancelable iff ( G is left-cancelable & G is right-cancelable ) )
proof
let G be non empty multMagma ; ::_thesis: ( G is cancelable iff ( G is left-cancelable & G is right-cancelable ) )
thus  ( G is cancelable implies ( G is left-cancelable & G is right-cancelable ) ) ::_thesis: ( G is left-cancelable & G is right-cancelable implies G is cancelable )
proof
assume  H2(G) is cancelable ; :: according to MONOID_0:def_19 ::_thesis: ( G is left-cancelable & G is right-cancelable )
hence  ( H2(G) is left-cancelable & H2(G) is right-cancelable ) by Th2; :: according to MONOID_0:def_17,MONOID_0:def_18 ::_thesis: verum
end;
assume  ( H2(G) is left-cancelable & H2(G) is right-cancelable ) ; :: according to MONOID_0:def_17,MONOID_0:def_18 ::_thesis: G is cancelable
hence  H2(G) is cancelable by Th2; :: according to MONOID_0:def_19 ::_thesis: verum
end;

Lm5:  for G being non empty multMagma st G is associative & G is invertible holds
G is Group-like
proof
let G be non empty multMagma ; ::_thesis: ( G is associative & G is invertible implies G is Group-like )
assume A1: ( G is associative & G is invertible ) ; ::_thesis: G is Group-like
then  G is unital by Th15;
then consider a being Element of G such that
A2: for b being Element of G holds
( a * b = b & b * a = b ) by Th6;
take  a ; :: according to GROUP_1:def_2 ::_thesis: for b1 being Element of the carrier of G holds
( b1 [*] a = b1 & a [*] b1 = b1 & ex b2 being Element of the carrier of G st
( b1 [*] b2 = a & b2 [*] b1 = a ) )
let b be Element of G; ::_thesis: ( b [*] a = b & a [*] b = b & ex b1 being Element of the carrier of G st
( b [*] b1 = a & b1 [*] b = a ) )
thus  ( b * a = b & a * b = b ) by A2; ::_thesis: ex b1 being Element of the carrier of G st
( b [*] b1 = a & b1 [*] b = a )
 H2(G) is invertible by A1, Def16;
then consider l, r being Element of G such that
A3: ( H2(G) . (b,l) = a & H2(G) . (r,b) = a ) by Def5;
take  l ; ::_thesis: ( b [*] l = a & l [*] b = a )
A4: ( b * l = a & r * b = a ) by A3;
r = r * a by A2
.= a * l by A1, A4, Lm2
.= l by A2 ;
hence  ( b [*] l = a & l [*] b = a ) by A3; ::_thesis: verum
end;

registration
cluster non empty Group-like associative  ->  non empty invertible for multMagma ;
coherence
 for b1 being non empty multMagma st b1 is associative & b1 is Group-like holds
b1 is invertible
proof
let G be non empty multMagma ; ::_thesis: ( G is associative & G is Group-like implies G is invertible )
assume  ( G is associative & G is Group-like ) ; ::_thesis: G is invertible
then reconsider G = G as non empty Group-like associative multMagma ;
 H2(G) is having_an_inverseOp ;
hence  G is invertible by Th15; ::_thesis: verum
end;
cluster non empty associative invertible  ->  non empty Group-like for multMagma ;
coherence
 for b1 being non empty multMagma st b1 is associative & b1 is invertible holds
b1 is Group-like by Lm5;
end;

registration
cluster non empty invertible  ->  non empty left-invertible right-invertible for multMagma ;
coherence
 for b1 being non empty multMagma st b1 is invertible holds
( b1 is left-invertible & b1 is right-invertible ) by Lm3;
cluster non empty left-invertible right-invertible  ->  non empty invertible for multMagma ;
coherence
 for b1 being non empty multMagma st b1 is left-invertible & b1 is right-invertible holds
b1 is invertible by Lm3;
cluster non empty cancelable  ->  non empty left-cancelable right-cancelable for multMagma ;
coherence
 for b1 being non empty multMagma st b1 is cancelable holds
( b1 is left-cancelable & b1 is right-cancelable ) by Lm4;
cluster non empty left-cancelable right-cancelable  ->  non empty cancelable for multMagma ;
coherence
 for b1 being non empty multMagma st b1 is left-cancelable & b1 is right-cancelable holds
b1 is cancelable by Lm4;
cluster non empty associative invertible  ->  non empty unital cancelable for multMagma ;
coherence
 for b1 being non empty multMagma st b1 is associative & b1 is invertible holds
( b1 is unital & b1 is cancelable )
proof
let G be non empty multMagma ; ::_thesis: ( G is associative & G is invertible implies ( G is unital & G is cancelable ) )
assume  ( G is associative & G is invertible ) ; ::_thesis: ( G is unital & G is cancelable )
then reconsider G = G as non empty associative invertible multMagma ;
 for a, b, c being Element of G st ( a * b = a * c or b * a = c * a ) holds
b = c by GROUP_1:6;
hence  ( G is unital & G is cancelable ) by Th13; ::_thesis: verum
end;
end;

begin

deffunc H3( multLoopStr ) ->  Element of the carrier of $1 = 1. $1;

definition
let IT be non empty multLoopStr ;
redefine attr IT is well-unital  means :Def21: :: MONOID_0:def 21
 1. IT is_a_unity_wrt the multF of IT;
compatibility
 ( IT is well-unital iff 1. IT is_a_unity_wrt the multF of IT )
proof
thus  ( IT is well-unital implies 1. IT is_a_unity_wrt the multF of IT ) ::_thesis: ( 1. IT is_a_unity_wrt the multF of IT implies IT is well-unital )
proof
assume A1: IT is well-unital ; ::_thesis: 1. IT is_a_unity_wrt the multF of IT
thus  1. IT is_a_left_unity_wrt the multF of IT :: according to BINOP_1:def_7 ::_thesis: 1. IT is_a_right_unity_wrt the multF of IT
proof
let a be Element of IT; :: according to BINOP_1:def_16 ::_thesis: the multF of IT . ((1. IT),a) = a
thus  the multF of IT . ((1. IT),a) = (1. IT) * a
.= a by A1, VECTSP_1:def_6 ; ::_thesis: verum
end;
let a be Element of IT; :: according to BINOP_1:def_17 ::_thesis: the multF of IT . (a,(1. IT)) = a
thus  the multF of IT . (a,(1. IT)) = a * (1. IT)
.= a by A1, VECTSP_1:def_6 ; ::_thesis: verum
end;
assume A2: 1. IT is_a_unity_wrt the multF of IT ; ::_thesis: IT is well-unital
let x be Element of IT; :: according to VECTSP_1:def_6 ::_thesis: ( x [*] (1. IT) = x & (1. IT) [*] x = x )
 1. IT is_a_right_unity_wrt the multF of IT by A2, BINOP_1:def_7;
hence  x * (1. IT) = x by BINOP_1:def_6; ::_thesis: (1. IT) [*] x = x
 1. IT is_a_left_unity_wrt the multF of IT by A2, BINOP_1:def_7;
hence  (1. IT) [*] x = x by BINOP_1:def_5; ::_thesis: verum
end;
end;

:: deftheorem Def21 defines well-unital MONOID_0:def_21_:_
 for IT being non empty multLoopStr holds
( IT is well-unital iff 1. IT is_a_unity_wrt the multF of IT );

theorem Th16: :: MONOID_0:16
for M being non empty multLoopStr holds
( M is well-unital iff for a being Element of M holds
( (1. M) * a = a & a * (1. M) = a ) )
proof
let M be non empty multLoopStr ; ::_thesis: ( M is well-unital iff for a being Element of M holds
( (1. M) * a = a & a * (1. M) = a ) )
A1: ( M is well-unital iff H3(M) is_a_unity_wrt H2(M) ) by Def21;
hence  ( M is well-unital implies for a being Element of M holds
( H3(M) * a = a & a * H3(M) = a ) ) by BINOP_1:3; ::_thesis: ( ( for a being Element of M holds
( (1. M) * a = a & a * (1. M) = a ) ) implies M is well-unital )
assume A2: for a being Element of M holds
( H3(M) * a = a & a * H3(M) = a ) ; ::_thesis: M is well-unital
now__::_thesis:_for_a_being_Element_of_M_holds_
(_H2(M)_._(H3(M),a)_=_a_&_H2(M)_._(a,H3(M))_=_a_)
let a be Element of M; ::_thesis: ( H2(M) . (H3(M),a) = a & H2(M) . (a,H3(M)) = a )
 ( H3(M) * a = a & a * H3(M) = a ) by A2;
hence  ( H2(M) . (H3(M),a) = a & H2(M) . (a,H3(M)) = a ) ; ::_thesis: verum
end;
hence  M is well-unital by A1, BINOP_1:3; ::_thesis: verum
end;

theorem Th17: :: MONOID_0:17
for M being non empty multLoopStr st M is well-unital holds
1. M = the_unity_wrt the multF of M
proof
let M be non empty multLoopStr ; ::_thesis: ( M is well-unital implies 1. M = the_unity_wrt the multF of M )
assume  H3(M) is_a_unity_wrt the multF of M ; :: according to MONOID_0:def_21 ::_thesis: 1. M = the_unity_wrt the multF of M
hence  1. M = the_unity_wrt the multF of M by BINOP_1:def_8; ::_thesis: verum
end;

registration
cluster non empty strict unital associative commutative well-unital constituted-Functions constituted-FinSeqs idempotent invertible cancelable uniquely-decomposable for multLoopStr ;
existence
 ex b1 being non empty multLoopStr st
( b1 is well-unital & b1 is commutative & b1 is associative & b1 is cancelable & b1 is idempotent & b1 is invertible & b1 is uniquely-decomposable & b1 is unital & b1 is constituted-Functions & b1 is constituted-FinSeqs & b1 is strict )
proof
set p = the FinSequence;
set o = the BinOp of { the FinSequence};
set e = the Element of { the FinSequence};
take G = multLoopStr(# { the FinSequence}, the BinOp of { the FinSequence}, the Element of { the FinSequence} #); ::_thesis: ( G is well-unital & G is commutative & G is associative & G is cancelable & G is idempotent & G is invertible & G is uniquely-decomposable & G is unital & G is constituted-Functions & G is constituted-FinSeqs & G is strict )
reconsider e = the Element of { the FinSequence} as Element of G ;
reconsider o = the BinOp of { the FinSequence} as BinOp of G ;
now__::_thesis:_for_b_being_Element_of_G_holds_
(_o_._(e,b)_=_b_&_o_._(b,e)_=_b_)
let b be Element of G; ::_thesis: ( o . (e,b) = b & o . (b,e) = b )
 ( o . (e,b) = the FinSequence & o . (b,e) = the FinSequence ) by TARSKI:def_1;
hence  ( o . (e,b) = b & o . (b,e) = b ) by TARSKI:def_1; ::_thesis: verum
end;
hence  H3(G) is_a_unity_wrt H2(G) by BINOP_1:3; :: according to MONOID_0:def_21 ::_thesis: ( G is commutative & G is associative & G is cancelable & G is idempotent & G is invertible & G is uniquely-decomposable & G is unital & G is constituted-Functions & G is constituted-FinSeqs & G is strict )
hence  ( H2(G) is commutative & H2(G) is associative & H2(G) is cancelable & H2(G) is idempotent & H2(G) is invertible & H2(G) is uniquely-decomposable & ex e being Element of G st e is_a_unity_wrt H2(G) ) by Th3; :: according to SETWISEO:def_2,MONOID_0:def_10,MONOID_0:def_11,MONOID_0:def_12,MONOID_0:def_13,MONOID_0:def_16,MONOID_0:def_19,MONOID_0:def_20 ::_thesis: ( G is constituted-Functions & G is constituted-FinSeqs & G is strict )
thus  ( ( for x being Element of G holds x is Function ) & ( for x being Element of G holds x is FinSequence ) ) by TARSKI:def_1; :: according to MONOID_0:def_1,MONOID_0:def_2 ::_thesis: G is strict
thus  G is strict ; ::_thesis: verum
end;
end;

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

definition
let G be multMagma ;
mode MonoidalExtension of G ->  multLoopStr  means :Def22: :: MONOID_0:def 22
 multMagma(# the carrier of it, the multF of it #) = multMagma(# the carrier of G, the multF of G #);
existence
 ex b1 being multLoopStr st multMagma(# the carrier of b1, the multF of b1 #) = multMagma(# the carrier of G, the multF of G #)
proof
set g = the Element of G;
take  multLoopStr(# H1(G),H2(G), the Element of G #) ; ::_thesis: multMagma(# the carrier of multLoopStr(# H1(G),H2(G), the Element of G #), the multF of multLoopStr(# H1(G),H2(G), the Element of G #) #) = multMagma(# the carrier of G, the multF of G #)
thus  multMagma(# the carrier of multLoopStr(# H1(G),H2(G), the Element of G #), the multF of multLoopStr(# H1(G),H2(G), the Element of G #) #) = multMagma(# the carrier of G, the multF of G #) ; ::_thesis: verum
end;
end;

:: deftheorem Def22 defines MonoidalExtension MONOID_0:def_22_:_
 for G being multMagma
for b2 being multLoopStr holds
( b2 is MonoidalExtension of G iff multMagma(# the carrier of b2, the multF of b2 #) = multMagma(# the carrier of G, the multF of G #) );

registration
let G be non empty multMagma ;
cluster  ->  non empty for MonoidalExtension of G;
coherence
 for b1 being MonoidalExtension of G holds not b1 is empty
proof
let M be MonoidalExtension of G; ::_thesis: not M is empty
 multMagma(# the carrier of M, the multF of M #) = multMagma(# the carrier of G, the multF of G #) by Def22;
hence  not the carrier of M is empty ; :: according to STRUCT_0:def_1 ::_thesis: verum
end;
end;

theorem Th18: :: MONOID_0:18
for G being non empty multMagma
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
for a9, b9 being Element of G st a = a9 & b = b9 holds
a * b = a9 * b9 ) )
proof
let G be non empty multMagma ; ::_thesis: 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
for a9, b9 being Element of G st a = a9 & b = b9 holds
a * b = a9 * b9 ) )
let M be MonoidalExtension of G; ::_thesis: ( the carrier of M = the carrier of G & the multF of M = the multF of G & ( for a, b being Element of M
for a9, b9 being Element of G st a = a9 & b = b9 holds
a * b = a9 * b9 ) )
A1: multMagma(# the carrier of M, the multF of M #) = multMagma(# the carrier of G, the multF of G #) by Def22;
hence  ( H1(M) = H1(G) & H2(M) = H2(G) ) ; ::_thesis: for a, b being Element of M
for a9, b9 being Element of G st a = a9 & b = b9 holds
a * b = a9 * b9
let a, b be Element of M; ::_thesis: for a9, b9 being Element of G st a = a9 & b = b9 holds
a * b = a9 * b9
let a9, b9 be Element of G; ::_thesis: ( a = a9 & b = b9 implies a * b = a9 * b9 )
thus  ( a = a9 & b = b9 implies a * b = a9 * b9 ) by A1; ::_thesis: verum
end;

registration
let G be multMagma ;
cluster strict for MonoidalExtension of G;
existence
 ex b1 being MonoidalExtension of G st b1 is strict
proof
set g = the Element of G;
set M = multLoopStr(# H1(G),H2(G), the Element of G #);
 multMagma(# the carrier of multLoopStr(# H1(G),H2(G), the Element of G #), the multF of multLoopStr(# H1(G),H2(G), the Element of G #) #) = multMagma(# the carrier of G, the multF of G #) ;
then  multLoopStr(# H1(G),H2(G), the Element of G #) is MonoidalExtension of G by Def22;
hence  ex b1 being MonoidalExtension of G st b1 is strict ; ::_thesis: verum
end;
end;

theorem Th19: :: MONOID_0:19
for G being non empty multMagma
for 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 ) )
proof
let G be non empty multMagma ; ::_thesis: for 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 ) )
let M be MonoidalExtension of G; ::_thesis: ( ( 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 ) )
A1: multMagma(# the carrier of M, the multF of M #) = multMagma(# the carrier of G, the multF of G #) by Def22;
thus  ( G is unital implies M is unital ) ::_thesis: ( ( G is commutative implies M is commutative ) & ( G is associative implies M is associative ) & ( G is invertible implies M is invertible ) & ( G is uniquely-decomposable implies M is uniquely-decomposable ) & ( G is cancelable implies M is cancelable ) )
proof
assume  H2(G) is having_a_unity ; :: according to MONOID_0:def_10 ::_thesis: M is unital
hence  H2(M) is having_a_unity by A1; :: according to MONOID_0:def_10 ::_thesis: verum
end;
thus  ( G is commutative implies M is commutative ) ::_thesis: ( ( G is associative implies M is associative ) & ( G is invertible implies M is invertible ) & ( G is uniquely-decomposable implies M is uniquely-decomposable ) & ( G is cancelable implies M is cancelable ) )
proof
assume  H2(G) is commutative ; :: according to MONOID_0:def_11 ::_thesis: M is commutative
hence  H2(M) is commutative by A1; :: according to MONOID_0:def_11 ::_thesis: verum
end;
thus  ( G is associative implies M is associative ) ::_thesis: ( ( G is invertible implies M is invertible ) & ( G is uniquely-decomposable implies M is uniquely-decomposable ) & ( G is cancelable implies M is cancelable ) )
proof
assume  H2(G) is associative ; :: according to MONOID_0:def_12 ::_thesis: M is associative
hence  H2(M) is associative by A1; :: according to MONOID_0:def_12 ::_thesis: verum
end;
thus  ( G is invertible implies M is invertible ) ::_thesis: ( ( G is uniquely-decomposable implies M is uniquely-decomposable ) & ( G is cancelable implies M is cancelable ) )
proof
assume  H2(G) is invertible ; :: according to MONOID_0:def_16 ::_thesis: M is invertible
hence  H2(M) is invertible by A1; :: according to MONOID_0:def_16 ::_thesis: verum
end;
thus  ( G is uniquely-decomposable implies M is uniquely-decomposable ) ::_thesis: ( G is cancelable implies M is cancelable )
proof
assume  H2(G) is uniquely-decomposable ; :: according to MONOID_0:def_20 ::_thesis: M is uniquely-decomposable
hence  H2(M) is uniquely-decomposable by A1; :: according to MONOID_0:def_20 ::_thesis: verum
end;
assume  H2(G) is cancelable ; :: according to MONOID_0:def_19 ::_thesis: M is cancelable
hence  H2(M) is cancelable by A1; :: according to MONOID_0:def_19 ::_thesis: verum
end;

registration
let G be constituted-Functions multMagma ;
cluster  ->  constituted-Functions for MonoidalExtension of G;
coherence
 for b1 being MonoidalExtension of G holds b1 is constituted-Functions
proof
let M be MonoidalExtension of G; ::_thesis: M is constituted-Functions
let a be Element of M; :: according to MONOID_0:def_1 ::_thesis: a is Function
 multMagma(# the carrier of M, the multF of M #) = multMagma(# the carrier of G, the multF of G #) by Def22;
hence  a is Function ; ::_thesis: verum
end;
end;

registration
let G be constituted-FinSeqs multMagma ;
cluster  ->  constituted-FinSeqs for MonoidalExtension of G;
coherence
 for b1 being MonoidalExtension of G holds b1 is constituted-FinSeqs
proof
let M be MonoidalExtension of G; ::_thesis: M is constituted-FinSeqs
let a be Element of M; :: according to MONOID_0:def_2 ::_thesis: a is FinSequence
 multMagma(# the carrier of M, the multF of M #) = multMagma(# the carrier of G, the multF of G #) by Def22;
hence  a is FinSequence ; ::_thesis: verum
end;
end;

registration
let G be non empty unital multMagma ;
cluster  ->  unital for MonoidalExtension of G;
coherence
 for b1 being MonoidalExtension of G holds b1 is unital by Th19;
end;

registration
let G be non empty associative multMagma ;
cluster  ->  associative for MonoidalExtension of G;
coherence
 for b1 being MonoidalExtension of G holds b1 is associative by Th19;
end;

registration
let G be non empty commutative multMagma ;
cluster  ->  commutative for MonoidalExtension of G;
coherence
 for b1 being MonoidalExtension of G holds b1 is commutative by Th19;
end;

registration
let G be non empty invertible multMagma ;
cluster  ->  invertible for MonoidalExtension of G;
coherence
 for b1 being MonoidalExtension of G holds b1 is invertible by Th19;
end;

registration
let G be non empty cancelable multMagma ;
cluster  ->  cancelable for MonoidalExtension of G;
coherence
 for b1 being MonoidalExtension of G holds b1 is cancelable by Th19;
end;

registration
let G be non empty uniquely-decomposable multMagma ;
cluster  ->  uniquely-decomposable for MonoidalExtension of G;
coherence
 for b1 being MonoidalExtension of G holds b1 is uniquely-decomposable by Th19;
end;

registration
let G be non empty unital multMagma ;
cluster non empty strict unital well-unital for MonoidalExtension of G;
existence
 ex b1 being MonoidalExtension of G st
( b1 is well-unital & b1 is strict )
proof
set M = multLoopStr(# H1(G),H2(G),(the_unity_wrt H2(G)) #);
 multMagma(# the carrier of multLoopStr(# H1(G),H2(G),(the_unity_wrt H2(G)) #), the multF of multLoopStr(# H1(G),H2(G),(the_unity_wrt H2(G)) #) #) = multMagma(# the carrier of G, the multF of G #) ;
then reconsider M = multLoopStr(# H1(G),H2(G),(the_unity_wrt H2(G)) #) as MonoidalExtension of G by Def22;
take  M ; ::_thesis: ( M is well-unital & M is strict )
thus  H3(M) is_a_unity_wrt H2(M) by Th4; :: according to MONOID_0:def_21 ::_thesis: M is strict
thus  M is strict ; ::_thesis: verum
end;
end;

theorem Th20: :: MONOID_0:20
for G being non empty unital multMagma
for M1, M2 being strict well-unital MonoidalExtension of G holds M1 = M2
proof
let G be non empty unital multMagma ; ::_thesis: for M1, M2 being strict well-unital MonoidalExtension of G holds M1 = M2
let M1, M2 be strict well-unital MonoidalExtension of G; ::_thesis: M1 = M2
A1: ( H3(M1) = the_unity_wrt H2(M1) & H3(M2) = the_unity_wrt H2(M2) ) by Th17;
 ( multMagma(# the carrier of M1, the multF of M1 #) = multMagma(# the carrier of G, the multF of G #) & multMagma(# the carrier of M2, the multF of M2 #) = multMagma(# the carrier of G, the multF of G #) ) by Def22;
hence  M1 = M2 by A1; ::_thesis: verum
end;

begin

definition
let G be multMagma ;
mode SubStr of G ->  multMagma  means :Def23: :: MONOID_0:def 23
 the multF of it c= the multF of G;
existence
 ex b1 being multMagma st the multF of b1 c= the multF of G ;
end;

:: deftheorem Def23 defines SubStr MONOID_0:def_23_:_
 for G, b2 being multMagma holds
( b2 is SubStr of G iff the multF of b2 c= the multF of G );

registration
let G be multMagma ;
cluster strict for SubStr of G;
existence
 ex b1 being SubStr of G st b1 is strict
proof
 multMagma(# the carrier of G, the multF of G #) is SubStr of G by Def23;
hence  ex b1 being SubStr of G st b1 is strict ; ::_thesis: verum
end;
end;

registration
let G be non empty multMagma ;
cluster non empty strict for SubStr of G;
existence
 ex b1 being SubStr of G st
( b1 is strict & not b1 is empty )
proof
 multMagma(# the carrier of G, the multF of G #) is SubStr of G by Def23;
hence  ex b1 being SubStr of G st
( b1 is strict & not b1 is empty ) ; ::_thesis: verum
end;
end;

registration
let G be non empty unital multMagma ;
cluster non empty strict unital associative commutative idempotent invertible cancelable uniquely-decomposable for SubStr of G;
existence
 ex b1 being non empty SubStr of G st
( b1 is unital & b1 is associative & b1 is commutative & b1 is cancelable & b1 is idempotent & b1 is invertible & b1 is uniquely-decomposable & b1 is strict )
proof
consider a being Element of G such that
A1: for b being Element of G holds
( a * b = b & b * a = b ) by Th6;
A2: a = a * a by A1;
set f = the BinOp of {a};
set H = multMagma(# {a}, the BinOp of {a} #);
A3: dom H2(G) = [:H1(G),H1(G):] by FUNCT_2:def_1;
the BinOp of {a} = (a,a) .--> a by Th3
.= [a,a] .--> a ;
then  H2( multMagma(# {a}, the BinOp of {a} #)) c= H2(G) by A2, A3, FUNCT_4:7;
then reconsider H = multMagma(# {a}, the BinOp of {a} #) as non empty SubStr of G by Def23;
take  H ; ::_thesis: ( H is unital & H is associative & H is commutative & H is cancelable & H is idempotent & H is invertible & H is uniquely-decomposable & H is strict )
thus  ( H2(H) is having_a_unity & H2(H) is associative & H2(H) is commutative & H2(H) is cancelable & H2(H) is idempotent & H2(H) is invertible & H2(H) is uniquely-decomposable ) by Th3; :: according to MONOID_0:def_10,MONOID_0:def_11,MONOID_0:def_12,MONOID_0:def_13,MONOID_0:def_16,MONOID_0:def_19,MONOID_0:def_20 ::_thesis: H is strict
thus  H is strict ; ::_thesis: verum
end;
end;

definition
let G be multMagma ;
mode MonoidalSubStr of G ->  multLoopStr  means :Def24: :: 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 ) );
existence
 ex b1 being multLoopStr st
( the multF of b1 c= the multF of G & ( for M being multLoopStr st G = M holds
1. b1 = 1. M ) )
proof
set M = the MonoidalExtension of G;
A1: now__::_thesis:_(_ex_M_being_multLoopStr_st_G_=_M_implies_ex_M_being_multLoopStr_st_
(_H2(M)_c=_H2(G)_&_(_for_N_being_multLoopStr_st_G_=_N_holds_
H3(M)_=_H3(N)_)_)_)
given M being multLoopStr  such that A2: G = M ; ::_thesis: ex M being multLoopStr st
( H2(M) c= H2(G) & ( for N being multLoopStr st G = N holds
H3(M) = H3(N) ) )
take M = M; ::_thesis: ( H2(M) c= H2(G) & ( for N being multLoopStr st G = N holds
H3(M) = H3(N) ) )
thus  H2(M) c= H2(G) by A2; ::_thesis: for N being multLoopStr st G = N holds
H3(M) = H3(N)
thus  for N being multLoopStr st G = N holds
H3(M) = H3(N) by A2; ::_thesis: verum
end;
A3: ( ex M being multLoopStr st G = M or for N being multLoopStr st G = N holds
H3( the MonoidalExtension of G) = H3(N) ) ;
 multMagma(# the carrier of the MonoidalExtension of G, the multF of the MonoidalExtension of G #) = multMagma(# the carrier of G, the multF of G #) by Def22;
hence  ex b1 being multLoopStr st
( the multF of b1 c= the multF of G & ( for M being multLoopStr st G = M holds
1. b1 = 1. M ) ) by A1, A3; ::_thesis: verum
end;
end;

:: deftheorem Def24 defines MonoidalSubStr MONOID_0:def_24_:_
 for G being multMagma
for b2 being multLoopStr holds
( b2 is MonoidalSubStr of G iff ( the multF of b2 c= the multF of G & ( for M being multLoopStr st G = M holds
1. b2 = 1. M ) ) );

registration
let G be multMagma ;
cluster strict for MonoidalSubStr of G;
existence
 ex b1 being MonoidalSubStr of G st b1 is strict
proof
set N = the MonoidalSubStr of G;
 H3( multLoopStr(# the carrier of the MonoidalSubStr of G, the multF of the MonoidalSubStr of G, the OneF of the MonoidalSubStr of G #)) = H3( the MonoidalSubStr of G) ;
then A1: for M being multLoopStr st G = M holds
H3( multLoopStr(# the carrier of the MonoidalSubStr of G, the multF of the MonoidalSubStr of G, the OneF of the MonoidalSubStr of G #)) = H3(M) by Def24;
 H2( multLoopStr(# the carrier of the MonoidalSubStr of G, the multF of the MonoidalSubStr of G, the OneF of the MonoidalSubStr of G #)) c= H2(G) by Def24;
then  multLoopStr(# the carrier of the MonoidalSubStr of G, the multF of the MonoidalSubStr of G, the OneF of the MonoidalSubStr of G #) is MonoidalSubStr of G by A1, Def24;
hence  ex b1 being MonoidalSubStr of G st b1 is strict ; ::_thesis: verum
end;
end;

registration
let G be non empty multMagma ;
cluster non empty strict for MonoidalSubStr of G;
existence
 ex b1 being MonoidalSubStr of G st
( b1 is strict & not b1 is empty )
proof
percases ( G is multLoopStr or not G is multLoopStr ) ;
suppose G is multLoopStr ; ::_thesis: ex b1 being MonoidalSubStr of G st
( b1 is strict & not b1 is empty )
then reconsider L = G as multLoopStr ;
 for N being multLoopStr st G = N holds
1. multLoopStr(# the carrier of L, the multF of L, the OneF of L #) = 1. N ;
then reconsider M = multLoopStr(# the carrier of L, the multF of L, the OneF of L #) as MonoidalSubStr of G by Def24;
take  M ; ::_thesis: ( M is strict & not M is empty )
thus  M is strict ; ::_thesis: not M is empty
thus  not the carrier of M is empty ; :: according to STRUCT_0:def_1 ::_thesis: verum
end;
supposeA1: G is not multLoopStr ; ::_thesis: ex b1 being MonoidalSubStr of G st
( b1 is strict & not b1 is empty )
set M = the strict MonoidalExtension of G;
A2: for N being multLoopStr st G = N holds
1. the strict MonoidalExtension of G = 1. N by A1;
 multMagma(# the carrier of the strict MonoidalExtension of G, the multF of the strict MonoidalExtension of G #) = multMagma(# the carrier of G, the multF of G #) by Def22;
then reconsider M = the strict MonoidalExtension of G as MonoidalSubStr of G by A2, Def24;
take  M ; ::_thesis: ( M is strict & not M is empty )
thus  ( M is strict & not M is empty ) ; ::_thesis: verum
end;
end;
end;
end;

definition
let M be multLoopStr ;
redefine mode MonoidalSubStr of M means :Def25: :: MONOID_0:def 25
( the multF of it c= the multF of M & 1. it = 1. M );
compatibility
 for b1 being multLoopStr holds
( b1 is MonoidalSubStr of M iff ( the multF of b1 c= the multF of M & 1. b1 = 1. M ) )
proof
let N be multLoopStr ; ::_thesis: ( N is MonoidalSubStr of M iff ( the multF of N c= the multF of M & 1. N = 1. M ) )
thus  ( N is MonoidalSubStr of M implies ( H2(N) c= H2(M) & H3(N) = H3(M) ) ) ::_thesis: ( the multF of N c= the multF of M & 1. N = 1. M implies N is MonoidalSubStr of M )
proof
assume  ( H2(N) c= H2(M) & ( for K being multLoopStr st M = K holds
H3(N) = H3(K) ) ) ; :: according to MONOID_0:def_24 ::_thesis: ( H2(N) c= H2(M) & H3(N) = H3(M) )
hence  ( H2(N) c= H2(M) & H3(N) = H3(M) ) ; ::_thesis: verum
end;
assume  ( H2(N) c= H2(M) & H3(N) = H3(M) ) ; ::_thesis: N is MonoidalSubStr of M
hence  ( H2(N) c= H2(M) & ( for K being multLoopStr st M = K holds
H3(N) = H3(K) ) ) ; :: according to MONOID_0:def_24 ::_thesis: verum
end;
end;

:: deftheorem Def25 defines MonoidalSubStr MONOID_0:def_25_:_
 for M, b2 being multLoopStr holds
( b2 is MonoidalSubStr of M iff ( the multF of b2 c= the multF of M & 1. b2 = 1. M ) );

registration
let G be non empty well-unital multLoopStr ;
cluster non empty strict associative commutative well-unital idempotent invertible cancelable uniquely-decomposable for MonoidalSubStr of G;
existence
 ex b1 being non empty MonoidalSubStr of G st
( b1 is well-unital & b1 is associative & b1 is commutative & b1 is cancelable & b1 is idempotent & b1 is invertible & b1 is uniquely-decomposable & b1 is strict )
proof
set a = H3(G);
reconsider e = H3(G) as Element of {H3(G)} by TARSKI:def_1;
set f = the BinOp of {H3(G)};
set H = multLoopStr(# {H3(G)}, the BinOp of {H3(G)},e #);
A1: ( H3(G) = H3(G) * H3(G) & dom H2(G) = [:H1(G),H1(G):] ) by Th16, FUNCT_2:def_1;
 ( [H3(G),H3(G)] .--> H3(G) = {[H3(G),H3(G)]} --> H3(G) & the BinOp of {H3(G)} = (H3(G),H3(G)) .--> H3(G) ) by Th3;
then  ( 1. multLoopStr(# {H3(G)}, the BinOp of {H3(G)},e #) = 1. G & H2( multLoopStr(# {H3(G)}, the BinOp of {H3(G)},e #)) c= H2(G) ) by A1, FUNCT_4:7;
then reconsider H = multLoopStr(# {H3(G)}, the BinOp of {H3(G)},e #) as non empty MonoidalSubStr of G by Def25;
take  H ; ::_thesis: ( H is well-unital & H is associative & H is commutative & H is cancelable & H is idempotent & H is invertible & H is uniquely-decomposable & H is strict )
now__::_thesis:_for_b_being_Element_of_H_holds_
(_H2(H)_._(H3(H),b)_=_b_&_H2(H)_._(b,H3(H))_=_b_)
let b be Element of H; ::_thesis: ( H2(H) . (H3(H),b) = b & H2(H) . (b,H3(H)) = b )
 b = H3(G) by TARSKI:def_1;
hence  ( H2(H) . (H3(H),b) = b & H2(H) . (b,H3(H)) = b ) by TARSKI:def_1; ::_thesis: verum
end;
hence  H3(H) is_a_unity_wrt H2(H) by BINOP_1:3; :: according to MONOID_0:def_21 ::_thesis: ( H is associative & H is commutative & H is cancelable & H is idempotent & H is invertible & H is uniquely-decomposable & H is strict )
thus  ( H2(H) is associative & H2(H) is commutative & H2(H) is cancelable & H2(H) is idempotent & H2(H) is invertible & H2(H) is uniquely-decomposable ) by Th3; :: according to MONOID_0:def_11,MONOID_0:def_12,MONOID_0:def_13,MONOID_0:def_16,MONOID_0:def_19,MONOID_0:def_20 ::_thesis: H is strict
thus  H is strict ; ::_thesis: verum
end;
end;

theorem Th21: :: MONOID_0:21
for G being multMagma
for M being MonoidalSubStr of G holds M is SubStr of G
proof
let G be multMagma ; ::_thesis: for M being MonoidalSubStr of G holds M is SubStr of G
let M be MonoidalSubStr of G; ::_thesis: M is SubStr of G
thus  H2(M) c= H2(G) by Def24; :: according to MONOID_0:def_23 ::_thesis: verum
end;

definition
let G be multMagma ;
let M be MonoidalExtension of G;
:: original: SubStr
redefine mode SubStr of M ->  SubStr of G;
coherence
 for b1 being SubStr of M holds b1 is SubStr of G
proof
let N be SubStr of M; ::_thesis: N is SubStr of G
 multMagma(# the carrier of M, the multF of M #) = multMagma(# the carrier of G, the multF of G #) by Def22;
hence  H2(N) c= H2(G) by Def23; :: according to MONOID_0:def_23 ::_thesis: verum
end;
end;

definition
let G1 be multMagma ;
let G2 be SubStr of G1;
:: original: SubStr
redefine mode SubStr of G2 ->  SubStr of G1;
coherence
 for b1 being SubStr of G2 holds b1 is SubStr of G1
proof
let G be SubStr of G2; ::_thesis: G is SubStr of G1
 ( H2(G) c= H2(G2) & H2(G2) c= H2(G1) ) by Def23;
hence  H2(G) c= H2(G1) by XBOOLE_1:1; :: according to MONOID_0:def_23 ::_thesis: verum
end;
end;

definition
let G1 be multMagma ;
let G2 be MonoidalSubStr of G1;
:: original: SubStr
redefine mode SubStr of G2 ->  SubStr of G1;
coherence
 for b1 being SubStr of G2 holds b1 is SubStr of G1
proof
reconsider H = G2 as SubStr of G1 by Th21;
let G be SubStr of G2; ::_thesis: G is SubStr of G1
 G is SubStr of H ;
hence  G is SubStr of G1 ; ::_thesis: verum
end;
end;

definition
let G be multMagma ;
let M be MonoidalSubStr of G;
:: original: MonoidalSubStr
redefine mode MonoidalSubStr of M ->  MonoidalSubStr of G;
coherence
 for b1 being MonoidalSubStr of M holds b1 is MonoidalSubStr of G
proof
let M9 be MonoidalSubStr of M; ::_thesis: M9 is MonoidalSubStr of G
A1: H3(M9) = H3(M) by Def24;
 ( H2(M9) c= H2(M) & H2(M) c= H2(G) ) by Def24;
hence  ( H2(M9) c= H2(G) & ( for N being multLoopStr st G = N holds
H3(M9) = H3(N) ) ) by A1, Def24, XBOOLE_1:1; :: according to MONOID_0:def_24 ::_thesis: verum
end;
end;

theorem :: MONOID_0:22
for G being non empty multMagma
for M being non empty multLoopStr holds
( G is SubStr of G & M is MonoidalSubStr of M )
proof
let G be non empty multMagma ; ::_thesis: for M being non empty multLoopStr holds
( G is SubStr of G & M is MonoidalSubStr of M )
let M be non empty multLoopStr ; ::_thesis: ( G is SubStr of G & M is MonoidalSubStr of M )
thus  H2(G) c= H2(G) ; :: according to MONOID_0:def_23 ::_thesis: M is MonoidalSubStr of M
thus  H2(M) c= H2(M) ; :: according to MONOID_0:def_25 ::_thesis: 1. M = 1. M
thus  1. M = 1. M ; ::_thesis: verum
end;


theorem Th23: :: MONOID_0:23
for G being non empty multMagma
for H being non empty SubStr of G
for N being non empty MonoidalSubStr of G holds
( the carrier of H c= the carrier of G & the carrier of N c= the carrier of G )
proof
let G be non empty multMagma ; ::_thesis: for H being non empty SubStr of G
for N being non empty MonoidalSubStr of G holds
( the carrier of H c= the carrier of G & the carrier of N c= the carrier of G )
let H be non empty SubStr of G; ::_thesis: for N being non empty MonoidalSubStr of G holds
( the carrier of H c= the carrier of G & the carrier of N c= the carrier of G )
let N be non empty MonoidalSubStr of G; ::_thesis: ( the carrier of H c= the carrier of G & the carrier of N c= the carrier of G )
A1: dom H2(N) = [:H1(N),H1(N):] by FUNCT_2:def_1;
A2: dom H2(G) = [:H1(G),H1(G):] by FUNCT_2:def_1;
 H2(H) c= H2(G) by Def23;
then A3: dom H2(H) c= dom H2(G) by GRFUNC_1:2;
A4: dom H2(H) = [:H1(H),H1(H):] by FUNCT_2:def_1;
thus  H1(H) c= H1(G) ::_thesis: the carrier of N c= the carrier of G
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in H1(H) or x in H1(G) )
assume  x in H1(H) ; ::_thesis: x in H1(G)
then  [x,x] in dom H2(H) by A4, ZFMISC_1:87;
hence  x in H1(G) by A3, A2, ZFMISC_1:87; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in the carrier of N or x in the carrier of G )
 H2(N) c= H2(G) by Def24;
then A5: dom H2(N) c= dom H2(G) by GRFUNC_1:2;
assume  x in H1(N) ; ::_thesis: x in the carrier of G
then  [x,x] in dom H2(N) by A1, ZFMISC_1:87;
hence  x in the carrier of G by A5, A2, ZFMISC_1:87; ::_thesis: verum
end;

theorem Th24: :: MONOID_0:24
for G being non empty multMagma
for H being non empty SubStr of G holds the multF of H = the multF of G || the carrier of H
proof
let G be non empty multMagma ; ::_thesis: for H being non empty SubStr of G holds the multF of H = the multF of G || the carrier of H
let H be non empty SubStr of G; ::_thesis: the multF of H = the multF of G || the carrier of H
 ( H2(H) c= H2(G) & dom H2(H) = [:H1(H),H1(H):] ) by Def23, FUNCT_2:def_1;
hence  the multF of H = the multF of G || the carrier of H by GRFUNC_1:23; ::_thesis: verum
end;

theorem Th25: :: MONOID_0:25
for G being non empty multMagma
for H being non empty SubStr of G
for a, b being Element of H
for a9, b9 being Element of G st a = a9 & b = b9 holds
a * b = a9 * b9
proof
let G be non empty multMagma ; ::_thesis: for H being non empty SubStr of G
for a, b being Element of H
for a9, b9 being Element of G st a = a9 & b = b9 holds
a * b = a9 * b9
let H be non empty SubStr of G; ::_thesis: for a, b being Element of H
for a9, b9 being Element of G st a = a9 & b = b9 holds
a * b = a9 * b9
let a, b be Element of H; ::_thesis: for a9, b9 being Element of G st a = a9 & b = b9 holds
a * b = a9 * b9
let a9, b9 be Element of G; ::_thesis: ( a = a9 & b = b9 implies a * b = a9 * b9 )
assume A1: ( a = a9 & b = b9 ) ; ::_thesis: a * b = a9 * b9
A2: ( dom H2(H) = [:H1(H),H1(H):] & H2(H) c= H2(G) ) by Def23, FUNCT_2:def_1;
thus a * b = H2(H) . [a,b]
.= a9 * b9 by A1, A2, GRFUNC_1:2 ; ::_thesis: verum
end;

theorem Th26: :: MONOID_0:26
for G being non empty multMagma
for H1, H2 being non empty SubStr of G st the carrier of H1 = the carrier of H2 holds
multMagma(# the carrier of H1, the multF of H1 #) = multMagma(# the carrier of H2, the multF of H2 #)
proof
let G be non empty multMagma ; ::_thesis: for H1, H2 being non empty SubStr of G st the carrier of H1 = the carrier of H2 holds
multMagma(# the carrier of H1, the multF of H1 #) = multMagma(# the carrier of H2, the multF of H2 #)
let H1, H2 be non empty SubStr of G; ::_thesis: ( the carrier of H1 = the carrier of H2 implies multMagma(# the carrier of H1, the multF of H1 #) = multMagma(# the carrier of H2, the multF of H2 #) )
A1: H2(H2) c= H2(G) by Def23;
 ( H2(H1) c= H2(G) & dom H2(H1) = [:H1(H1),H1(H1):] ) by Def23, FUNCT_2:def_1;
then A2: H2(H1) = H2(G) || H1(H1) by GRFUNC_1:23;
assume A3: H1(H1) = H1(H2) ; ::_thesis: multMagma(# the carrier of H1, the multF of H1 #) = multMagma(# the carrier of H2, the multF of H2 #)
then  dom H2(H2) = [:H1(H1),H1(H1):] by FUNCT_2:def_1;
hence  multMagma(# the carrier of H1, the multF of H1 #) = multMagma(# the carrier of H2, the multF of H2 #) by A3, A1, A2, GRFUNC_1:23; ::_thesis: verum
end;

theorem :: MONOID_0:27
for M being non empty multLoopStr
for H1, H2 being non empty MonoidalSubStr of M st the carrier of H1 = the carrier of H2 holds
multLoopStr(# the carrier of H1, the multF of H1, the OneF of H1 #) = multLoopStr(# the carrier of H2, the multF of H2, the OneF of H2 #)
proof
let M be non empty multLoopStr ; ::_thesis: for H1, H2 being non empty MonoidalSubStr of M st the carrier of H1 = the carrier of H2 holds
multLoopStr(# the carrier of H1, the multF of H1, the OneF of H1 #) = multLoopStr(# the carrier of H2, the multF of H2, the OneF of H2 #)
let H1, H2 be non empty MonoidalSubStr of M; ::_thesis: ( the carrier of H1 = the carrier of H2 implies multLoopStr(# the carrier of H1, the multF of H1, the OneF of H1 #) = multLoopStr(# the carrier of H2, the multF of H2, the OneF of H2 #) )
assume A1: the carrier of H1 = the carrier of H2 ; ::_thesis: multLoopStr(# the carrier of H1, the multF of H1, the OneF of H1 #) = multLoopStr(# the carrier of H2, the multF of H2, the OneF of H2 #)
reconsider N1 = H1, N2 = H2 as SubStr of M by Th21;
A2: ( H3(H1) = H3(M) & H3(H2) = H3(M) ) by Def25;
 multMagma(# the carrier of N1, the multF of N1 #) = multMagma(# the carrier of N2, the multF of N2 #) by A1, Th26;
hence  multLoopStr(# the carrier of H1, the multF of H1, the OneF of H1 #) = multLoopStr(# the carrier of H2, the multF of H2, the OneF of H2 #) by A2; ::_thesis: verum
end;

theorem Th28: :: MONOID_0:28
for G being non empty multMagma
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
proof
let G be non empty multMagma ; ::_thesis: 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
let H1, H2 be non empty SubStr of G; ::_thesis: ( the carrier of H1 c= the carrier of H2 implies H1 is SubStr of H2 )
assume  H1(H1) c= H1(H2) ; ::_thesis: H1 is SubStr of H2
then  [:H1(H1),H1(H1):] c= [:H1(H2),H1(H2):] by ZFMISC_1:96;
then A1: (H2(G) || H1(H2)) || H1(H1) = H2(G) || H1(H1) by FUNCT_1:51;
 ( H2(H2) c= H2(G) & dom H2(H2) = [:H1(H2),H1(H2):] ) by Def23, FUNCT_2:def_1;
then A2: H2(H2) = H2(G) || H1(H2) by GRFUNC_1:23;
 ( H2(H1) c= H2(G) & dom H2(H1) = [:H1(H1),H1(H1):] ) by Def23, FUNCT_2:def_1;
then  H2(H1) = H2(G) || H1(H1) by GRFUNC_1:23;
hence  H2(H1) c= H2(H2) by A1, A2, RELAT_1:59; :: according to MONOID_0:def_23 ::_thesis: verum
end;

theorem :: MONOID_0:29
for M being non empty multLoopStr
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
proof
let M be non empty multLoopStr ; ::_thesis: 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
let H1, H2 be non empty MonoidalSubStr of M; ::_thesis: ( the carrier of H1 c= the carrier of H2 implies H1 is MonoidalSubStr of H2 )
assume A1: H1(H1) c= H1(H2) ; ::_thesis: H1 is MonoidalSubStr of H2
 ( H1 is SubStr of M & H2 is SubStr of M ) by Th21;
then  H1 is SubStr of H2 by A1, Th28;
hence  H2(H1) c= H2(H2) by Def23; :: according to MONOID_0:def_25 ::_thesis: 1. H1 = 1. H2
 H3(H1) = H3(M) by Def25;
hence  1. H1 = 1. H2 by Def25; ::_thesis: verum
end;

theorem Th30: :: MONOID_0:30
for G being non empty multMagma
for H being non empty SubStr of G st G is unital & the_unity_wrt the multF of G in the carrier of H holds
( H is unital & the_unity_wrt the multF of G = the_unity_wrt the multF of H )
proof
let G be non empty multMagma ; ::_thesis: for H being non empty SubStr of G st G is unital & the_unity_wrt the multF of G in the carrier of H holds
( H is unital & the_unity_wrt the multF of G = the_unity_wrt the multF of H )
let H be non empty SubStr of G; ::_thesis: ( 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 ) )
set e9 = the_unity_wrt H2(G);
assume  G is unital ; ::_thesis: ( not the_unity_wrt the multF of G in the carrier of H or ( H is unital & the_unity_wrt the multF of G = the_unity_wrt the multF of H ) )
then A1: the_unity_wrt H2(G) is_a_unity_wrt H2(G) by Th4;
assume  the_unity_wrt H2(G) in H1(H) ; ::_thesis: ( H is unital & the_unity_wrt the multF of G = the_unity_wrt the multF of H )
then reconsider e = the_unity_wrt H2(G) as Element of H ;
A2: now__::_thesis:_for_a_being_Element_of_H_holds_
(_e_*_a_=_a_&_a_*_e_=_a_)
let a be Element of H; ::_thesis: ( e * a = a & a * e = a )
 H1(H) c= H1(G) by Th23;
then reconsider a9 = a as Element of G by TARSKI:def_3;
thus e * a = (the_unity_wrt H2(G)) * a9 by Th25
.= a by A1, BINOP_1:3 ; ::_thesis: a * e = a
thus a * e = a9 * (the_unity_wrt H2(G)) by Th25
.= a by A1, BINOP_1:3 ; ::_thesis: verum
end;
hence  H is unital by Th6; ::_thesis: the_unity_wrt the multF of G = the_unity_wrt the multF of H
now__::_thesis:_for_a_being_Element_of_H_holds_
(_H2(H)_._(e,a)_=_a_&_H2(H)_._(a,e)_=_a_)
let a be Element of H; ::_thesis: ( H2(H) . (e,a) = a & H2(H) . (a,e) = a )
 ( e * a = H2(H) . (e,a) & a * e = H2(H) . (a,e) ) ;
hence  ( H2(H) . (e,a) = a & H2(H) . (a,e) = a ) by A2; ::_thesis: verum
end;
then  e is_a_unity_wrt H2(H) by BINOP_1:3;
hence  the_unity_wrt the multF of G = the_unity_wrt the multF of H by BINOP_1:def_8; ::_thesis: verum
end;

theorem Th31: :: MONOID_0:31
for M being non empty well-unital multLoopStr
for N being non empty MonoidalSubStr of M holds N is well-unital
proof
let M be non empty well-unital multLoopStr ; ::_thesis: for N being non empty MonoidalSubStr of M holds N is well-unital
let N be non empty MonoidalSubStr of M; ::_thesis: N is well-unital
A1: H3(M) is_a_unity_wrt H2(M) by Def21;
A2: ( N is SubStr of M & H3(N) = H3(M) ) by Def24, Th21;
now__::_thesis:_for_a_being_Element_of_N_holds_
(_H2(N)_._(H3(N),a)_=_a_&_H2(N)_._(a,H3(N))_=_a_)
let a be Element of N; ::_thesis: ( H2(N) . (H3(N),a) = a & H2(N) . (a,H3(N)) = a )
 H1(N) c= H1(M) by Th23;
then reconsider a9 = a as Element of M by TARSKI:def_3;
thus H2(N) . (H3(N),a) = H3(N) * a
.= H3(M) * a9 by A2, Th25
.= a by A1, BINOP_1:3 ; ::_thesis: H2(N) . (a,H3(N)) = a
thus H2(N) . (a,H3(N)) = a * H3(N)
.= a9 * H3(M) by A2, Th25
.= a by A1, BINOP_1:3 ; ::_thesis: verum
end;
hence  H3(N) is_a_unity_wrt H2(N) by BINOP_1:3; :: according to MONOID_0:def_21 ::_thesis: verum
end;

theorem Th32: :: MONOID_0:32
for G being non empty multMagma
for H being non empty SubStr of G st G is commutative holds
H is commutative
proof
let G be non empty multMagma ; ::_thesis: for H being non empty SubStr of G st G is commutative holds
H is commutative
let H be non empty SubStr of G; ::_thesis: ( G is commutative implies H is commutative )
assume A1: G is commutative ; ::_thesis: H is commutative
now__::_thesis:_for_a,_b_being_Element_of_H_holds_a_*_b_=_b_*_a
let a, b be Element of H; ::_thesis: a * b = b * a
 H1(H) c= H1(G) by Th23;
then reconsider a9 = a, b9 = b as Element of G by TARSKI:def_3;
thus a * b = a9 * b9 by Th25
.= b9 * a9 by A1, Lm1
.= b * a by Th25 ; ::_thesis: verum
end;
hence  H is commutative by Lm1; ::_thesis: verum
end;

theorem Th33: :: MONOID_0:33
for G being non empty multMagma
for H being non empty SubStr of G st G is associative holds
H is associative
proof
let G be non empty multMagma ; ::_thesis: for H being non empty SubStr of G st G is associative holds
H is associative
let H be non empty SubStr of G; ::_thesis: ( G is associative implies H is associative )
assume A1: G is associative ; ::_thesis: H is associative
now__::_thesis:_for_a,_b,_c_being_Element_of_H_holds_(a_*_b)_*_c_=_a_*_(b_*_c)
let a, b, c be Element of H; ::_thesis: (a * b) * c = a * (b * c)
 H1(H) c= H1(G) by Th23;
then reconsider a9 = a, b9 = b, c9 = c, ab = a * b, bc = b * c as Element of G by TARSKI:def_3;
thus (a * b) * c = ab * c9 by Th25
.= (a9 * b9) * c9 by Th25
.= a9 * (b9 * c9) by A1, Lm2
.= a9 * bc by Th25
.= a * (b * c) by Th25 ; ::_thesis: verum
end;
hence  H is associative by Lm2; ::_thesis: verum
end;

theorem Th34: :: MONOID_0:34
for G being non empty multMagma
for H being non empty SubStr of G st G is idempotent holds
H is idempotent
proof
let G be non empty multMagma ; ::_thesis: for H being non empty SubStr of G st G is idempotent holds
H is idempotent
let H be non empty SubStr of G; ::_thesis: ( G is idempotent implies H is idempotent )
assume A1: G is idempotent ; ::_thesis: H is idempotent
A2: H1(H) c= H1(G) by Th23;
now__::_thesis:_for_a_being_Element_of_H_holds_a_*_a_=_a
let a be Element of H; ::_thesis: a * a = a
reconsider a9 = a as Element of G by A2, TARSKI:def_3;
thus a * a = a9 * a9 by Th25
.= a by A1, Th7 ; ::_thesis: verum
end;
hence  H is idempotent by Th7; ::_thesis: verum
end;

theorem Th35: :: MONOID_0:35
for G being non empty multMagma
for H being non empty SubStr of G st G is cancelable holds
H is cancelable
proof
let G be non empty multMagma ; ::_thesis: for H being non empty SubStr of G st G is cancelable holds
H is cancelable
let H be non empty SubStr of G; ::_thesis: ( G is cancelable implies H is cancelable )
assume A1: G is cancelable ; ::_thesis: H is cancelable
A2: H1(H) c= H1(G) by Th23;
now__::_thesis:_for_a,_b,_c_being_Element_of_H_st_(_a_*_b_=_a_*_c_or_b_*_a_=_c_*_a_)_holds_
b_=_c
let a, b, c be Element of H; ::_thesis: ( ( a * b = a * c or b * a = c * a ) implies b = c )
reconsider a9 = a, b9 = b, c9 = c as Element of G by A2, TARSKI:def_3;
A3: ( b * a = b9 * a9 & c * a = c9 * a9 ) by Th25;
 ( a * b = a9 * b9 & a * c = a9 * c9 ) by Th25;
hence  ( ( a * b = a * c or b * a = c * a ) implies b = c ) by A1, A3, Th13; ::_thesis: verum
end;
hence  H is cancelable by Th13; ::_thesis: verum
end;

theorem Th36: :: MONOID_0:36
for G being non empty multMagma
for H being non empty SubStr of G st the_unity_wrt the multF of G in the carrier of H & G is uniquely-decomposable holds
H is uniquely-decomposable
proof
let G be non empty multMagma ; ::_thesis: for H being non empty SubStr of G st the_unity_wrt the multF of G in the carrier of H & G is uniquely-decomposable holds
H is uniquely-decomposable
let H be non empty SubStr of G; ::_thesis: ( the_unity_wrt the multF of G in the carrier of H & G is uniquely-decomposable implies H is uniquely-decomposable )
assume A1: the_unity_wrt H2(G) in H1(H) ; ::_thesis: ( not G is uniquely-decomposable or H is uniquely-decomposable )
assume that
A2: H2(G) is having_a_unity and
A3: for a, b being Element of G st H2(G) . (a,b) = the_unity_wrt H2(G) holds
( a = b & b = the_unity_wrt H2(G) ) ; :: according to MONOID_0:def_9,MONOID_0:def_20 ::_thesis: H is uniquely-decomposable
A4: G is unital by A2, Def10;
then  H is unital by A1, Th30;
hence  H2(H) is having_a_unity ; :: according to MONOID_0:def_9,MONOID_0:def_20 ::_thesis: for a, b being Element of the carrier of H st the multF of H . (a,b) = the_unity_wrt the multF of H holds
( a = b & b = the_unity_wrt the multF of H )
let a, b be Element of H; ::_thesis: ( the multF of H . (a,b) = the_unity_wrt the multF of H implies ( a = b & b = the_unity_wrt the multF of H ) )
 H1(H) c= H1(G) by Th23;
then reconsider a9 = a, b9 = b as Element of G by TARSKI:def_3;
A5: H2(H) . (a,b) = a * b
.= a9 * b9 by Th25
.= H2(G) . (a9,b9) ;
 the_unity_wrt H2(G) = the_unity_wrt H2(H) by A1, A4, Th30;
hence  ( the multF of H . (a,b) = the_unity_wrt the multF of H implies ( a = b & b = the_unity_wrt the multF of H ) ) by A3, A5; ::_thesis: verum
end;

theorem Th37: :: MONOID_0:37
for M being non empty well-unital uniquely-decomposable multLoopStr
for N being non empty MonoidalSubStr of M holds N is uniquely-decomposable
proof
let M be non empty well-unital uniquely-decomposable multLoopStr ; ::_thesis: for N being non empty MonoidalSubStr of M holds N is uniquely-decomposable
let N be non empty MonoidalSubStr of M; ::_thesis: N is uniquely-decomposable
A1: H3(M) = H3(N) by Def25;
 ( N is SubStr of M & H3(M) = the_unity_wrt H2(M) ) by Th17, Th21;
hence  N is uniquely-decomposable by A1, Th36; ::_thesis: verum
end;

registration
let G be non empty constituted-Functions multMagma ;
cluster non empty  ->  non empty constituted-Functions for SubStr of G;
coherence
 for b1 being non empty SubStr of G holds b1 is constituted-Functions
proof
let H be non empty SubStr of G; ::_thesis: H is constituted-Functions
let a be Element of H; :: according to MONOID_0:def_1 ::_thesis: a is Function
 H1(H) c= H1(G) by Th23;
then  a is Element of G by TARSKI:def_3;
hence  a is Function ; ::_thesis: verum
end;
cluster non empty  ->  non empty constituted-Functions for MonoidalSubStr of G;
coherence
 for b1 being non empty MonoidalSubStr of G holds b1 is constituted-Functions
proof
let H be non empty MonoidalSubStr of G; ::_thesis: H is constituted-Functions
let a be Element of H; :: according to MONOID_0:def_1 ::_thesis: a is Function
 H1(H) c= H1(G) by Th23;
then  a is Element of G by TARSKI:def_3;
hence  a is Function ; ::_thesis: verum
end;
end;

registration
let G be non empty constituted-FinSeqs multMagma ;
cluster non empty  ->  non empty constituted-FinSeqs for SubStr of G;
coherence
 for b1 being non empty SubStr of G holds b1 is constituted-FinSeqs
proof
let H be non empty SubStr of G; ::_thesis: H is constituted-FinSeqs
let a be Element of H; :: according to MONOID_0:def_2 ::_thesis: a is FinSequence
 H1(H) c= H1(G) by Th23;
then  a is Element of G by TARSKI:def_3;
hence  a is FinSequence ; ::_thesis: verum
end;
cluster non empty  ->  non empty constituted-FinSeqs for MonoidalSubStr of G;
coherence
 for b1 being non empty MonoidalSubStr of G holds b1 is constituted-FinSeqs
proof
let H be non empty MonoidalSubStr of G; ::_thesis: H is constituted-FinSeqs
let a be Element of H; :: according to MONOID_0:def_2 ::_thesis: a is FinSequence
 H1(H) c= H1(G) by Th23;
then  a is Element of G by TARSKI:def_3;
hence  a is FinSequence ; ::_thesis: verum
end;
end;

registration
let M be non empty well-unital multLoopStr ;
cluster non empty  ->  non empty well-unital for MonoidalSubStr of M;
coherence
 for b1 being non empty MonoidalSubStr of M holds b1 is well-unital by Th31;
end;

registration
let G be non empty commutative multMagma ;
cluster non empty  ->  non empty commutative for SubStr of G;
coherence
 for b1 being non empty SubStr of G holds b1 is commutative by Th32;
cluster non empty  ->  non empty commutative for MonoidalSubStr of G;
coherence
 for b1 being non empty MonoidalSubStr of G holds b1 is commutative
proof
let N be non empty MonoidalSubStr of G; ::_thesis: N is commutative
 N is SubStr of G by Th21;
hence  N is commutative ; ::_thesis: verum
end;
end;

registration
let G be non empty associative multMagma ;
cluster non empty  ->  non empty associative for SubStr of G;
coherence
 for b1 being non empty SubStr of G holds b1 is associative by Th33;
cluster non empty  ->  non empty associative for MonoidalSubStr of G;
coherence
 for b1 being non empty MonoidalSubStr of G holds b1 is associative
proof
let N be non empty MonoidalSubStr of G; ::_thesis: N is associative
 N is SubStr of G by Th21;
hence  N is associative ; ::_thesis: verum
end;
end;

registration
let G be non empty idempotent multMagma ;
cluster non empty  ->  non empty idempotent for SubStr of G;
coherence
 for b1 being non empty SubStr of G holds b1 is idempotent by Th34;
cluster non empty  ->  non empty idempotent for MonoidalSubStr of G;
coherence
 for b1 being non empty MonoidalSubStr of G holds b1 is idempotent
proof
let N be non empty MonoidalSubStr of G; ::_thesis: N is idempotent
 N is SubStr of G by Th21;
hence  N is idempotent ; ::_thesis: verum
end;
end;

registration
let G be non empty cancelable multMagma ;
cluster non empty  ->  non empty cancelable for SubStr of G;
coherence
 for b1 being non empty SubStr of G holds b1 is cancelable by Th35;
cluster non empty  ->  non empty cancelable for MonoidalSubStr of G;
coherence
 for b1 being non empty MonoidalSubStr of G holds b1 is cancelable
proof
let N be non empty MonoidalSubStr of G; ::_thesis: N is cancelable
 N is SubStr of G by Th21;
hence  N is cancelable ; ::_thesis: verum
end;
end;

registration
let M be non empty well-unital uniquely-decomposable multLoopStr ;
cluster non empty  ->  non empty uniquely-decomposable for MonoidalSubStr of M;
coherence
 for b1 being non empty MonoidalSubStr of M holds b1 is uniquely-decomposable by Th37;
end;

Lm6: now__::_thesis:_for_G_being_non_empty_multMagma_
for_D_being_non_empty_Subset_of_G_st_(_for_x,_y_being_Element_of_D_holds_x_*_y_in_D_)_holds_
ex_H_being_non_empty_strict_SubStr_of_G_st_the_carrier_of_H_=_D
let G be non empty multMagma ; ::_thesis: for D being non empty Subset of G st ( for x, y being Element of D holds x * y in D ) holds
ex H being non empty strict SubStr of G st the carrier of H = D
let D be non empty Subset of G; ::_thesis: ( ( for x, y being Element of D holds x * y in D ) implies ex H being non empty strict SubStr of G st the carrier of H = D )
assume A1: for x, y being Element of D holds x * y in D ; ::_thesis: ex H being non empty strict SubStr of G st the carrier of H = D
thus  ex H being non empty strict SubStr of G st the carrier of H = D ::_thesis: verum
proof
set op = the multF of G;
set carr = the carrier of G;
A2: dom the multF of G = [: the carrier of G, the carrier of G:] by FUNCT_2:def_1;
A3: rng ( the multF of G || D) c= D
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in rng ( the multF of G || D) or x in D )
assume  x in rng ( the multF of G || D) ; ::_thesis: x in D
then consider y being set  such that
A4: y in dom ( the multF of G || D) and
A5: x = ( the multF of G || D) . y by FUNCT_1:def_3;
reconsider y = y as Element of [:D,D:] by A2, A4, RELAT_1:62;
reconsider y1 = y `1 , y2 = y `2 as Element of D ;
 y = [y1,y2] by MCART_1:21;
then  x = y1 * y2 by A4, A5, FUNCT_1:47;
hence  x in D by A1; ::_thesis: verum
end;
 dom ( the multF of G || D) = [:D,D:] by A2, RELAT_1:62;
then reconsider f = the multF of G || D as BinOp of D by A3, FUNCT_2:def_1, RELSET_1:4;
 f c= the multF of G by RELAT_1:59;
then reconsider H = multMagma(# D,f #) as non empty strict SubStr of G by Def23;
take  H ; ::_thesis: the carrier of H = D
thus  the carrier of H = D ; ::_thesis: verum
end;
end;

scheme :: MONOID_0:sch 1
SubStrEx2{ F1() ->  non empty multMagma , P1[ set ] } :
 ex H being non empty strict SubStr of F1() st
for x being Element of F1() holds
( x in the carrier of H iff P1[x] )
provided
A1: for x, y being Element of F1() st P1[x] & P1[y] holds
P1[x * y] and
A2: ex x being Element of F1() st P1[x]
proof
consider X being set  such that
A3: for x being set holds
( x in X iff ( x in H1(F1()) & P1[x] ) ) from XBOOLE_0:sch_1();
reconsider X = X as non empty set by A2, A3;
 X c= H1(F1())
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in X or x in H1(F1()) )
thus  ( not x in X or x in H1(F1()) ) by A3; ::_thesis: verum
end;
then reconsider X = X as non empty Subset of F1() ;
A4: now__::_thesis:_for_x,_y_being_Element_of_X_holds_x_*_y_in_X
let x, y be Element of X; ::_thesis: x * y in X
 ( P1[x] & P1[y] ) by A3;
then  P1[x * y] by A1;
hence  x * y in X by A3; ::_thesis: verum
end;
consider H being non empty strict SubStr of F1() such that
A5: the carrier of H = X by Lm6, A4;
take  H ; ::_thesis: for x being Element of F1() holds
( x in the carrier of H iff P1[x] )
thus  for x being Element of F1() holds
( x in the carrier of H iff P1[x] ) by A3, A5; ::_thesis: verum
end;

scheme :: MONOID_0:sch 2
MonoidalSubStrEx2{ F1() ->  non empty multLoopStr , P1[ set ] } :
 ex M being non empty strict MonoidalSubStr of F1() st
for x being Element of F1() holds
( x in the carrier of M iff P1[x] )
provided
A1: for x, y being Element of F1() st P1[x] & P1[y] holds
P1[x * y] and
A2: P1[ 1. F1()]
proof
reconsider G = F1() as non empty multMagma ;
A3: ex x being Element of G st P1[x] by A2;
A4: for x, y being Element of G st P1[x] & P1[y] holds
P1[x * y] by A1;
consider H being non empty strict SubStr of G such that
A5: for x being Element of G holds
( x in the carrier of H iff P1[x] ) from MONOID_0:sch_1(A4, A3);
reconsider e = 1. F1() as Element of H by A2, A5;
set M = multLoopStr(# H1(H),H2(H),e #);
 ( 1. F1() = 1. multLoopStr(# H1(H),H2(H),e #) & the multF of H c= the multF of F1() ) by Def23;
then reconsider M = multLoopStr(# H1(H),H2(H),e #) as non empty strict MonoidalSubStr of F1() by Def25;
take  M ; ::_thesis: for x being Element of F1() holds
( x in the carrier of M iff P1[x] )
thus  for x being Element of F1() holds
( x in the carrier of M iff P1[x] ) by A5; ::_thesis: verum
end;

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

begin

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

:: deftheorem  defines <REAL,+> MONOID_0:def_26_:_
 <REAL,+> = multMagma(# REAL,addreal #);

registration
cluster <REAL,+>  ->  non empty strict unital associative commutative invertible cancelable ;
coherence
 ( <REAL,+> is unital & <REAL,+> is associative & <REAL,+> is invertible & <REAL,+> is commutative & <REAL,+> is cancelable & <REAL,+> is strict ) by GROUP_1:46;
end;

theorem :: MONOID_0:38
for x being set holds
( x is Element of <REAL,+> iff x is Real ) ;

theorem Th39: :: MONOID_0:39
for N being non empty SubStr of <REAL,+>
for a, b being Element of N
for x, y being Real st a = x & b = y holds
a * b = x + y
proof
let N be non empty SubStr of <REAL,+> ; ::_thesis: for a, b being Element of N
for x, y being Real st a = x & b = y holds
a * b = x + y
let a, b be Element of N; ::_thesis: for x, y being Real st a = x & b = y holds
a * b = x + y
 H1(N) c= H1( <REAL,+> ) by Th23;
then reconsider a9 = a, b9 = b as Element of <REAL,+> by TARSKI:def_3;
 a * b = a9 * b9 by Th25;
hence  for x, y being Real st a = x & b = y holds
a * b = x + y by BINOP_2:def_9; ::_thesis: verum
end;

theorem Th40: :: MONOID_0:40
for N being non empty unital SubStr of <REAL,+> holds the_unity_wrt the multF of N = 0
proof
let N be non empty unital SubStr of <REAL,+> ; ::_thesis: the_unity_wrt the multF of N = 0
consider a being Element of N such that
A1: for b being Element of N holds
( a * b = b & b * a = b ) by Th6;
 H1(N) c= REAL by Th23;
then reconsider x = a as Real by TARSKI:def_3;
now__::_thesis:_for_b_being_Element_of_N_holds_
(_H2(N)_._(a,b)_=_b_&_H2(N)_._(b,a)_=_b_)
let b be Element of N; ::_thesis: ( H2(N) . (a,b) = b & H2(N) . (b,a) = b )
 ( a * b = H2(N) . (a,b) & b * a = H2(N) . (b,a) ) ;
hence  ( H2(N) . (a,b) = b & H2(N) . (b,a) = b ) by A1; ::_thesis: verum
end;
then A2: a is_a_unity_wrt H2(N) by BINOP_1:3;
x + 0 = a * a by A1
.= x + x by Th39 ;
hence  the_unity_wrt the multF of N = 0 by A2, BINOP_1:def_8; ::_thesis: verum
end;

registration
let G be non empty unital multMagma ;
cluster non empty associative invertible  ->  non empty unital Group-like cancelable for SubStr of G;
coherence
 for b1 being non empty SubStr of G st b1 is associative & b1 is invertible holds
( b1 is unital & b1 is cancelable & b1 is Group-like ) ;
end;

definition
:: original: INT.Group
redefine func INT.Group  ->  non empty strict SubStr of <REAL,+> ;
coherence
 INT.Group is non empty strict SubStr of <REAL,+>
proof
 dom addreal = [:REAL,REAL:] by FUNCT_2:def_1;
then A1: dom (addreal || INT) = [:INT,INT:] by NUMBERS:15, RELAT_1:62, ZFMISC_1:96;
A2: now__::_thesis:_for_x_being_set_st_x_in_[:INT,INT:]_holds_
addint_._x_=_(addreal_||_INT)_._x
let x be set ; ::_thesis: ( x in [:INT,INT:] implies addint . x = (addreal || INT) . x )
assume A3: x in [:INT,INT:] ; ::_thesis: addint . x = (addreal || INT) . x
then A4: x = [(x `1),(x `2)] by MCART_1:21;
reconsider i1 = x `1 , i2 = x `2 as Element of INT by A3, MCART_1:10;
thus addint . x = addint . (i1,i2) by A3, MCART_1:21
.= addreal . (i1,i2) by GR_CY_1:def_1
.= (addreal || INT) . x by A1, A3, A4, FUNCT_1:47 ; ::_thesis: verum
end;
 dom addint = [:INT,INT:] by FUNCT_2:def_1;
then  addint = addreal || INT by A1, A2, FUNCT_1:2;
then  H2( INT.Group ) c= H2( <REAL,+> ) by GR_CY_1:def_3, RELAT_1:59;
hence  INT.Group is non empty strict SubStr of <REAL,+> by Def23; ::_thesis: verum
end;
end;

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

theorem :: MONOID_0:42
for x being set holds
( x is Element of INT.Group iff x is Integer ) by GR_CY_1:def_3, INT_1:def_2;

definition
func <NAT,+>  ->  non empty strict unital uniquely-decomposable SubStr of INT.Group  means :Def27: :: MONOID_0:def 27
 the carrier of it = NAT ;
existence
 ex b1 being non empty strict unital uniquely-decomposable SubStr of INT.Group st the carrier of b1 = NAT
proof
set f = addint || NAT;
 dom addint = [:INT,INT:] by FUNCT_2:def_1;
then A1: dom (addint || NAT) = [:NAT,NAT:] by NUMBERS:17, RELAT_1:62, ZFMISC_1:96;
 rng (addint || NAT) c= NAT
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in rng (addint || NAT) or x in NAT )
assume  x in rng (addint || NAT) ; ::_thesis: x in NAT
then consider y being set  such that
A2: y in dom (addint || NAT) and
A3: x = (addint || NAT) . y by FUNCT_1:def_3;
reconsider n1 = y `1 , n2 = y `2 as Element of NAT by A1, A2, MCART_1:10;
reconsider i1 = n1, i2 = n2 as Integer ;
x = addint . y by A2, A3, FUNCT_1:47
.= addint . (i1,i2) by A1, A2, MCART_1:21
.= n1 + n2 by BINOP_2:def_20 ;
hence  x in NAT ; ::_thesis: verum
end;
then reconsider f = addint || NAT as BinOp of NAT by A1, FUNCT_2:def_1, RELSET_1:4;
 f c= H2( INT.Group ) by GR_CY_1:def_3, RELAT_1:59;
then reconsider N = multMagma(# NAT,f #) as non empty strict SubStr of INT.Group by Def23;
reconsider a = 0 as Element of N ;
A4: now__::_thesis:_for_b_being_Element_of_N_holds_
(_a_*_b_=_b_&_b_*_a_=_b_)
let b be Element of N; ::_thesis: ( a * b = b & b * a = b )
reconsider n = b as Element of NAT ;
thus a * b = 0 + n by Th39
.= b ; ::_thesis: b * a = b
thus b * a = n + 0 by Th39
.= b ; ::_thesis: verum
end;
now__::_thesis:_for_b_being_Element_of_N_holds_
(_H2(N)_._(a,b)_=_b_&_H2(N)_._(b,a)_=_b_)
let b be Element of N; ::_thesis: ( H2(N) . (a,b) = b & H2(N) . (b,a) = b )
thus H2(N) . (a,b) = a * b
.= b by A4 ; ::_thesis: H2(N) . (b,a) = b
thus H2(N) . (b,a) = b * a
.= b by A4 ; ::_thesis: verum
end;
then A5: a is_a_unity_wrt H2(N) by BINOP_1:3;
then A6: the_unity_wrt H2(N) = a by BINOP_1:def_8;
A7: now__::_thesis:_for_a,_b_being_Element_of_N_st_a_*_b_=_the_unity_wrt_H2(N)_holds_
(_a_=_b_&_b_=_the_unity_wrt_H2(N)_)
let a, b be Element of N; ::_thesis: ( a * b = the_unity_wrt H2(N) implies ( a = b & b = the_unity_wrt H2(N) ) )
assume A8: a * b = the_unity_wrt H2(N) ; ::_thesis: ( a = b & b = the_unity_wrt H2(N) )
reconsider n = a, m = b as Element of NAT ;
A9: a * b = n + m by Th39;
then  a = 0 by A6, A8, NAT_1:7;
hence  ( a = b & b = the_unity_wrt H2(N) ) by A5, A8, A9, BINOP_1:def_8; ::_thesis: verum
end;
A10: N is unital by A4, Th6;
then  N is uniquely-decomposable by A7, Th14;
hence  ex b1 being non empty strict unital uniquely-decomposable SubStr of INT.Group st the carrier of b1 = NAT by A10; ::_thesis: verum
end;
uniqueness
 for b1, b2 being non empty strict unital uniquely-decomposable SubStr of INT.Group st the carrier of b1 = NAT & the carrier of b2 = NAT holds
b1 = b2 by Th26;
end;

:: deftheorem Def27 defines <NAT,+> MONOID_0:def_27_:_
 for b1 being non empty strict unital uniquely-decomposable SubStr of INT.Group holds
( b1 = <NAT,+> iff the carrier of b1 = NAT );

definition
func <NAT,+,0>  ->  non empty strict well-unital MonoidalExtension of <NAT,+>  means :: MONOID_0:def 28
verum;
existence
 ex b1 being non empty strict well-unital MonoidalExtension of <NAT,+> st verum ;
uniqueness
 for b1, b2 being non empty strict well-unital MonoidalExtension of <NAT,+> holds b1 = b2 by Th20;
end;

:: deftheorem  defines <NAT,+,0> MONOID_0:def_28_:_
 for b1 being non empty strict well-unital MonoidalExtension of <NAT,+> holds
( b1 = <NAT,+,0> iff verum );

definition
redefine func addnat  equals :: MONOID_0:def 29
 the multF of <NAT,+>;
compatibility
 for b1 being Element of bool [:[:NAT,NAT:],NAT:] holds
( b1 = addnat iff b1 = the multF of <NAT,+> )
proof
let b be BinOp of NAT; ::_thesis: ( b = addnat iff b = the multF of <NAT,+> )
A1: the carrier of <NAT,+> = NAT by Def27;
now__::_thesis:_for_n1,_n2_being_Element_of_NAT_holds_addnat_._(n1,n2)_=_the_multF_of_<NAT,+>_._(n1,n2)
let n1, n2 be Element of NAT ; ::_thesis: addnat . (n1,n2) = the multF of <NAT,+> . (n1,n2)
thus addnat . (n1,n2) = n1 + n2 by BINOP_2:def_23
.= addint . (n1,n2) by BINOP_2:def_20
.= (addint || NAT) . [n1,n2] by FUNCT_1:49
.= the multF of <NAT,+> . (n1,n2) by A1, Th24, GR_CY_1:def_3 ; ::_thesis: verum
end;
hence  ( b = addnat iff b = the multF of <NAT,+> ) by A1, BINOP_1:2; ::_thesis: verum
end;
end;

:: deftheorem  defines addnat MONOID_0:def_29_:_
 addnat = the multF of <NAT,+>;

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

theorem :: MONOID_0:44
for x being set holds
( x is Element of <NAT,+,0> iff x is Element of NAT )
proof
let x be set ; ::_thesis: ( x is Element of <NAT,+,0> iff x is Element of NAT )
H1( <NAT,+,0> ) = H1( <NAT,+> ) by Th18
.= NAT by Def27 ;
hence  ( x is Element of <NAT,+,0> iff x is Element of NAT ) ; ::_thesis: verum
end;

theorem :: MONOID_0:45
for n1, n2 being Element of NAT
for m1, m2 being Element of <NAT,+,0> st n1 = m1 & n2 = m2 holds
m1 * m2 = n1 + n2
proof
 H2( <NAT,+,0> ) = H2( <NAT,+> ) by Th18;
then  <NAT,+,0> is SubStr of <NAT,+> by Def23;
hence  for n1, n2 being Element of NAT
for m1, m2 being Element of <NAT,+,0> st n1 = m1 & n2 = m2 holds
m1 * m2 = n1 + n2 by Th39; ::_thesis: verum
end;

theorem :: MONOID_0:46
<NAT,+,0> = multLoopStr(# NAT,addnat,0 #)
proof
set N = <NAT,+,0> ;
 ( multMagma(# the carrier of <NAT,+,0>, the multF of <NAT,+,0> #) = <NAT,+> & the_unity_wrt H2( <NAT,+,0> ) = H3( <NAT,+,0> ) ) by Def22, Th17;
hence  <NAT,+,0> = multLoopStr(# NAT,addnat,0 #) by Th40, Th43; ::_thesis: verum
end;

theorem :: MONOID_0:47
( addnat = addreal || NAT & addnat = addint || NAT )
proof
 H1( <NAT,+> ) = NAT by Def27;
hence  ( addnat = addreal || NAT & addnat = addint || NAT ) by Th24, GR_CY_1:def_3; ::_thesis: verum
end;

theorem :: MONOID_0:48
( 0 is_a_unity_wrt addnat & addnat is uniquely-decomposable )
proof
 ( the_unity_wrt addnat = 0 & ex n being Element of NAT st n is_a_unity_wrt addnat ) by Th40, Th43, SETWISEO:def_2;
hence  0 is_a_unity_wrt addnat by BINOP_1:def_8; ::_thesis: addnat is uniquely-decomposable
thus  addnat is uniquely-decomposable by Def20, Th43; ::_thesis: verum
end;

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

:: deftheorem  defines <REAL,*> MONOID_0:def_30_:_
 <REAL,*> = multMagma(# REAL,multreal #);

theorem :: MONOID_0:49
for x being set holds
( x is Element of <REAL,*> iff x is Real ) ;

theorem Th50: :: MONOID_0:50
for N being non empty SubStr of <REAL,*>
for a, b being Element of N
for x, y being Real st a = x & b = y holds
a * b = x * y
proof
let N be non empty SubStr of <REAL,*> ; ::_thesis: for a, b being Element of N
for x, y being Real st a = x & b = y holds
a * b = x * y
let a, b be Element of N; ::_thesis: for x, y being Real st a = x & b = y holds
a * b = x * y
 H1(N) c= H1( <REAL,*> ) by Th23;
then reconsider a9 = a, b9 = b as Element of <REAL,*> by TARSKI:def_3;
 a * b = a9 * b9 by Th25;
hence  for x, y being Real st a = x & b = y holds
a * b = x * y by BINOP_2:def_11; ::_thesis: verum
end;

theorem :: MONOID_0:51
for N being non empty unital SubStr of <REAL,*> holds
( the_unity_wrt the multF of N = 0 or the_unity_wrt the multF of N = 1 )
proof
let N be non empty unital SubStr of <REAL,*> ; ::_thesis: ( the_unity_wrt the multF of N = 0 or the_unity_wrt the multF of N = 1 )
set e = the_unity_wrt H2(N);
 H1(N) c= H1( <REAL,*> ) by Th23;
then reconsider x = the_unity_wrt H2(N) as Real by TARSKI:def_3;
 the_unity_wrt H2(N) is_a_unity_wrt H2(N) by Th4;
then  the_unity_wrt H2(N) = (the_unity_wrt H2(N)) * (the_unity_wrt H2(N)) by BINOP_1:3
.= x * x by Th50 ;
then  x * 1 = x * x ;
hence  ( the_unity_wrt the multF of N = 0 or the_unity_wrt the multF of N = 1 ) by XCMPLX_1:5; ::_thesis: verum
end;

definition
func <NAT,*>  ->  non empty strict unital uniquely-decomposable SubStr of <REAL,*>  means :Def31: :: MONOID_0:def 31
 the carrier of it = NAT ;
existence
 ex b1 being non empty strict unital uniquely-decomposable SubStr of <REAL,*> st the carrier of b1 = NAT
proof
set f = multreal || NAT;
 dom multreal = [:REAL,REAL:] by FUNCT_2:def_1;
then A1: dom (multreal || NAT) = [:NAT,NAT:] by RELAT_1:62;
 rng (multreal || NAT) c= NAT
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in rng (multreal || NAT) or x in NAT )
assume  x in rng (multreal || NAT) ; ::_thesis: x in NAT
then consider y being set  such that
A2: y in dom (multreal || NAT) and
A3: x = (multreal || NAT) . y by FUNCT_1:def_3;
reconsider n1 = y `1 , n2 = y `2 as Element of NAT by A1, A2, MCART_1:10;
x = multreal . y by A2, A3, FUNCT_1:47
.= multreal . (n1,n2) by A1, A2, MCART_1:21
.= n1 * n2 by BINOP_2:def_11 ;
hence  x in NAT ; ::_thesis: verum
end;
then reconsider f = multreal || NAT as BinOp of NAT by A1, FUNCT_2:def_1, RELSET_1:4;
 f c= H2( <REAL,*> ) by RELAT_1:59;
then reconsider N = multMagma(# NAT,f #) as non empty strict SubStr of <REAL,*> by Def23;
reconsider a = 1 as Element of N ;
A4: now__::_thesis:_for_b_being_Element_of_N_holds_
(_a_*_b_=_b_&_b_*_a_=_b_)
let b be Element of N; ::_thesis: ( a * b = b & b * a = b )
reconsider n = b as Element of NAT ;
thus a * b = 1 * n by Th50
.= b ; ::_thesis: b * a = b
thus b * a = n * 1 by Th50
.= b ; ::_thesis: verum
end;
now__::_thesis:_for_b_being_Element_of_N_holds_
(_H2(N)_._(a,b)_=_b_&_H2(N)_._(b,a)_=_b_)
let b be Element of N; ::_thesis: ( H2(N) . (a,b) = b & H2(N) . (b,a) = b )
thus H2(N) . (a,b) = a * b
.= b by A4 ; ::_thesis: H2(N) . (b,a) = b
thus H2(N) . (b,a) = b * a
.= b by A4 ; ::_thesis: verum
end;
then A5: a is_a_unity_wrt H2(N) by BINOP_1:3;
then A6: the_unity_wrt H2(N) = a by BINOP_1:def_8;
A7: now__::_thesis:_for_a,_b_being_Element_of_N_st_a_*_b_=_the_unity_wrt_H2(N)_holds_
(_a_=_b_&_b_=_the_unity_wrt_H2(N)_)
let a, b be Element of N; ::_thesis: ( a * b = the_unity_wrt H2(N) implies ( a = b & b = the_unity_wrt H2(N) ) )
assume A8: a * b = the_unity_wrt H2(N) ; ::_thesis: ( a = b & b = the_unity_wrt H2(N) )
reconsider n = a, m = b as Element of NAT ;
A9: a * b = n * m by Th50;
then  a = 1 by A6, A8, NAT_1:15;
hence  ( a = b & b = the_unity_wrt H2(N) ) by A5, A8, A9, BINOP_1:def_8; ::_thesis: verum
end;
A10: N is unital by A4, Th6;
then  N is uniquely-decomposable by A7, Th14;
hence  ex b1 being non empty strict unital uniquely-decomposable SubStr of <REAL,*> st the carrier of b1 = NAT by A10; ::_thesis: verum
end;
uniqueness
 for b1, b2 being non empty strict unital uniquely-decomposable SubStr of <REAL,*> st the carrier of b1 = NAT & the carrier of b2 = NAT holds
b1 = b2 by Th26;
end;

:: deftheorem Def31 defines <NAT,*> MONOID_0:def_31_:_
 for b1 being non empty strict unital uniquely-decomposable SubStr of <REAL,*> holds
( b1 = <NAT,*> iff the carrier of b1 = NAT );

definition
func <NAT,*,1>  ->  non empty strict well-unital MonoidalExtension of <NAT,*>  means :: MONOID_0:def 32
verum;
uniqueness
 for b1, b2 being non empty strict well-unital MonoidalExtension of <NAT,*> holds b1 = b2 by Th20;
existence
 ex b1 being non empty strict well-unital MonoidalExtension of <NAT,*> st verum ;
end;

:: deftheorem  defines <NAT,*,1> MONOID_0:def_32_:_
 for b1 being non empty strict well-unital MonoidalExtension of <NAT,*> holds
( b1 = <NAT,*,1> iff verum );

definition
redefine func multnat  equals :: MONOID_0:def 33
 the multF of <NAT,*>;
compatibility
 for b1 being Element of bool [:[:NAT,NAT:],NAT:] holds
( b1 = multnat iff b1 = the multF of <NAT,*> )
proof
let b be BinOp of NAT; ::_thesis: ( b = multnat iff b = the multF of <NAT,*> )
A1: the carrier of <NAT,*> = NAT by Def31;
now__::_thesis:_for_n1,_n2_being_Element_of_NAT_holds_multnat_._(n1,n2)_=_the_multF_of_<NAT,*>_._(n1,n2)
let n1, n2 be Element of NAT ; ::_thesis: multnat . (n1,n2) = the multF of <NAT,*> . (n1,n2)
thus multnat . (n1,n2) = n1 * n2 by BINOP_2:def_24
.= multreal . (n1,n2) by BINOP_2:def_11
.= (multreal || NAT) . [n1,n2] by FUNCT_1:49
.= the multF of <NAT,*> . (n1,n2) by A1, Th24 ; ::_thesis: verum
end;
hence  ( b = multnat iff b = the multF of <NAT,*> ) by A1, BINOP_1:2; ::_thesis: verum
end;
end;

:: deftheorem  defines multnat MONOID_0:def_33_:_
 multnat = the multF of <NAT,*>;

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

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

theorem Th54: :: MONOID_0:54
the_unity_wrt the multF of <NAT,*> = 1
proof
 H1( <NAT,*> ) = NAT by Def31;
hence  the_unity_wrt the multF of <NAT,*> = 1 by Th30, BINOP_2:7; ::_thesis: verum
end;

theorem :: MONOID_0:55
for n1, n2 being Element of NAT
for m1, m2 being Element of <NAT,*,1> st n1 = m1 & n2 = m2 holds
m1 * m2 = n1 * n2
proof
let n1, n2 be Element of NAT ; ::_thesis: for m1, m2 being Element of <NAT,*,1> st n1 = m1 & n2 = m2 holds
m1 * m2 = n1 * n2
let m1, m2 be Element of <NAT,*,1>; ::_thesis: ( n1 = m1 & n2 = m2 implies m1 * m2 = n1 * n2 )
 multMagma(# the carrier of <NAT,*,1>, the multF of <NAT,*,1> #) = <NAT,*> by Def22;
then reconsider x1 = m1, x2 = m2 as Element of <NAT,*> ;
 x1 * x2 = m1 * m2 by Th18;
hence  ( n1 = m1 & n2 = m2 implies m1 * m2 = n1 * n2 ) by Th50; ::_thesis: verum
end;

theorem :: MONOID_0:56
<NAT,*,1> = multLoopStr(# NAT,multnat,1 #)
proof
set N = <NAT,*,1> ;
 ( multMagma(# the carrier of <NAT,*,1>, the multF of <NAT,*,1> #) = <NAT,*> & the_unity_wrt H2( <NAT,*,1> ) = H3( <NAT,*,1> ) ) by Def22, Th17;
hence  <NAT,*,1> = multLoopStr(# NAT,multnat,1 #) by Def31, Th54; ::_thesis: verum
end;

theorem :: MONOID_0:57
multnat = multreal || NAT by Th24, Th52;

theorem :: MONOID_0:58
( 1 is_a_unity_wrt multnat & multnat is uniquely-decomposable )
proof
 ex n being Element of NAT st n is_a_unity_wrt multnat by SETWISEO:def_2;
hence  1 is_a_unity_wrt multnat by Th52, Th54, BINOP_1:def_8; ::_thesis: multnat is uniquely-decomposable
thus  multnat is uniquely-decomposable by Def20, Th52; ::_thesis: verum
end;

begin

definition
let D be non empty set ;
funcD *+^  ->  non empty strict unital associative constituted-FinSeqs cancelable uniquely-decomposable multMagma  means :Def34: :: MONOID_0:def 34
( the carrier of it = D * & ( for p, q being Element of it holds p [*] q = p ^ q ) );
existence
 ex b1 being non empty strict unital associative constituted-FinSeqs cancelable uniquely-decomposable multMagma st
( the carrier of b1 = D * & ( for p, q being Element of b1 holds p [*] q = p ^ q ) )
proof
deffunc H4( Element of D * , Element of D * ) ->  Element of D * = $1 ^ $2;
consider f being BinOp of (D *) such that
A1: for a, b being Element of D * holds f . (a,b) = H4(a,b) from BINOP_1:sch_4();
set G = multMagma(# (D *),f #);
 multMagma(# (D *),f #) is constituted-FinSeqs
proof
let x be Element of multMagma(# (D *),f #); :: according to MONOID_0:def_2 ::_thesis: x is FinSequence
thus  x is FinSequence ; ::_thesis: verum
end;
then reconsider G = multMagma(# (D *),f #) as non empty strict constituted-FinSeqs multMagma ;
 ( G is unital & G is associative & G is cancelable & G is uniquely-decomposable )
proof
set N = G;
set f = H2(G);
 <*> D = {} ;
then reconsider a = {} as Element of G by FINSEQ_1:def_11;
A2: now__::_thesis:_for_b_being_Element_of_G_holds_
(_a_[*]_b_=_b_&_b_[*]_a_=_b_)
let b be Element of G; ::_thesis: ( a [*] b = b & b [*] a = b )
thus a [*] b = a ^ b by A1
.= b by FINSEQ_1:34 ; ::_thesis: b [*] a = b
thus b [*] a = b ^ a by A1
.= b by FINSEQ_1:34 ; ::_thesis: verum
end;
hence  G is unital by Th6; ::_thesis: ( G is associative & G is cancelable & G is uniquely-decomposable )
now__::_thesis:_for_a,_b,_c_being_Element_of_G_holds_(a_*_b)_*_c_=_a_*_(b_*_c)
let a, b, c be Element of G; ::_thesis: (a * b) * c = a * (b * c)
reconsider p = a [*] b, q = b [*] c as Element of G ;
thus (a * b) * c = p ^ c by A1
.= (a ^ b) ^ c by A1
.= a ^ (b ^ c) by FINSEQ_1:32
.= a ^ q by A1
.= a * (b * c) by A1 ; ::_thesis: verum
end;
hence  G is associative by Lm2; ::_thesis: ( G is cancelable & G is uniquely-decomposable )
now__::_thesis:_for_a,_b,_c_being_Element_of_G_st_(_a_*_b_=_a_*_c_or_b_*_a_=_c_*_a_)_holds_
b_=_c
let a, b, c be Element of G; ::_thesis: ( ( a * b = a * c or b * a = c * a ) implies b = c )
A3: ( b * a = b ^ a & c * a = c ^ a ) by A1;
 ( a * b = a ^ b & a * c = a ^ c ) by A1;
hence  ( ( a * b = a * c or b * a = c * a ) implies b = c ) by A3, FINSEQ_1:33; ::_thesis: verum
end;
hence  G is cancelable by Th13; ::_thesis: G is uniquely-decomposable
 G is unital by A2, Th6;
hence  H2(G) is having_a_unity ; :: according to MONOID_0:def_9,MONOID_0:def_20 ::_thesis: for a, b being Element of the carrier of G st the multF of G . (a,b) = the_unity_wrt the multF of G holds
( a = b & b = the_unity_wrt the multF of G )
let a9, b be Element of G; ::_thesis: ( the multF of G . (a9,b) = the_unity_wrt the multF of G implies ( a9 = b & b = the_unity_wrt the multF of G ) )
now__::_thesis:_for_b_being_Element_of_G_holds_
(_H2(G)_._(a,b)_=_b_&_H2(G)_._(b,a)_=_b_)
let b be Element of G; ::_thesis: ( H2(G) . (a,b) = b & H2(G) . (b,a) = b )
 ( a [*] b = H2(G) . (a,b) & b [*] a = H2(G) . (b,a) ) ;
hence  ( H2(G) . (a,b) = b & H2(G) . (b,a) = b ) by A2; ::_thesis: verum
end;
then A4: a is_a_unity_wrt H2(G) by BINOP_1:3;
assume  H2(G) . (a9,b) = the_unity_wrt H2(G) ; ::_thesis: ( a9 = b & b = the_unity_wrt the multF of G )
then A5: {} = a9 [*] b by A4, BINOP_1:def_8
.= a9 ^ b by A1 ;
then  a = b ;
hence  ( a9 = b & b = the_unity_wrt the multF of G ) by A4, A5, BINOP_1:def_8; ::_thesis: verum
end;
then reconsider G = G as non empty strict unital associative constituted-FinSeqs cancelable uniquely-decomposable multMagma ;
take  G ; ::_thesis: ( the carrier of G = D * & ( for p, q being Element of G holds p [*] q = p ^ q ) )
thus  ( the carrier of G = D * & ( for p, q being Element of G holds p [*] q = p ^ q ) ) by A1; ::_thesis: verum
end;
uniqueness
 for b1, b2 being non empty strict unital associative constituted-FinSeqs cancelable uniquely-decomposable multMagma st the carrier of b1 = D * & ( for p, q being Element of b1 holds p [*] q = p ^ q ) & the carrier of b2 = D * & ( for p, q being Element of b2 holds p [*] q = p ^ q ) holds
b1 = b2
proof
let G1, G2 be non empty strict unital associative constituted-FinSeqs cancelable uniquely-decomposable multMagma ; ::_thesis: ( the carrier of G1 = D * & ( for p, q being Element of G1 holds p [*] q = p ^ q ) & the carrier of G2 = D * & ( for p, q being Element of G2 holds p [*] q = p ^ q ) implies G1 = G2 )
assume that
A6: H1(G1) = D * and
A7: for p, q being Element of G1 holds p [*] q = p ^ q and
A8: H1(G2) = D * and
A9: for p, q being Element of G2 holds p [*] q = p ^ q ; ::_thesis: G1 = G2
set f1 = H2(G1);
set f2 = H2(G2);
now__::_thesis:_for_a,_b_being_Element_of_D_*_holds_H2(G1)_._(a,b)_=_H2(G2)_._(a,b)
let a, b be Element of D * ; ::_thesis: H2(G1) . (a,b) = H2(G2) . (a,b)
reconsider a2 = a, b2 = b as Element of G2 by A8;
reconsider a1 = a, b1 = b as Element of G1 by A6;
reconsider p = a, q = b as Element of D * ;
 ( a2 [*] b2 = p ^ q & a1 [*] b1 = p ^ q ) by A7, A9;
hence  H2(G1) . (a,b) = H2(G2) . (a,b) ; ::_thesis: verum
end;
hence  G1 = G2 by A6, A8, BINOP_1:2; ::_thesis: verum
end;
end;

:: deftheorem Def34 defines *+^ MONOID_0:def_34_:_
 for D being non empty set
for b2 being non empty strict unital associative constituted-FinSeqs cancelable uniquely-decomposable multMagma holds
( b2 = D *+^ iff ( the carrier of b2 = D * & ( for p, q being Element of b2 holds p [*] q = p ^ q ) ) );

definition
let D be non empty set ;
funcD *+^+<0>  ->  non empty strict well-unital MonoidalExtension of D *+^  means :: MONOID_0:def 35
verum;
correctness
existence
ex b1 being non empty strict well-unital MonoidalExtension of D *+^ st verum;
uniqueness
for b1, b2 being non empty strict well-unital MonoidalExtension of D *+^ holds b1 = b2;
by Th20;
funcD -concatenation  ->  BinOp of (D *) equals :: MONOID_0:def 36
 the multF of (D *+^);
correctness
coherence
the multF of (D *+^) is BinOp of (D *);
proof
 H1(D *+^ ) = D * by Def34;
hence  the multF of (D *+^) is BinOp of (D *) ; ::_thesis: verum
end;
end;

:: deftheorem  defines *+^+<0> MONOID_0:def_35_:_
 for D being non empty set
for b2 being non empty strict well-unital MonoidalExtension of D *+^ holds
( b2 = D *+^+<0> iff verum );

:: deftheorem  defines -concatenation MONOID_0:def_36_:_
 for D being non empty set holds D -concatenation = the multF of (D *+^);

theorem :: MONOID_0:59
for D being non empty set holds D *+^ = multMagma(# (D *),(D -concatenation) #) by Def34;

theorem Th60: :: MONOID_0:60
for D being non empty set holds the_unity_wrt the multF of (D *+^) = {}
proof
let D be non empty set ; ::_thesis: the_unity_wrt the multF of (D *+^) = {}
set N = D *+^ ;
set f = H2(D *+^ );
 ( H1(D *+^ ) = D * & {} = <*> D ) by Def34;
then reconsider a = {} as Element of (D *+^) by FINSEQ_1:def_11;
now__::_thesis:_for_b_being_Element_of_(D_*+^)_holds_
(_H2(D_*+^_)_._(a,b)_=_b_&_H2(D_*+^_)_._(b,a)_=_b_)
let b be Element of (D *+^); ::_thesis: ( H2(D *+^ ) . (a,b) = b & H2(D *+^ ) . (b,a) = b )
thus H2(D *+^ ) . (a,b) = a [*] b
.= {} ^ b by Def34
.= b by FINSEQ_1:34 ; ::_thesis: H2(D *+^ ) . (b,a) = b
thus H2(D *+^ ) . (b,a) = b [*] a
.= b ^ {} by Def34
.= b by FINSEQ_1:34 ; ::_thesis: verum
end;
then  a is_a_unity_wrt H2(D *+^ ) by BINOP_1:3;
hence  the_unity_wrt the multF of (D *+^) = {} by BINOP_1:def_8; ::_thesis: verum
end;

theorem :: MONOID_0:61
for D being non empty set holds
( the carrier of (D *+^+<0>) = D * & the multF of (D *+^+<0>) = D -concatenation & 1. (D *+^+<0>) = {} )
proof
let D be non empty set ; ::_thesis: ( the carrier of (D *+^+<0>) = D * & the multF of (D *+^+<0>) = D -concatenation & 1. (D *+^+<0>) = {} )
set M = D *+^+<0> ;
 ( multMagma(# the carrier of (D *+^+<0>), the multF of (D *+^+<0>) #) = D *+^ & the_unity_wrt H2(D *+^+<0> ) = H3(D *+^+<0> ) ) by Def22, Th17;
hence  ( the carrier of (D *+^+<0>) = D * & the multF of (D *+^+<0>) = D -concatenation & 1. (D *+^+<0>) = {} ) by Def34, Th60; ::_thesis: verum
end;

theorem :: MONOID_0:62
for D being non empty set
for a, b being Element of (D *+^+<0>) holds a [*] b = a ^ b
proof
let D be non empty set ; ::_thesis: for a, b being Element of (D *+^+<0>) holds a [*] b = a ^ b
let a, b be Element of (D *+^+<0>); ::_thesis: a [*] b = a ^ b
 multMagma(# the carrier of (D *+^+<0>), the multF of (D *+^+<0>) #) = D *+^ by Def22;
then reconsider p = a, q = b as Element of (D *+^) ;
thus a [*] b = p [*] q by Th18
.= a ^ b by Def34 ; ::_thesis: verum
end;

theorem Th63: :: MONOID_0:63
for D being non empty set
for F being non empty SubStr of D *+^
for p, q being Element of F holds p [*] q = p ^ q
proof
let D be non empty set ; ::_thesis: for F being non empty SubStr of D *+^
for p, q being Element of F holds p [*] q = p ^ q
let F be non empty SubStr of D *+^ ; ::_thesis: for p, q being Element of F holds p [*] q = p ^ q
let p, q be Element of F; ::_thesis: p [*] q = p ^ q
 H1(F) c= H1(D *+^ ) by Th23;
then reconsider p9 = p, q9 = q as Element of (D *+^) by TARSKI:def_3;
thus p [*] q = p9 [*] q9 by Th25
.= p ^ q by Def34 ; ::_thesis: verum
end;

theorem :: MONOID_0:64
for D being non empty set
for F being non empty unital SubStr of D *+^ holds the_unity_wrt the multF of F = {}
proof
let D be non empty set ; ::_thesis: for F being non empty unital SubStr of D *+^ holds the_unity_wrt the multF of F = {}
let F be non empty unital SubStr of D *+^ ; ::_thesis: the_unity_wrt the multF of F = {}
set p = the_unity_wrt H2(F);
reconsider q = the_unity_wrt H2(F) as Element of F ;
q ^ {} = the_unity_wrt H2(F) by FINSEQ_1:34
.= (the_unity_wrt H2(F)) [*] (the_unity_wrt H2(F)) by SETWISEO:15
.= q ^ q by Th63 ;
hence  the_unity_wrt the multF of F = {} by FINSEQ_1:33; ::_thesis: verum
end;

theorem :: MONOID_0:65
for D being non empty set
for F being non empty SubStr of D *+^ st {} is Element of F holds
( F is unital & the_unity_wrt the multF of F = {} )
proof
let D be non empty set ; ::_thesis: for F being non empty SubStr of D *+^ st {} is Element of F holds
( F is unital & the_unity_wrt the multF of F = {} )
let F be non empty SubStr of D *+^ ; ::_thesis: ( {} is Element of F implies ( F is unital & the_unity_wrt the multF of F = {} ) )
 the_unity_wrt H2(D *+^ ) = {} by Th60;
hence  ( {} is Element of F implies ( F is unital & the_unity_wrt the multF of F = {} ) ) by Th30; ::_thesis: verum
end;

theorem :: MONOID_0:66
for A, B being non empty set st A c= B holds
A *+^ is SubStr of B *+^
proof
let A, B be non empty set ; ::_thesis: ( A c= B implies A *+^ is SubStr of B *+^ )
 H1(A *+^ ) = A * by Def34;
then A1: dom H2(A *+^ ) = [:(A *),(A *):] by FUNCT_2:def_1;
 H1(B *+^ ) = B * by Def34;
then A2: dom H2(B *+^ ) = [:(B *),(B *):] by FUNCT_2:def_1;
assume  A c= B ; ::_thesis: A *+^ is SubStr of B *+^
then A3: A * c= B * by FINSEQ_1:62;
A4: now__::_thesis:_for_x_being_set_st_x_in_[:(A_*),(A_*):]_holds_
H2(A_*+^_)_._x_=_H2(B_*+^_)_._x
let x be set ; ::_thesis: ( x in [:(A *),(A *):] implies H2(A *+^ ) . x = H2(B *+^ ) . x )
assume A5: x in [:(A *),(A *):] ; ::_thesis: H2(A *+^ ) . x = H2(B *+^ ) . x
then A6: ( x `1 in A * & x `2 in A * ) by MCART_1:10;
then reconsider x1 = x `1 , x2 = x `2 as Element of (A *+^) by Def34;
reconsider y1 = x `1 , y2 = x `2 as Element of (B *+^) by A3, A6, Def34;
thus H2(A *+^ ) . x = x1 [*] x2 by A5, MCART_1:21
.= x1 ^ x2 by Def34
.= y1 [*] y2 by Def34
.= H2(B *+^ ) . x by A5, MCART_1:21 ; ::_thesis: verum
end;
 [:(A *),(A *):] c= [:(B *),(B *):] by A3, ZFMISC_1:96;
hence  H2(A *+^ ) c= H2(B *+^ ) by A1, A2, A4, GRFUNC_1:2; :: according to MONOID_0:def_23 ::_thesis: verum
end;

theorem :: MONOID_0:67
for D being non empty set holds
( D -concatenation is having_a_unity & the_unity_wrt (D -concatenation) = {} & D -concatenation is associative )
proof
let D be non empty set ; ::_thesis: ( D -concatenation is having_a_unity & the_unity_wrt (D -concatenation) = {} & D -concatenation is associative )
 multMagma(# (D *),(D -concatenation) #) = D *+^ by Def34;
hence  ( D -concatenation is having_a_unity & the_unity_wrt (D -concatenation) = {} & D -concatenation is associative ) by Th60; ::_thesis: verum
end;

begin

definition
let X be set ;
func GPFuncs X ->  strict constituted-Functions multMagma  means :Def37: :: MONOID_0:def 37
( the carrier of it = PFuncs (X,X) & ( for f, g being Element of it holds f [*] g = g (*) f ) );
existence
 ex b1 being strict constituted-Functions multMagma st
( the carrier of b1 = PFuncs (X,X) & ( for f, g being Element of b1 holds f [*] g = g (*) f ) )
proof
reconsider g = id X as PartFunc of X,X ;
set D = PFuncs (X,X);
defpred S1[ Element of PFuncs (X,X), Element of PFuncs (X,X), Element of PFuncs (X,X)] means  ex f, g being PartFunc of X,X st
( $1 = f & $2 = g & $3 = g (*) f );
A1: for a, b being Element of PFuncs (X,X) ex c being Element of PFuncs (X,X) st S1[a,b,c]
proof
let a, b be Element of PFuncs (X,X); ::_thesis: ex c being Element of PFuncs (X,X) st S1[a,b,c]
reconsider f = a, g = b as PartFunc of X,X by PARTFUN1:46;
reconsider c = g * f as Element of PFuncs (X,X) by PARTFUN1:45;
take  c ; ::_thesis: S1[a,b,c]
take  f ; ::_thesis: ex g being PartFunc of X,X st
( a = f & b = g & c = g (*) f )
take  g ; ::_thesis: ( a = f & b = g & c = g (*) f )
thus  ( a = f & b = g & c = g (*) f ) ; ::_thesis: verum
end;
consider f being BinOp of (PFuncs (X,X)) such that
A2: for a, b being Element of PFuncs (X,X) holds S1[a,b,f . (a,b)] from BINOP_1:sch_3(A1);
set G = multMagma(# (PFuncs (X,X)),f #);
 multMagma(# (PFuncs (X,X)),f #) is constituted-Functions
proof
let x be Element of multMagma(# (PFuncs (X,X)),f #); :: according to MONOID_0:def_1 ::_thesis: x is Function
thus  x is Function ; ::_thesis: verum
end;
then reconsider G = multMagma(# (PFuncs (X,X)),f #) as strict constituted-Functions multMagma ;
take  G ; ::_thesis: ( the carrier of G = PFuncs (X,X) & ( for f, g being Element of G holds f [*] g = g (*) f ) )
thus  H1(G) = PFuncs (X,X) ; ::_thesis: for f, g being Element of G holds f [*] g = g (*) f
let g, h be Element of G; ::_thesis: g [*] h = h (*) g
reconsider g9 = g, h9 = h as Element of PFuncs (X,X) ;
 ex g, h being PartFunc of X,X st
( g9 = g & h9 = h & f . (g9,h9) = h (*) g ) by A2;
hence  g [*] h = h (*) g ; ::_thesis: verum
end;
uniqueness
 for b1, b2 being strict constituted-Functions multMagma st the carrier of b1 = PFuncs (X,X) & ( for f, g being Element of b1 holds f [*] g = g (*) f ) & the carrier of b2 = PFuncs (X,X) & ( for f, g being Element of b2 holds f [*] g = g (*) f ) holds
b1 = b2
proof
let G1, G2 be strict constituted-Functions multMagma ; ::_thesis: ( the carrier of G1 = PFuncs (X,X) & ( for f, g being Element of G1 holds f [*] g = g (*) f ) & the carrier of G2 = PFuncs (X,X) & ( for f, g being Element of G2 holds f [*] g = g (*) f ) implies G1 = G2 )
assume that
A3: H1(G1) = PFuncs (X,X) and
A4: for f, g being Element of G1 holds f [*] g = g (*) f and
A5: H1(G2) = PFuncs (X,X) and
A6: for f, g being Element of G2 holds f [*] g = g (*) f ; ::_thesis: G1 = G2
set f1 = H2(G1);
set f2 = H2(G2);
now__::_thesis:_for_a,_b_being_Element_of_G1_holds_H2(G1)_._(a,b)_=_H2(G2)_._(a,b)
let a, b be Element of G1; ::_thesis: H2(G1) . (a,b) = H2(G2) . (a,b)
reconsider a9 = a, b9 = b as Element of G2 by A3, A5;
 ( a [*] b = b (*) a & a9 [*] b9 = b9 (*) a9 ) by A4, A6;
hence  H2(G1) . (a,b) = H2(G2) . (a,b) ; ::_thesis: verum
end;
hence  G1 = G2 by A3, A5, BINOP_1:2; ::_thesis: verum
end;
end;

:: deftheorem Def37 defines GPFuncs MONOID_0:def_37_:_
 for X being set
for b2 being strict constituted-Functions multMagma holds
( b2 = GPFuncs X iff ( the carrier of b2 = PFuncs (X,X) & ( for f, g being Element of b2 holds f [*] g = g (*) f ) ) );

registration
let X be set ;
cluster GPFuncs X ->  non empty strict unital associative constituted-Functions ;
coherence
 ( GPFuncs X is unital & GPFuncs X is associative & not GPFuncs X is empty )
proof
set G = GPFuncs X;
reconsider g = id X as PartFunc of X,X ;
set D = PFuncs (X,X);
A1: the carrier of (GPFuncs X) = PFuncs (X,X) by Def37;
A2: now__::_thesis:_for_f9,_g,_h_being_Element_of_(GPFuncs_X)_holds_(f9_[*]_g)_[*]_h_=_f9_[*]_(g_[*]_h)
let f9, g, h be Element of (GPFuncs X); ::_thesis: (f9 [*] g) [*] h = f9 [*] (g [*] h)
reconsider fg = f9 [*] g, gh = g [*] h as Element of (GPFuncs X) ;
thus (f9 [*] g) [*] h = h (*) fg by Def37
.= h (*) (g (*) f9) by Def37
.= (h (*) g) (*) f9 by RELAT_1:36
.= gh (*) f9 by Def37
.= f9 [*] (g [*] h) by Def37 ; ::_thesis: verum
end;
reconsider f1 = g as Element of (GPFuncs X) by A1, PARTFUN1:45;
now__::_thesis:_for_h_being_Element_of_(GPFuncs_X)_holds_
(_f1_[*]_h_=_h_&_h_[*]_f1_=_h_)
let h be Element of (GPFuncs X); ::_thesis: ( f1 [*] h = h & h [*] f1 = h )
reconsider j = h as PartFunc of X,X by A1, PARTFUN1:46;
thus f1 [*] h = j (*) g by Def37
.= h by PARTFUN1:6 ; ::_thesis: h [*] f1 = h
thus h [*] f1 = g (*) j by Def37
.= h by PARTFUN1:7 ; ::_thesis: verum
end;
hence  ( GPFuncs X is unital & GPFuncs X is associative & not GPFuncs X is empty ) by A1, A2, Lm2, Th6; ::_thesis: verum
end;
end;

definition
let X be set ;
func MPFuncs X ->  non empty strict well-unital MonoidalExtension of GPFuncs X means :: MONOID_0:def 38
verum;
existence
 ex b1 being non empty strict well-unital MonoidalExtension of GPFuncs X st verum ;
uniqueness
 for b1, b2 being non empty strict well-unital MonoidalExtension of GPFuncs X holds b1 = b2 by Th20;
funcX -composition  ->  BinOp of (PFuncs (X,X)) equals :: MONOID_0:def 39
 the multF of (GPFuncs X);
correctness
coherence
the multF of (GPFuncs X) is BinOp of (PFuncs (X,X));
proof
 H1( GPFuncs X) = PFuncs (X,X) by Def37;
hence  the multF of (GPFuncs X) is BinOp of (PFuncs (X,X)) ; ::_thesis: verum
end;
end;

:: deftheorem  defines MPFuncs MONOID_0:def_38_:_
 for X being set
for b2 being non empty strict well-unital MonoidalExtension of GPFuncs X holds
( b2 = MPFuncs X iff verum );

:: deftheorem  defines -composition MONOID_0:def_39_:_
 for X being set holds X -composition = the multF of (GPFuncs X);

theorem :: MONOID_0:68
for x, X being set holds
( x is Element of (GPFuncs X) iff x is PartFunc of X,X )
proof
let x, X be set ; ::_thesis: ( x is Element of (GPFuncs X) iff x is PartFunc of X,X )
 H1( GPFuncs X) = PFuncs (X,X) by Def37;
hence  ( x is Element of (GPFuncs X) iff x is PartFunc of X,X ) by PARTFUN1:45, PARTFUN1:46; ::_thesis: verum
end;

theorem Th69: :: MONOID_0:69
for X being set holds the_unity_wrt the multF of (GPFuncs X) = id X
proof
let X be set ; ::_thesis: the_unity_wrt the multF of (GPFuncs X) = id X
reconsider g = id X as PartFunc of X,X ;
set op = H2( GPFuncs X);
A1: H1( GPFuncs X) = PFuncs (X,X) by Def37;
then reconsider f = g as Element of (GPFuncs X) by PARTFUN1:45;
now__::_thesis:_for_h_being_Element_of_(GPFuncs_X)_holds_
(_H2(_GPFuncs_X)_._(f,h)_=_h_&_H2(_GPFuncs_X)_._(h,f)_=_h_)
let h be Element of (GPFuncs X); ::_thesis: ( H2( GPFuncs X) . (f,h) = h & H2( GPFuncs X) . (h,f) = h )
reconsider j = h as PartFunc of X,X by A1, PARTFUN1:46;
thus H2( GPFuncs X) . (f,h) = f [*] h
.= j (*) g by Def37
.= h by PARTFUN1:6 ; ::_thesis: H2( GPFuncs X) . (h,f) = h
thus H2( GPFuncs X) . (h,f) = h [*] f
.= g (*) j by Def37
.= h by PARTFUN1:7 ; ::_thesis: verum
end;
then  f is_a_unity_wrt H2( GPFuncs X) by BINOP_1:3;
hence  the_unity_wrt the multF of (GPFuncs X) = id X by BINOP_1:def_8; ::_thesis: verum
end;

theorem Th70: :: MONOID_0:70
for X being set
for F being non empty SubStr of GPFuncs X
for f, g being Element of F holds f [*] g = g (*) f
proof
let X be set ; ::_thesis: for F being non empty SubStr of GPFuncs X
for f, g being Element of F holds f [*] g = g (*) f
let F be non empty SubStr of GPFuncs X; ::_thesis: for f, g being Element of F holds f [*] g = g (*) f
let f, g be Element of F; ::_thesis: f [*] g = g (*) f
 H1(F) c= H1( GPFuncs X) by Th23;
then reconsider f9 = f, g9 = g as Element of (GPFuncs X) by TARSKI:def_3;
 f [*] g = f9 [*] g9 by Th25;
hence  f [*] g = g (*) f by Def37; ::_thesis: verum
end;

theorem Th71: :: MONOID_0:71
for X being set
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 )
proof
let X be set ; ::_thesis: 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 )
let F be non empty SubStr of GPFuncs X; ::_thesis: ( id X is Element of F implies ( F is unital & the_unity_wrt the multF of F = id X ) )
 the_unity_wrt H2( GPFuncs X) = id X by Th69;
hence  ( id X is Element of F implies ( F is unital & the_unity_wrt the multF of F = id X ) ) by Th30; ::_thesis: verum
end;

theorem :: MONOID_0:72
for Y, X being set st Y c= X holds
GPFuncs Y is SubStr of GPFuncs X
proof
let Y, X be set ; ::_thesis: ( Y c= X implies GPFuncs Y is SubStr of GPFuncs X )
 H1( GPFuncs Y) = PFuncs (Y,Y) by Def37;
then A1: dom H2( GPFuncs Y) = [:(PFuncs (Y,Y)),(PFuncs (Y,Y)):] by FUNCT_2:def_1;
 H1( GPFuncs X) = PFuncs (X,X) by Def37;
then A2: dom H2( GPFuncs X) = [:(PFuncs (X,X)),(PFuncs (X,X)):] by FUNCT_2:def_1;
assume  Y c= X ; ::_thesis: GPFuncs Y is SubStr of GPFuncs X
then A3: PFuncs (Y,Y) c= PFuncs (X,X) by PARTFUN1:50;
A4: now__::_thesis:_for_x_being_set_st_x_in_[:(PFuncs_(Y,Y)),(PFuncs_(Y,Y)):]_holds_
H2(_GPFuncs_Y)_._x_=_H2(_GPFuncs_X)_._x
let x be set ; ::_thesis: ( x in [:(PFuncs (Y,Y)),(PFuncs (Y,Y)):] implies H2( GPFuncs Y) . x = H2( GPFuncs X) . x )
assume A5: x in [:(PFuncs (Y,Y)),(PFuncs (Y,Y)):] ; ::_thesis: H2( GPFuncs Y) . x = H2( GPFuncs X) . x
then A6: ( x `1 in PFuncs (Y,Y) & x `2 in PFuncs (Y,Y) ) by MCART_1:10;
then reconsider x1 = x `1 , x2 = x `2 as Element of (GPFuncs Y) by Def37;
reconsider y1 = x `1 , y2 = x `2 as Element of (GPFuncs X) by A3, A6, Def37;
thus H2( GPFuncs Y) . x = x1 [*] x2 by A5, MCART_1:21
.= x2 (*) x1 by Def37
.= y1 [*] y2 by Def37
.= H2( GPFuncs X) . x by A5, MCART_1:21 ; ::_thesis: verum
end;
 [:(PFuncs (Y,Y)),(PFuncs (Y,Y)):] c= [:(PFuncs (X,X)),(PFuncs (X,X)):] by A3, ZFMISC_1:96;
hence  H2( GPFuncs Y) c= H2( GPFuncs X) by A1, A2, A4, GRFUNC_1:2; :: according to MONOID_0:def_23 ::_thesis: verum
end;

definition
let X be set ;
func GFuncs X ->  strict SubStr of GPFuncs X means :Def40: :: MONOID_0:def 40
 the carrier of it = Funcs (X,X);
existence
 ex b1 being strict SubStr of GPFuncs X st the carrier of b1 = Funcs (X,X)
proof
 Funcs (X,X) c= PFuncs (X,X) by FUNCT_2:72;
then reconsider F = Funcs (X,X) as non empty Subset of (GPFuncs X) by Def37;
A1: for x, y being Element of F holds x [*] y in F
proof
let x, y be Element of F; ::_thesis: x [*] y in F
reconsider f = x, g = y as Function of X,X by FUNCT_2:66;
 x [*] y = g * f by Def37;
hence  x [*] y in F by FUNCT_2:9; ::_thesis: verum
end;
consider G being non empty strict SubStr of GPFuncs X such that
A2: the carrier of G = F by Lm6, A1;
take  G ; ::_thesis: the carrier of G = Funcs (X,X)
thus  the carrier of G = Funcs (X,X) by A2; ::_thesis: verum
end;
uniqueness
 for b1, b2 being strict SubStr of GPFuncs X st the carrier of b1 = Funcs (X,X) & the carrier of b2 = Funcs (X,X) holds
b1 = b2 by Th26;
end;

:: deftheorem Def40 defines GFuncs MONOID_0:def_40_:_
 for X being set
for b2 being strict SubStr of GPFuncs X holds
( b2 = GFuncs X iff the carrier of b2 = Funcs (X,X) );

registration
let X be set ;
cluster GFuncs X ->  non empty strict unital ;
coherence
 ( GFuncs X is unital & not GFuncs X is empty )
proof
A1: the carrier of (GFuncs X) = Funcs (X,X) by Def40;
 id X in Funcs (X,X) by FUNCT_2:9;
hence  ( GFuncs X is unital & not GFuncs X is empty ) by A1, Th71; ::_thesis: verum
end;
end;

definition
let X be set ;
func MFuncs X ->  strict well-unital MonoidalExtension of GFuncs X means :: MONOID_0:def 41
verum;
correctness
existence
ex b1 being strict well-unital MonoidalExtension of GFuncs X st verum;
uniqueness
for b1, b2 being strict well-unital MonoidalExtension of GFuncs X holds b1 = b2;
by Th20;
end;

:: deftheorem  defines MFuncs MONOID_0:def_41_:_
 for X being set
for b2 being strict well-unital MonoidalExtension of GFuncs X holds
( b2 = MFuncs X iff verum );

theorem :: MONOID_0:73
for x, X being set holds
( x is Element of (GFuncs X) iff x is Function of X,X )
proof
let x, X be set ; ::_thesis: ( x is Element of (GFuncs X) iff x is Function of X,X )
 H1( GFuncs X) = Funcs (X,X) by Def40;
hence  ( x is Element of (GFuncs X) iff x is Function of X,X ) by FUNCT_2:9, FUNCT_2:66; ::_thesis: verum
end;

theorem Th74: :: MONOID_0:74
for X being set holds the multF of (GFuncs X) = (X -composition) || (Funcs (X,X))
proof
let X be set ; ::_thesis: the multF of (GFuncs X) = (X -composition) || (Funcs (X,X))
A1: H1( GFuncs X) = Funcs (X,X) by Def40;
 ( H2( GFuncs X) c= H2( GPFuncs X) & dom H2( GFuncs X) = [:H1( GFuncs X),H1( GFuncs X):] ) by Def23, FUNCT_2:def_1;
hence  the multF of (GFuncs X) = (X -composition) || (Funcs (X,X)) by A1, GRFUNC_1:23; ::_thesis: verum
end;

theorem Th75: :: MONOID_0:75
for X being set holds the_unity_wrt the multF of (GFuncs X) = id X
proof
let X be set ; ::_thesis: the_unity_wrt the multF of (GFuncs X) = id X
 ( id X in Funcs (X,X) & H1( GFuncs X) = Funcs (X,X) ) by Def40, FUNCT_2:9;
hence  the_unity_wrt the multF of (GFuncs X) = id X by Th71; ::_thesis: verum
end;

theorem :: MONOID_0:76
for X being set holds
( the carrier of (MFuncs X) = Funcs (X,X) & the multF of (MFuncs X) = (X -composition) || (Funcs (X,X)) & 1. (MFuncs X) = id X )
proof
let X be set ; ::_thesis: ( the carrier of (MFuncs X) = Funcs (X,X) & the multF of (MFuncs X) = (X -composition) || (Funcs (X,X)) & 1. (MFuncs X) = id X )
 ( the_unity_wrt H2( GFuncs X) = id X & multMagma(# the carrier of (MFuncs X), the multF of (MFuncs X) #) = GFuncs X ) by Def22, Th75;
hence  ( the carrier of (MFuncs X) = Funcs (X,X) & the multF of (MFuncs X) = (X -composition) || (Funcs (X,X)) & 1. (MFuncs X) = id X ) by Def40, Th17, Th74; ::_thesis: verum
end;

definition
let X be set ;
func GPerms X ->  non empty strict SubStr of GFuncs X means :Def42: :: MONOID_0:def 42
 for f being Element of (GFuncs X) holds
( f in the carrier of it iff f is Permutation of X );
existence
 ex b1 being non empty strict SubStr of GFuncs X st
for f being Element of (GFuncs X) holds
( f in the carrier of b1 iff f is Permutation of X )
proof
defpred S1[ Element of (GFuncs X)] means $1 is Permutation of X;
A1: ex x being Element of (GFuncs X) st S1[x]
proof
set f = the Permutation of X;
 H1( GFuncs X) = Funcs (X,X) by Def40;
then reconsider x = the Permutation of X as Element of (GFuncs X) by FUNCT_2:9;
take  x ; ::_thesis: S1[x]
thus  S1[x] ; ::_thesis: verum
end;
 H1( GFuncs X) = Funcs (X,X) by Def40;
then reconsider f = id X as Element of (GFuncs X) by FUNCT_2:9;
A2: for x, y being Element of (GFuncs X) st S1[x] & S1[y] holds
S1[x [*] y]
proof
let x, y be Element of (GFuncs X); ::_thesis: ( S1[x] & S1[y] implies S1[x [*] y] )
assume  ( x is Permutation of X & y is Permutation of X ) ; ::_thesis: S1[x [*] y]
then reconsider f = x, g = y as Permutation of X ;
 x [*] y = g * f by Th70;
hence  S1[x [*] y] ; ::_thesis: verum
end;
consider G being non empty strict SubStr of GFuncs X such that
A3: for f being Element of (GFuncs X) holds
( f in the carrier of G iff S1[f] ) from MONOID_0:sch_1(A2, A1);
take  G ; ::_thesis: for f being Element of (GFuncs X) holds
( f in the carrier of G iff f is Permutation of X )
thus  for f being Element of (GFuncs X) holds
( f in the carrier of G iff f is Permutation of X ) by A3; ::_thesis: verum
end;
uniqueness
 for b1, b2 being non empty strict SubStr of GFuncs X st ( for f being Element of (GFuncs X) holds
( f in the carrier of b1 iff f is Permutation of X ) ) & ( for f being Element of (GFuncs X) holds
( f in the carrier of b2 iff f is Permutation of X ) ) holds
b1 = b2
proof
let G1, G2 be non empty strict SubStr of GFuncs X; ::_thesis: ( ( for f being Element of (GFuncs X) holds
( f in the carrier of G1 iff f is Permutation of X ) ) & ( for f being Element of (GFuncs X) holds
( f in the carrier of G2 iff f is Permutation of X ) ) implies G1 = G2 )
assume that
A4: for f being Element of (GFuncs X) holds
( f in H1(G1) iff f is Permutation of X ) and
A5: for f being Element of (GFuncs X) holds
( f in H1(G2) iff f is Permutation of X ) ; ::_thesis: G1 = G2
A6: H1(G2) c= H1( GFuncs X) by Th23;
A7: H1(G1) c= H1( GFuncs X) by Th23;
 H1(G1) = H1(G2)
proof
thus  H1(G1) c= H1(G2) :: according to XBOOLE_0:def_10 ::_thesis: H1(G2) c= H1(G1)
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in H1(G1) or x in H1(G2) )
assume A8: x in H1(G1) ; ::_thesis: x in H1(G2)
then reconsider f = x as Element of (GFuncs X) by A7;
 f is Permutation of X by A4, A8;
hence  x in H1(G2) by A5; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in H1(G2) or x in H1(G1) )
assume A9: x in H1(G2) ; ::_thesis: x in H1(G1)
then reconsider f = x as Element of (GFuncs X) by A6;
 f is Permutation of X by A5, A9;
hence  x in H1(G1) by A4; ::_thesis: verum
end;
hence  G1 = G2 by Th26; ::_thesis: verum
end;
end;

:: deftheorem Def42 defines GPerms MONOID_0:def_42_:_
 for X being set
for b2 being non empty strict SubStr of GFuncs X holds
( b2 = GPerms X iff for f being Element of (GFuncs X) holds
( f in the carrier of b2 iff f is Permutation of X ) );

registration
let X be set ;
cluster GPerms X ->  non empty strict unital invertible ;
coherence
 ( GPerms X is unital & GPerms X is invertible )
proof
set G = GPerms X;
A1: H1( GFuncs X) = Funcs (X,X) by Def40;
then reconsider f = id X as Element of (GFuncs X) by FUNCT_2:9;
 f in H1( GPerms X) by Def42;
hence  GPerms X is unital by Th71; ::_thesis: GPerms X is invertible
now__::_thesis:_for_a,_b_being_Element_of_(GPerms_X)_ex_r,_l_being_Element_of_(GPerms_X)_st_
(_a_[*]_r_=_b_&_l_[*]_a_=_b_)
reconsider i = f as Element of (GPerms X) by Def42;
let a, b be Element of (GPerms X); ::_thesis: ex r, l being Element of (GPerms X) st
( a [*] r = b & l [*] a = b )
 H1( GPerms X) c= H1( GFuncs X) by Th23;
then reconsider a9 = a, b9 = b as Element of (GFuncs X) by TARSKI:def_3;
reconsider f = a9, g = b9 as Permutation of X by Def42;
A2: ( i = f (*) (f ") & i = (f ") (*) f ) by FUNCT_2:61;
reconsider f9 = f " as Element of (GFuncs X) by A1, FUNCT_2:9;
A3: ( g (*) i = g & i (*) g = g ) by FUNCT_2:17;
reconsider f9 = f9 as Element of (GPerms X) by Def42;
reconsider r = f9 [*] b, l = b [*] f9 as Element of (GPerms X) ;
take r = r; ::_thesis: ex l being Element of (GPerms X) st
( a [*] r = b & l [*] a = b )
take l = l; ::_thesis: ( a [*] r = b & l [*] a = b )
A4: ( i [*] b = g (*) (id X) & b [*] i = (id X) (*) g ) by Th70;
 ( a [*] f9 = (f ") (*) f & f9 [*] a = f (*) (f ") ) by Th70;
hence  ( a [*] r = b & l [*] a = b ) by A2, A3, A4, Lm2; ::_thesis: verum
end;
hence  GPerms X is invertible by Th10; ::_thesis: verum
end;
end;

theorem Th77: :: MONOID_0:77
for x, X being set holds
( x is Element of (GPerms X) iff x is Permutation of X )
proof
let x, X be set ; ::_thesis: ( x is Element of (GPerms X) iff x is Permutation of X )
A1: ( x is Permutation of X implies x in Funcs (X,X) ) by FUNCT_2:9;
 H1( GPerms X) c= H1( GFuncs X) by Th23;
then A2: ( x is Element of (GPerms X) implies x is Element of (GFuncs X) ) by TARSKI:def_3;
 H1( GFuncs X) = Funcs (X,X) by Def40;
hence  ( x is Element of (GPerms X) iff x is Permutation of X ) by A1, A2, Def42; ::_thesis: verum
end;

theorem Th78: :: MONOID_0:78
for X being set holds
( the_unity_wrt the multF of (GPerms X) = id X & 1_ (GPerms X) = id X )
proof
let X be set ; ::_thesis: ( the_unity_wrt the multF of (GPerms X) = id X & 1_ (GPerms X) = id X )
reconsider i = id X as Element of (GPerms X) by Th77;
now__::_thesis:_for_a_being_Element_of_(GPerms_X)_holds_
(_H2(_GPerms_X)_._(i,a)_=_a_&_H2(_GPerms_X)_._(a,i)_=_a_)
let a be Element of (GPerms X); ::_thesis: ( H2( GPerms X) . (i,a) = a & H2( GPerms X) . (a,i) = a )
reconsider f = a as Permutation of X by Th77;
 a [*] i = i (*) a by Th70;
then A1: H2( GPerms X) . (a,i) = i (*) f ;
 i [*] a = a (*) i by Th70;
hence  ( H2( GPerms X) . (i,a) = a & H2( GPerms X) . (a,i) = a ) by A1, FUNCT_2:17; ::_thesis: verum
end;
then  i is_a_unity_wrt H2( GPerms X) by BINOP_1:3;
hence  the_unity_wrt H2( GPerms X) = id X by BINOP_1:def_8; ::_thesis: 1_ (GPerms X) = id X
hence  1_ (GPerms X) = id X by GROUP_1:22; ::_thesis: verum
end;

theorem :: MONOID_0:79
for X being set
for f being Element of (GPerms X) holds f " = f "
proof
let X be set ; ::_thesis: for f being Element of (GPerms X) holds f " = f "
let f be Element of (GPerms X); ::_thesis: f " = f "
reconsider g = f as Permutation of X by Th77;
A1: ( g (*) (g ") = id X & (g ") (*) g = id X ) by FUNCT_2:61;
reconsider b = g " as Element of (GPerms X) by Th77;
reconsider b = b as Element of (GPerms X) ;
A2: b [*] f = g (*) (g ") by Th70;
 ( id X = 1_ (GPerms X) & f [*] b = (g ") (*) g ) by Th70, Th78;
hence  f " = f " by A1, A2, GROUP_1:def_5; ::_thesis: verum
end;

theorem :: MONOID_0:80
for S being 1-sorted st the carrier of S is functional holds
S is constituted-Functions
proof
let S be 1-sorted ; ::_thesis: ( the carrier of S is functional implies S is constituted-Functions )
assume A1: the carrier of S is functional ; ::_thesis: S is constituted-Functions
let a be Element of S; :: according to MONOID_0:def_1 ::_thesis: a is Function
thus  a is Function by A1; ::_thesis: verum
end;

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

theorem :: MONOID_0:82
for G being non empty multLoopStr
for D being non empty Subset of G st ( for x, y being Element of D holds x * y in D ) & 1. G in D holds
ex H being non empty strict MonoidalSubStr of G st the carrier of H = D
proof
let G be non empty multLoopStr ; ::_thesis: for D being non empty Subset of G st ( for x, y being Element of D holds x * y in D ) & 1. G in D holds
ex H being non empty strict MonoidalSubStr of G st the carrier of H = D
let D be non empty Subset of G; ::_thesis: ( ( for x, y being Element of D holds x * y in D ) & 1. G in D implies ex H being non empty strict MonoidalSubStr of G st the carrier of H = D )
assume that
A1: for x, y being Element of D holds x * y in D and
A2: 1. G in D ; ::_thesis: ex H being non empty strict MonoidalSubStr of G st the carrier of H = D
thus  ex H being non empty strict MonoidalSubStr of G st the carrier of H = D ::_thesis: verum
proof
consider H being non empty strict SubStr of G such that
A3: the carrier of H = D by Lm6, A1;
reconsider e = 1. G as Element of H by A2, A3;
set N = multLoopStr(# the carrier of H, the multF of H,e #);
 ( H2( multLoopStr(# the carrier of H, the multF of H,e #)) c= H2(G) & ( for M being multLoopStr st G = M holds
1. multLoopStr(# the carrier of H, the multF of H,e #) = 1. M ) ) by Def23;
then reconsider N = multLoopStr(# the carrier of H, the multF of H,e #) as non empty strict MonoidalSubStr of G by Def25;
take  N ; ::_thesis: the carrier of N = D
thus  the carrier of N = D by A3; ::_thesis: verum
end;
end;