:: MONOID_0 semantic presentation  Show TPTP formulae Show IDV graph for whole article:: Showing IDV graph ... (Click the Palm Trees again to close it)

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

deffunc H2( HGrStr ) -> Relation of [:the carrier of $1,the carrier of $1:],the carrier of $1 = the mult 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 ;
attr IT is constituted-Functions means :Def1: :: MONOID_0:def 1
for a being Element of IT holds a is Function;
attr IT 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 1-sorted ;
existence
ex b1 being 1-sorted st b1 is constituted-Functions
proof end;
cluster constituted-FinSeqs 1-sorted ;
existence
ex b1 being 1-sorted st b1 is constituted-FinSeqs
proof end;
end;

registration
let X be constituted-Functions 1-sorted ;
cluster -> Relation-like Function-like 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 1-sorted ;
coherence
for b1 being 1-sorted st b1 is constituted-FinSeqs holds
b1 is constituted-Functions
proof end;
end;

registration
cluster constituted-FinSeqs -> constituted-Functions HGrStr ;
coherence
for b1 being HGrStr st b1 is constituted-FinSeqs holds
b1 is constituted-Functions
proof end;
end;

registration
let X be constituted-FinSeqs 1-sorted ;
cluster -> Relation-like Function-like FinSequence-like 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 func p ^ q -> Element of D * ;
coherence
p ^ q is Element of D *
proof end;
end;

Lm1: ( ( for X being set
for f, g being Function of X,X holds f * g is Function of X,X ) & ( for X being set
for f, g being Permutation of X holds f * g is Permutation of X ) & ( for X, Y, Z being set
for f being PartFunc of X,Y
for g being PartFunc of Y,Z holds g * f is PartFunc of X,Z ) & ( for X being set
for A, B being non empty set
for f being Function of X,A
for g being Function of A,B holds g * f is Function of X,B ) )
;

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

definition
let X be set ;
let g, f be Function of X,X;
:: original: (*)
redefine func f * g -> Function of X,X;
coherence
f (*) g is Function of X,X
by Lm1;
end;

definition
let X be set ;
let g, f be Permutation of X;
:: original: (*)
redefine func f * g -> Permutation of X;
coherence
f (*) g is Permutation of X
by Lm1;
end;

definition
let D be non empty set ;
let IT be BinOp of D;
attr IT is left-invertible means :: MONOID_0:def 3
for a, b being Element of D ex l being Element of D st IT . l,a = b;
attr IT is right-invertible means :: MONOID_0:def 4
for a, b being Element of D ex r being Element of D st IT . a,r = b;
attr IT is invertible means :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 );
attr IT is left-cancelable means :: MONOID_0:def 6
for a, b, c being Element of D st IT . a,b = IT . a,c holds
b = c;
attr IT is right-cancelable means :: MONOID_0:def 7
for a, b, c being Element of D st IT . b,a = IT . c,a holds
b = c;
attr IT is cancelable means :: MONOID_0:def 8
for a, b, c being Element of D st ( IT . a,b = IT . a,c or IT . b,a = IT . c,a ) holds
b = c;
attr IT is uniquely-decomposable means :: MONOID_0:def 9
( IT has_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 has_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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 end;

theorem Th2: :: MONOID_0:2  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 end;

theorem Th3: :: MONOID_0:3  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x being set
for f being BinOp of {x} holds
( f = {[x,x]} --> x & f has_a_unity & f is commutative & f is associative & f is idempotent & f is invertible & f is cancelable & f is uniquely-decomposable )
proof end;

definition
let IT be non empty HGrStr ;
redefine attr IT is unital means :Def10: :: MONOID_0:def 10
the mult of IT has_a_unity ;
compatibility
( IT is unital iff the mult of IT has_a_unity )
proof end;
end;

:: deftheorem Def10 defines unital MONOID_0:def 10 :
for IT being non empty HGrStr holds
( IT is unital iff the mult of IT has_a_unity );

definition
let G be non empty HGrStr ;
redefine attr G is commutative means :: MONOID_0:def 11
the mult of G is commutative;
compatibility
( G is commutative iff the mult of G is commutative )
proof end;
redefine attr G is associative means :Def12: :: MONOID_0:def 12
the mult of G is associative;
compatibility
( G is associative iff the mult of G is associative )
proof end;
end;

:: deftheorem defines commutative MONOID_0:def 11 :
for G being non empty HGrStr holds
( G is commutative iff the mult of G is commutative );

:: deftheorem Def12 defines associative MONOID_0:def 12 :
for G being non empty HGrStr holds
( G is associative iff the mult of G is associative );

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

:: deftheorem defines idempotent MONOID_0:def 13 :
for IT being non empty HGrStr holds
( IT is idempotent iff the mult of IT is idempotent );

:: deftheorem defines left-invertible MONOID_0:def 14 :
for IT being non empty HGrStr holds
( IT is left-invertible iff the mult of IT is left-invertible );

:: deftheorem defines right-invertible MONOID_0:def 15 :
for IT being non empty HGrStr holds
( IT is right-invertible iff the mult of IT is right-invertible );

:: deftheorem Def16 defines invertible MONOID_0:def 16 :
for IT being non empty HGrStr holds
( IT is invertible iff the mult of IT is invertible );

:: deftheorem defines left-cancelable MONOID_0:def 17 :
for IT being non empty HGrStr holds
( IT is left-cancelable iff the mult of IT is left-cancelable );

:: deftheorem defines right-cancelable MONOID_0:def 18 :
for IT being non empty HGrStr holds
( IT is right-cancelable iff the mult of IT is right-cancelable );

:: deftheorem defines cancelable MONOID_0:def 19 :
for IT being non empty HGrStr holds
( IT is cancelable iff the mult of IT is cancelable );

:: deftheorem Def20 defines uniquely-decomposable MONOID_0:def 20 :
for IT being non empty HGrStr holds
( IT is uniquely-decomposable iff the mult of IT is uniquely-decomposable );

registration
cluster non empty strict unital associative commutative constituted-Functions constituted-FinSeqs idempotent invertible cancelable uniquely-decomposable HGrStr ;
existence
ex b1 being non empty HGrStr 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 end;
end;

theorem Th4: :: MONOID_0:4  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for G being non empty HGrStr st G is unital holds
the_unity_wrt the mult of G is_a_unity_wrt the mult of G
proof end;

theorem :: MONOID_0:5  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for G being non empty HGrStr holds
( G is unital iff for a being Element of G holds
( (the_unity_wrt the mult of G) * a = a & a * (the_unity_wrt the mult of G) = a ) )
proof end;

theorem Th6: :: MONOID_0:6  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for G being non empty HGrStr 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 end;

Lm2: for G being non empty HGrStr holds
( G is commutative iff for a, b being Element of G holds a * b = b * a )
proof end;

Lm3: for G being non empty HGrStr holds
( G is associative iff for a, b, c being Element of G holds (a * b) * c = a * (b * c) )
proof end;

theorem :: MONOID_0:7  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: MONOID_0:8  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem Th9: :: MONOID_0:9  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for G being non empty HGrStr holds
( G is idempotent iff for a being Element of G holds a * a = a )
proof end;

theorem :: MONOID_0:10  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for G being non empty HGrStr holds
( G is left-invertible iff for a, b being Element of G ex l being Element of G st l * a = b )
proof end;

theorem :: MONOID_0:11  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for G being non empty HGrStr holds
( G is right-invertible iff for a, b being Element of G ex r being Element of G st a * r = b )
proof end;

theorem Th12: :: MONOID_0:12  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for G being non empty HGrStr 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 end;

theorem :: MONOID_0:13  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for G being non empty HGrStr holds
( G is left-cancelable iff for a, b, c being Element of G st a * b = a * c holds
b = c )
proof end;

theorem :: MONOID_0:14  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for G being non empty HGrStr holds
( G is right-cancelable iff for a, b, c being Element of G st b * a = c * a holds
b = c )
proof end;

theorem Th15: :: MONOID_0:15  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for G being non empty HGrStr 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 end;

theorem Th16: :: MONOID_0:16  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for G being non empty HGrStr holds
( G is uniquely-decomposable iff ( the mult of G has_a_unity & ( for a, b being Element of G st a * b = the_unity_wrt the mult of G holds
( a = b & b = the_unity_wrt the mult of G ) ) ) )
proof end;

theorem Th17: :: MONOID_0:17  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for G being non empty HGrStr st G is associative holds
( G is invertible iff ( G is unital & the mult of G has_an_inverseOp ) )
proof end;

Lm4: for G being non empty HGrStr holds
( G is invertible iff ( G is left-invertible & G is right-invertible ) )
proof end;

Lm5: for G being non empty HGrStr holds
( G is cancelable iff ( G is left-cancelable & G is right-cancelable ) )
proof end;

Lm6: for G being non empty HGrStr st G is associative & G is invertible holds
G is Group-like
proof end;

registration
cluster non empty Group-like associative -> non empty invertible HGrStr ;
coherence
for b1 being non empty HGrStr st b1 is associative & b1 is Group-like holds
b1 is invertible
proof end;
cluster non empty associative invertible -> non empty Group-like HGrStr ;
coherence
for b1 being non empty HGrStr st b1 is associative & b1 is invertible holds
b1 is Group-like
by Lm6;
end;

registration
cluster non empty invertible -> non empty left-invertible right-invertible HGrStr ;
coherence
for b1 being non empty HGrStr st b1 is invertible holds
( b1 is left-invertible & b1 is right-invertible )
by Lm4;
cluster non empty left-invertible right-invertible -> non empty invertible HGrStr ;
coherence
for b1 being non empty HGrStr st b1 is left-invertible & b1 is right-invertible holds
b1 is invertible
by Lm4;
cluster non empty cancelable -> non empty left-cancelable right-cancelable HGrStr ;
coherence
for b1 being non empty HGrStr st b1 is cancelable holds
( b1 is left-cancelable & b1 is right-cancelable )
by Lm5;
cluster non empty left-cancelable right-cancelable -> non empty cancelable HGrStr ;
coherence
for b1 being non empty HGrStr st b1 is left-cancelable & b1 is right-cancelable holds
b1 is cancelable
by Lm5;
cluster non empty associative invertible -> non empty unital cancelable HGrStr ;
coherence
for b1 being non empty HGrStr st b1 is associative & b1 is invertible holds
( b1 is unital & b1 is cancelable )
proof end;
end;

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

definition
let IT be non empty multLoopStr ;
redefine attr IT is well-unital means :Def21: :: MONOID_0:def 21
the unity of IT is_a_unity_wrt the mult of IT;
compatibility
( IT is well-unital iff the unity of IT is_a_unity_wrt the mult of IT )
proof end;
end;

:: deftheorem Def21 defines well-unital MONOID_0:def 21 :
for IT being non empty multLoopStr holds
( IT is well-unital iff the unity of IT is_a_unity_wrt the mult of IT );

theorem Th18: :: MONOID_0:18  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for M being non empty multLoopStr holds
( M is well-unital iff for a being Element of M holds
( the unity of M * a = a & a * the unity of M = a ) )
proof end;

Lm7: for M being non empty multLoopStr st M is well-unital holds
M is unital
proof end;

registration
cluster non empty well-unital -> non empty unital multLoopStr ;
coherence
for b1 being non empty multLoopStr st b1 is well-unital holds
b1 is unital
by Lm7;
end;

theorem Th19: :: MONOID_0:19  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for M being non empty multLoopStr st M is well-unital holds
the unity of M = the_unity_wrt the mult of M
proof end;

registration
let A be non empty set ;
let m be BinOp of A;
let u be Element of A;
cluster multLoopStr(# A,m,u #) -> non empty ;
coherence
not multLoopStr(# A,m,u #) is empty
by STRUCT_0:def 1;
end;

registration
cluster non empty unital Group-like associative commutative strict well-unital constituted-Functions constituted-FinSeqs idempotent left-invertible right-invertible invertible left-cancelable right-cancelable cancelable uniquely-decomposable 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 end;
end;

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

definition
let G be HGrStr ;
mode MonoidalExtension of G -> multLoopStr means :Def22: :: MONOID_0:def 22
HGrStr(# the carrier of it,the mult of it #) = HGrStr(# the carrier of G,the mult of G #);
existence
ex b1 being multLoopStr st HGrStr(# the carrier of b1,the mult of b1 #) = HGrStr(# the carrier of G,the mult of G #)
proof end;
end;

:: deftheorem Def22 defines MonoidalExtension MONOID_0:def 22 :
for G being HGrStr
for b2 being multLoopStr holds
( b2 is MonoidalExtension of G iff HGrStr(# the carrier of b2,the mult of b2 #) = HGrStr(# the carrier of G,the mult of G #) );

registration
let G be non empty HGrStr ;
cluster -> non empty MonoidalExtension of G;
coherence
for b1 being MonoidalExtension of G holds not b1 is empty
proof end;
end;

theorem Th20: :: MONOID_0:20  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for G being non empty HGrStr
for M being MonoidalExtension of G holds
( the carrier of M = the carrier of G & the mult of M = the mult of G & ( for a, b being Element of M
for a', b' being Element of G st a = a' & b = b' holds
a * b = a' * b' ) )
proof end;

registration
let G be HGrStr ;
cluster strict MonoidalExtension of G;
existence
ex b1 being MonoidalExtension of G st b1 is strict
proof end;
end;

theorem Th21: :: MONOID_0:21  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for G being non empty HGrStr
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 end;

registration
let G be constituted-Functions HGrStr ;
cluster -> constituted-Functions MonoidalExtension of G;
coherence
for b1 being MonoidalExtension of G holds b1 is constituted-Functions
proof end;
end;

registration
let G be constituted-FinSeqs HGrStr ;
cluster -> constituted-Functions constituted-FinSeqs MonoidalExtension of G;
coherence
for b1 being MonoidalExtension of G holds b1 is constituted-FinSeqs
proof end;
end;

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

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

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

registration
let G be non empty invertible HGrStr ;
cluster -> non empty left-invertible right-invertible invertible MonoidalExtension of G;
coherence
for b1 being MonoidalExtension of G holds b1 is invertible
by Th21;
end;

registration
let G be non empty cancelable HGrStr ;
cluster -> non empty left-cancelable right-cancelable cancelable MonoidalExtension of G;
coherence
for b1 being MonoidalExtension of G holds b1 is cancelable
by Th21;
end;

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

registration
let G be non empty unital HGrStr ;
cluster non empty unital strict well-unital MonoidalExtension of G;
existence
ex b1 being MonoidalExtension of G st
( b1 is well-unital & b1 is strict )
proof end;
end;

theorem Th22: :: MONOID_0:22  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for G being non empty unital HGrStr
for M1, M2 being strict well-unital MonoidalExtension of G holds M1 = M2
proof end;

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

:: deftheorem Def23 defines SubStr MONOID_0:def 23 :
for G, b2 being HGrStr holds
( b2 is SubStr of G iff the mult of b2 <= the mult of G );

registration
let G be HGrStr ;
cluster strict SubStr of G;
existence
ex b1 being SubStr of G st b1 is strict
proof end;
end;

registration
let G be non empty HGrStr ;
cluster non empty strict SubStr of G;
existence
ex b1 being SubStr of G st
( b1 is strict & not b1 is empty )
proof end;
end;

registration
let G be non empty unital HGrStr ;
cluster non empty strict unital Group-like associative commutative idempotent left-invertible right-invertible invertible left-cancelable right-cancelable cancelable uniquely-decomposable 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 end;
end;

definition
let G be HGrStr ;
mode MonoidalSubStr of G -> multLoopStr means :Def24: :: MONOID_0:def 24
( the mult of it <= the mult of G & ( for M being multLoopStr st G = M holds
the unity of it = the unity of M ) );
existence
ex b1 being multLoopStr st
( the mult of b1 <= the mult of G & ( for M being multLoopStr st G = M holds
the unity of b1 = the unity of M ) )
proof end;
end;

:: deftheorem Def24 defines MonoidalSubStr MONOID_0:def 24 :
for G being HGrStr
for b2 being multLoopStr holds
( b2 is MonoidalSubStr of G iff ( the mult of b2 <= the mult of G & ( for M being multLoopStr st G = M holds
the unity of b2 = the unity of M ) ) );

registration
let G be HGrStr ;
cluster strict MonoidalSubStr of G;
existence
ex b1 being MonoidalSubStr of G st b1 is strict
proof end;
end;

registration
let G be non empty HGrStr ;
cluster non empty strict MonoidalSubStr of G;
existence
ex b1 being MonoidalSubStr of G st
( b1 is strict & not b1 is empty )
proof end;
end;

definition
let M be multLoopStr ;
redefine mode MonoidalSubStr of M means :Def25: :: MONOID_0:def 25
( the mult of it <= the mult of M & the unity of it = the unity of M );
compatibility
for b1 being multLoopStr holds
( b1 is MonoidalSubStr of M iff ( the mult of b1 <= the mult of M & the unity of b1 = the unity of M ) )
proof end;
end;

:: deftheorem Def25 defines MonoidalSubStr MONOID_0:def 25 :
for M, b2 being multLoopStr holds
( b2 is MonoidalSubStr of M iff ( the mult of b2 <= the mult of M & the unity of b2 = the unity of M ) );

registration
let G be non empty well-unital multLoopStr ;
cluster non empty unital Group-like associative commutative strict well-unital idempotent left-invertible right-invertible invertible left-cancelable right-cancelable cancelable uniquely-decomposable 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 end;
end;

theorem Th23: :: MONOID_0:23  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for G being HGrStr
for M being MonoidalSubStr of G holds M is SubStr of G
proof end;

definition
let G be HGrStr ;
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 end;
end;

definition
let G1 be HGrStr ;
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 end;
end;

definition
let G1 be HGrStr ;
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 end;
end;

definition
let G be HGrStr ;
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 end;
end;

theorem :: MONOID_0:24  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for G being non empty HGrStr
for M being non empty multLoopStr holds
( G is SubStr of G & M is MonoidalSubStr of M )
proof end;

theorem Th25: :: MONOID_0:25  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for G being non empty HGrStr
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 end;

theorem Th26: :: MONOID_0:26  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for G being non empty HGrStr
for H being non empty SubStr of G holds the mult of H = the mult of G || the carrier of H
proof end;

theorem Th27: :: MONOID_0:27  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for G being non empty HGrStr
for H being non empty SubStr of G
for a, b being Element of H
for a', b' being Element of G st a = a' & b = b' holds
a * b = a' * b'
proof end;

theorem Th28: :: MONOID_0:28  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for G being non empty HGrStr
for H1, H2 being non empty SubStr of G st the carrier of H1 = the carrier of H2 holds
HGrStr(# the carrier of H1,the mult of H1 #) = HGrStr(# the carrier of H2,the mult of H2 #)
proof end;

theorem :: MONOID_0:29  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 mult of H1,the unity of H1 #) = multLoopStr(# the carrier of H2,the mult of H2,the unity of H2 #)
proof end;

theorem Th30: :: MONOID_0:30  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for G being non empty HGrStr
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 end;

theorem :: MONOID_0:31  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 end;

theorem Th32: :: MONOID_0:32  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for G being non empty HGrStr
for H being non empty SubStr of G st G is unital & the_unity_wrt the mult of G in the carrier of H holds
( H is unital & the_unity_wrt the mult of G = the_unity_wrt the mult of H )
proof end;

theorem Th33: :: MONOID_0:33  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for M being non empty well-unital multLoopStr
for N being non empty MonoidalSubStr of M holds N is well-unital
proof end;

theorem Th34: :: MONOID_0:34  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for G being non empty HGrStr
for H being non empty SubStr of G st G is commutative holds
H is commutative
proof end;

theorem Th35: :: MONOID_0:35  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for G being non empty HGrStr
for H being non empty SubStr of G st G is associative holds
H is associative
proof end;

theorem Th36: :: MONOID_0:36  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for G being non empty HGrStr
for H being non empty SubStr of G st G is idempotent holds
H is idempotent
proof end;

theorem Th37: :: MONOID_0:37  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for G being non empty HGrStr
for H being non empty SubStr of G st G is cancelable holds
H is cancelable
proof end;

theorem Th38: :: MONOID_0:38  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for G being non empty HGrStr
for H being non empty SubStr of G st the_unity_wrt the mult of G in the carrier of H & G is uniquely-decomposable holds
H is uniquely-decomposable
proof end;

theorem Th39: :: MONOID_0:39  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for M being non empty well-unital uniquely-decomposable multLoopStr
for N being non empty MonoidalSubStr of M holds N is uniquely-decomposable
proof end;

registration
let G be non empty constituted-Functions HGrStr ;
cluster non empty -> non empty constituted-Functions SubStr of G;
coherence
for b1 being non empty SubStr of G holds b1 is constituted-Functions
proof end;
cluster non empty -> non empty constituted-Functions MonoidalSubStr of G;
coherence
for b1 being non empty MonoidalSubStr of G holds b1 is constituted-Functions
proof end;
end;

registration
let G be non empty constituted-FinSeqs HGrStr ;
cluster non empty -> non empty constituted-Functions constituted-FinSeqs SubStr of G;
coherence
for b1 being non empty SubStr of G holds b1 is constituted-FinSeqs
proof end;
cluster non empty -> non empty constituted-Functions constituted-FinSeqs MonoidalSubStr of G;
coherence
for b1 being non empty MonoidalSubStr of G holds b1 is constituted-FinSeqs
proof end;
end;

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

registration
let G be non empty commutative HGrStr ;
cluster non empty -> non empty commutative SubStr of G;
coherence
for b1 being non empty SubStr of G holds b1 is commutative
by Th34;
cluster non empty -> non empty commutative MonoidalSubStr of G;
coherence
for b1 being non empty MonoidalSubStr of G holds b1 is commutative
proof end;
end;

registration
let G be non empty associative HGrStr ;
cluster non empty -> non empty associative SubStr of G;
coherence
for b1 being non empty SubStr of G holds b1 is associative
by Th35;
cluster non empty -> non empty associative MonoidalSubStr of G;
coherence
for b1 being non empty MonoidalSubStr of G holds b1 is associative
proof end;
end;

registration
let G be non empty idempotent HGrStr ;
cluster non empty -> non empty idempotent SubStr of G;
coherence
for b1 being non empty SubStr of G holds b1 is idempotent
by Th36;
cluster non empty -> non empty idempotent MonoidalSubStr of G;
coherence
for b1 being non empty MonoidalSubStr of G holds b1 is idempotent
proof end;
end;

registration
let G be non empty cancelable HGrStr ;
cluster non empty -> non empty left-cancelable right-cancelable cancelable SubStr of G;
coherence
for b1 being non empty SubStr of G holds b1 is cancelable
by Th37;
cluster non empty -> non empty left-cancelable right-cancelable cancelable MonoidalSubStr of G;
coherence
for b1 being non empty MonoidalSubStr of G holds b1 is cancelable
proof end;
end;

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

scheme :: MONOID_0:sch 1
SubStrEx1{ F1() -> non empty HGrStr , F2() -> non empty Subset of F1() } :
ex H being non empty strict SubStr of F1() st the carrier of H = F2()
provided
A1: for x, y being Element of F2() holds x * y in F2()
proof end;

scheme :: MONOID_0:sch 2
SubStrEx2{ F1() -> non empty HGrStr , 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 end;

scheme :: MONOID_0:sch 3
MonoidalSubStrEx1{ F1() -> non empty multLoopStr , F2() -> non empty Subset of F1() } :
ex H being non empty strict MonoidalSubStr of F1() st the carrier of H = F2()
provided
A1: for x, y being Element of F2() holds x * y in F2() and
A2: the unity of F1() in F2()
proof end;

scheme :: MONOID_0:sch 4
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[the unity of F1()]
proof end;

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

definition
let G be non empty HGrStr ;
let a, b be Element of G;
:: original: [*]
redefine func a [*] b -> Element of G;
coherence
a [*] b is Element of G
;
end;

definition
func <REAL,+> -> non empty strict unital associative commutative invertible cancelable HGrStr equals :: MONOID_0:def 26
HGrStr(# REAL ,addreal #);
coherence
HGrStr(# REAL ,addreal #) is non empty strict unital associative commutative invertible cancelable HGrStr
proof end;
end;

:: deftheorem defines <REAL,+> MONOID_0:def 26 :
<REAL,+> = HGrStr(# REAL ,addreal #);

theorem Th40: :: MONOID_0:40  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
( the carrier of <REAL,+> = REAL & the mult of <REAL,+> = addreal & ( for a, b being Element of <REAL,+>
for x, y being Real st a = x & b = y holds
a * b = x + y ) ) by BINOP_2:def 9;

theorem :: MONOID_0:41  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x being set holds
( x is Element of <REAL,+> iff x is Real ) ;

theorem :: MONOID_0:42  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
the_unity_wrt the mult of <REAL,+> = 0 by BINOP_2:2;

theorem Th43: :: MONOID_0:43  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 end;

theorem Th44: :: MONOID_0:44  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for N being non empty unital SubStr of <REAL,+> holds the_unity_wrt the mult of N = 0
proof end;

registration
let G be non empty unital HGrStr ;
cluster non empty associative invertible -> non empty unital Group-like left-cancelable right-cancelable cancelable 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 )
proof end;
end;

definition
:: original: INT.Group
redefine func INT.Group -> non empty strict unital invertible SubStr of <REAL,+> ;
coherence
INT.Group is non empty strict unital invertible SubStr of <REAL,+>
proof end;
end;

theorem :: MONOID_0:45  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: MONOID_0:46  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for G being non empty strict SubStr of <REAL,+> holds
( G = INT.Group iff the carrier of G = INT ) by Th28, GR_CY_1:def 4;

theorem :: MONOID_0:47  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x being set holds
( x is Element of INT.Group iff x is Integer ) by GR_CY_1:def 4, 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 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 Th28;
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 Th22;
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 :Def29: :: MONOID_0:def 29
the mult of <NAT,+> ;
compatibility
for b1 being Relation of [:NAT ,NAT :], NAT holds
( b1 = addnat iff b1 = the mult of <NAT,+> )
proof end;
end;

:: deftheorem Def29 defines addnat MONOID_0:def 29 :
addnat = the mult of <NAT,+> ;

theorem :: MONOID_0:48  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem Th49: :: MONOID_0:49  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
<NAT,+> = HGrStr(# NAT ,addnat #) by Def27, Def29;

theorem :: MONOID_0:50  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x being set holds
( x is Element of <NAT,+,0> iff x is Nat )
proof end;

theorem :: MONOID_0:51  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n1, n2 being Nat
for m1, m2 being Element of <NAT,+,0> st n1 = m1 & n2 = m2 holds
m1 * m2 = n1 + n2
proof end;

theorem :: MONOID_0:52  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
<NAT,+,0> = multLoopStr(# NAT ,addnat ,0 #)
proof end;

theorem :: MONOID_0:53  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
( addnat = addreal || NAT & addnat = addint || NAT )
proof end;

theorem :: MONOID_0:54  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
( 0 is_a_unity_wrt addnat & addnat is uniquely-decomposable )
proof end;

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

:: deftheorem defines <REAL,*> MONOID_0:def 30 :
<REAL,*> = HGrStr(# REAL ,multreal #);

theorem Th55: :: MONOID_0:55  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
( the carrier of <REAL,*> = REAL & the mult of <REAL,*> = multreal & ( for a, b being Element of <REAL,*>
for x, y being Real st a = x & b = y holds
a * b = x * y ) ) by BINOP_2:def 11;

theorem :: MONOID_0:56  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x being set holds
( x is Element of <REAL,*> iff x is Real ) ;

theorem :: MONOID_0:57  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
the_unity_wrt the mult of <REAL,*> = 1 by BINOP_2:7;

theorem Th58: :: MONOID_0:58  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 end;

theorem :: MONOID_0:59  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: MONOID_0:60  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for N being non empty unital SubStr of <REAL,*> holds
( the_unity_wrt the mult of N = 0 or the_unity_wrt the mult of N = 1 )
proof 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 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 Th28;
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 Th22;
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 :Def33: :: MONOID_0:def 33
the mult of <NAT,*> ;
compatibility
for b1 being Relation of [:NAT ,NAT :], NAT holds
( b1 = multnat iff b1 = the mult of <NAT,*> )
proof end;
end;

:: deftheorem Def33 defines multnat MONOID_0:def 33 :
multnat = the mult of <NAT,*> ;

theorem Th61: :: MONOID_0:61  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
<NAT,*> = HGrStr(# NAT ,multnat #) by Def31, Def33;

theorem :: MONOID_0:62  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n1, n2 being Nat
for m1, m2 being Element of <NAT,*> st n1 = m1 & n2 = m2 holds
m1 * m2 = n1 * n2 by Th58;

theorem Th63: :: MONOID_0:63  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
the_unity_wrt the mult of <NAT,*> = 1
proof end;

theorem :: MONOID_0:64  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n1, n2 being Nat
for m1, m2 being Element of <NAT,*,1> st n1 = m1 & n2 = m2 holds
m1 * m2 = n1 * n2
proof end;

theorem :: MONOID_0:65  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
<NAT,*,1> = multLoopStr(# NAT ,multnat ,1 #)
proof end;

theorem :: MONOID_0:66  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
multnat = multreal || NAT by Th26, Th61;

theorem :: MONOID_0:67  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
( 1 is_a_unity_wrt multnat & multnat is uniquely-decomposable )
proof end;

definition
let D be non empty set ;
func D *+^ -> non empty strict unital associative constituted-FinSeqs cancelable uniquely-decomposable HGrStr 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 HGrStr st
( the carrier of b1 = D * & ( for p, q being Element of b1 holds p [*] q = p ^ q ) )
proof end;
uniqueness
for b1, b2 being non empty strict unital associative constituted-FinSeqs cancelable uniquely-decomposable HGrStr 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 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 HGrStr 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 ;
func D *+^+<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 Th22;
func D -concatenation -> BinOp of D * equals :: MONOID_0:def 36
the mult of (D *+^ );
correctness
coherence
the mult of (D *+^ ) is BinOp of D *
;
proof 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 mult of (D *+^ );

theorem Th68: :: MONOID_0:68  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for D being non empty set holds D *+^ = HGrStr(# (D * ),(D -concatenation ) #) by Def34;

theorem Th69: :: MONOID_0:69  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for D being non empty set holds the_unity_wrt the mult of (D *+^ ) = {}
proof end;

theorem :: MONOID_0:70  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for D being non empty set holds
( the carrier of (D *+^+<0> ) = D * & the mult of (D *+^+<0> ) = D -concatenation & the unity of (D *+^+<0> ) = {} )
proof end;

theorem :: MONOID_0:71  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for D being non empty set
for a, b being Element of (D *+^+<0> ) holds a [*] b = a ^ b
proof end;

theorem Th72: :: MONOID_0:72  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 end;

theorem :: MONOID_0:73  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for D being non empty set
for F being non empty unital SubStr of D *+^ holds the_unity_wrt the mult of F = {}
proof end;

theorem :: MONOID_0:74  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 mult of F = {} )
proof end;

theorem :: MONOID_0:75  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for A, B being non empty set st A c= B holds
A *+^ is SubStr of B *+^
proof end;

theorem :: MONOID_0:76  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for D being non empty set holds
( D -concatenation has_a_unity & the_unity_wrt (D -concatenation ) = {} & D -concatenation is associative )
proof end;

definition
let X be set ;
func GPFuncs X -> non empty strict unital associative constituted-Functions HGrStr means :Def37: :: MONOID_0:def 37
( the carrier of it = PFuncs X,X & ( for f, g being Element of it holds f [*] g = f (*) g ) );
existence
ex b1 being non empty strict unital associative constituted-Functions HGrStr st
( the carrier of b1 = PFuncs X,X & ( for f, g being Element of b1 holds f [*] g = f (*) g ) )
proof end;
uniqueness
for b1, b2 being non empty strict unital associative constituted-Functions HGrStr st the carrier of b1 = PFuncs X,X & ( for f, g being Element of b1 holds f [*] g = f (*) g ) & the carrier of b2 = PFuncs X,X & ( for f, g being Element of b2 holds f [*] g = f (*) g ) holds
b1 = b2
proof end;
end;

:: deftheorem Def37 defines GPFuncs MONOID_0:def 37 :
for X being set
for b2 being non empty strict unital associative constituted-Functions HGrStr holds
( b2 = GPFuncs X iff ( the carrier of b2 = PFuncs X,X & ( for f, g being Element of b2 holds f [*] g = f (*) g ) ) );

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 Th22;
func X -composition -> BinOp of PFuncs X,X equals :: MONOID_0:def 39
the mult of (GPFuncs X);
correctness
coherence
the mult of (GPFuncs X) is BinOp of PFuncs X,X
;
proof 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 mult of (GPFuncs X);

theorem :: MONOID_0:77  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x, X being set holds
( x is Element of (GPFuncs X) iff x is PartFunc of X,X )
proof end;

theorem Th78: :: MONOID_0:78  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being set holds the_unity_wrt the mult of (GPFuncs X) = id X
proof end;

theorem Th79: :: MONOID_0:79  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being set
for F being non empty SubStr of GPFuncs X
for f, g being Element of F holds f [*] g = f (*) g
proof end;

theorem Th80: :: MONOID_0:80  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 mult of F = id X )
proof end;

theorem :: MONOID_0:81  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for Y, X being set st Y c= X holds
GPFuncs Y is SubStr of GPFuncs X
proof end;

Lm8: for x, X being set st x in Funcs X,X holds
x is Function of X,X
proof end;

definition
let X be set ;
func GFuncs X -> non empty strict unital SubStr of GPFuncs X means :Def40: :: MONOID_0:def 40
the carrier of it = Funcs X,X;
existence
ex b1 being non empty strict unital SubStr of GPFuncs X st the carrier of b1 = Funcs X,X
proof end;
uniqueness
for b1, b2 being non empty strict unital SubStr of GPFuncs X st the carrier of b1 = Funcs X,X & the carrier of b2 = Funcs X,X holds
b1 = b2
by Th28;
end;

:: deftheorem Def40 defines GFuncs MONOID_0:def 40 :
for X being set
for b2 being non empty strict unital SubStr of GPFuncs X holds
( b2 = GFuncs X iff the carrier of b2 = Funcs X,X );

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 Th22;
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:82  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x, X being set holds
( x is Element of (GFuncs X) iff x is Function of X,X )
proof end;

theorem Th83: :: MONOID_0:83  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being set holds the mult of (GFuncs X) = (X -composition ) || (Funcs X,X)
proof end;

theorem Th84: :: MONOID_0:84  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being set holds the_unity_wrt the mult of (GFuncs X) = id X
proof end;

theorem :: MONOID_0:85  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being set holds
( the carrier of (MFuncs X) = Funcs X,X & the mult of (MFuncs X) = (X -composition ) || (Funcs X,X) & the unity of (MFuncs X) = id X )
proof end;

definition
let X be set ;
func GPerms X -> non empty strict unital invertible 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 unital invertible 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 end;
uniqueness
for b1, b2 being non empty strict unital invertible 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 end;
end;

:: deftheorem Def42 defines GPerms MONOID_0:def 42 :
for X being set
for b2 being non empty strict unital invertible 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 ) );

theorem Th86: :: MONOID_0:86  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x, X being set holds
( x is Element of (GPerms X) iff x is Permutation of X )
proof end;

theorem Th87: :: MONOID_0:87  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being set holds
( the_unity_wrt the mult of (GPerms X) = id X & 1. (GPerms X) = id X )
proof end;

theorem :: MONOID_0:88  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being set
for f being Element of (GPerms X) holds f " = f "
proof end;

theorem :: MONOID_0:89  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for S being 1-sorted st the carrier of S is functional holds
S is constituted-Functions
proof end;