MONOID_0: Monoids

proof end;

cluster constituted-FinSeqs for 1-sorted ;

proof end;

end;

registration

let X be constituted-Functions 1-sorted ;

cluster -> Relation-like Function-like for Element of the carrier of X;

coherence by Def1;

end;

registration

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

coherence ;

end;

registration

let X be constituted-FinSeqs 1-sorted ;

cluster -> FinSequence-like for Element of the carrier of X;

coherence by Def2;

end;

definition

let D be set ;
let p, q be FinSequence of D;
:: original: ^
redefine func p ^ q -> Element of D * ;
coherence

proof 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;

attr IT is left-invertible means :: MONOID_0:def 3
for a, b being Element of D ex l being Element of D st IT . (l,a) = b;

attr IT is right-invertible means :: MONOID_0:def 4
for a, b being Element of D ex r being Element of D st IT . (a,r) = b;

attr IT is invertible means :: MONOID_0:def 5
for a, b being Element of D ex r, l being Element of D st
( IT . (a,r) = b & IT . (l,a) = b );

attr IT is left-cancelable means :: MONOID_0:def 6
for a, b, c being Element of D st IT . (a,b) = IT . (a,c) holds
b = c;

attr IT is right-cancelable means :: MONOID_0:def 7
for a, b, c being Element of D st IT . (b,a) = IT . (c,a) holds
b = c;

attr IT is cancelable means :: MONOID_0:def 8
for a, b, c being Element of D st ( IT . (a,b) = IT . (a,c) or IT . (b,a) = IT . (c,a) ) holds
b = c;

attr IT is uniquely-decomposable means :: MONOID_0:def 9
( IT is having_a_unity & ( for a, b being Element of D st IT . (a,b) = the_unity_wrt IT holds
( a = b & b = the_unity_wrt IT ) ) );

end;

:: deftheorem defines left-invertible MONOID_0:def 3 :

:: deftheorem defines right-invertible MONOID_0:def 4 :

:: deftheorem defines invertible MONOID_0:def 5 :

:: deftheorem defines left-cancelable MONOID_0:def 6 :

:: deftheorem defines right-cancelable MONOID_0:def 7 :

:: deftheorem defines cancelable MONOID_0:def 8 :

:: deftheorem defines uniquely-decomposable MONOID_0:def 9 :

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 end;

theorem :: 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 ) ) ;

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 end;

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 ;

proof end;

end;

:: deftheorem Def10 defines unital MONOID_0:def 10 :

definition

let G be non empty multMagma ;

redefine attr G is commutative means :Def11: :: MONOID_0:def 11
the multF of G is commutative ;

proof end;

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

compatibility ;

end;

:: deftheorem Def11 defines commutative MONOID_0:def 11 :

:: deftheorem Def12 defines associative MONOID_0:def 12 :

definition

let IT be non empty multMagma ;

attr IT is idempotent means :: MONOID_0:def 13
the multF of IT is idempotent ;

attr IT is left-invertible means :: MONOID_0:def 14
the multF of IT is left-invertible ;

attr IT is right-invertible means :: MONOID_0:def 15
the multF of IT is right-invertible ;

attr IT is invertible means :: MONOID_0:def 16
the multF of IT is invertible ;

attr IT is left-cancelable means :: MONOID_0:def 17
the multF of IT is left-cancelable ;

attr IT is right-cancelable means :: MONOID_0:def 18
the multF of IT is right-cancelable ;

attr IT is cancelable means :: MONOID_0:def 19
the multF of IT is cancelable ;

attr IT is uniquely-decomposable means :Def20: :: MONOID_0:def 20
the multF of IT is uniquely-decomposable ;

end;

:: deftheorem defines idempotent MONOID_0:def 13 :

:: deftheorem defines left-invertible MONOID_0:def 14 :

:: deftheorem defines right-invertible MONOID_0:def 15 :

:: deftheorem defines invertible MONOID_0:def 16 :

:: deftheorem defines left-cancelable MONOID_0:def 17 :

:: deftheorem defines right-cancelable MONOID_0:def 18 :

:: deftheorem defines cancelable MONOID_0:def 19 :

:: deftheorem Def20 defines uniquely-decomposable MONOID_0:def 20 :

registration

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

proof 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 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 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 ) ) ;

Lm1: 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) )
;

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 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 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 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 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 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 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 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 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 end;

Lm2: for G being non empty multMagma holds
( G is invertible iff ( G is left-invertible & G is right-invertible ) )
by Th1;

Lm3: for G being non empty multMagma holds
( G is cancelable iff ( G is left-cancelable & G is right-cancelable ) )

proof end;

Lm4: for G being non empty multMagma st G is associative & G is invertible holds
G is Group-like

proof end;

registration

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

coherence by Th15;

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

coherence by Lm4;

end;

registration

cluster non empty invertible -> non empty left-invertible right-invertible for multMagma ;

coherence by Lm2;

cluster non empty left-invertible right-invertible -> non empty invertible for multMagma ;

coherence by Lm2;

cluster non empty cancelable -> non empty left-cancelable right-cancelable for multMagma ;

coherence by Lm3;

cluster non empty left-cancelable right-cancelable -> non empty cancelable for multMagma ;

coherence by Lm3;

cluster non empty associative invertible -> non empty unital cancelable for multMagma ;

proof end;

end;

deffunc H₃( 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;

proof end;

end;

:: deftheorem Def21 defines well-unital MONOID_0:def 21 :

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 ) ) ;

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 by BINOP_1:def 8;

registration

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

proof end;

end;

definition

mode Monoid is non empty well-unital associative 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 #);

proof end;

end;

:: deftheorem Def22 defines MonoidalExtension MONOID_0:def 22 :

registration

let G be non empty multMagma ;

cluster -> non empty for MonoidalExtension of G;

proof 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 end;

registration

let G be multMagma ;

cluster strict for MonoidalExtension of G;

proof 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 end;

registration

let G be constituted-Functions multMagma ;

cluster -> constituted-Functions for MonoidalExtension of G;

proof end;

end;

registration

let G be constituted-FinSeqs multMagma ;

cluster -> constituted-FinSeqs for MonoidalExtension of G;

proof end;

end;

registration

let G be non empty unital multMagma ;

cluster -> unital for MonoidalExtension of G;

coherence by Th19;

end;

registration

let G be non empty associative multMagma ;

cluster -> associative for MonoidalExtension of G;

coherence by Th19;

end;

registration

let G be non empty commutative multMagma ;

cluster -> commutative for MonoidalExtension of G;

coherence by Th19;

end;

registration

let G be non empty invertible multMagma ;

cluster -> invertible for MonoidalExtension of G;

coherence by Th19;

end;

registration

let G be non empty cancelable multMagma ;

cluster -> cancelable for MonoidalExtension of G;

coherence by Th19;

end;

registration

let G be non empty uniquely-decomposable multMagma ;

cluster -> uniquely-decomposable for MonoidalExtension of G;

coherence by Th19;

end;

registration

let G be non empty unital multMagma ;

cluster non empty strict well-unital unital for MonoidalExtension of G;

proof 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 end;

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 ;

end;

:: deftheorem Def23 defines SubStr MONOID_0:def 23 :

registration

let G be multMagma ;

cluster strict for SubStr of G;

proof end;

end;

registration

let G be non empty multMagma ;

cluster non empty strict for SubStr of G;

proof 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;

proof 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 ) );

proof end;

end;

:: deftheorem Def24 defines MonoidalSubStr MONOID_0:def 24 :

registration

let G be multMagma ;

cluster strict for MonoidalSubStr of G;

proof end;

end;

registration

let G be non empty multMagma ;

cluster non empty strict for MonoidalSubStr of G;

proof 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 );

proof end;

end;

:: deftheorem Def25 defines MonoidalSubStr MONOID_0:def 25 :

registration

let G be non empty well-unital multLoopStr ;

cluster non empty strict well-unital associative commutative idempotent invertible cancelable uniquely-decomposable for MonoidalSubStr of G;

proof end;

end;

theorem Th21: :: MONOID_0:21

for G being multMagma
for M being MonoidalSubStr of G holds M is SubStr of G

proof end;

definition

let G be multMagma ;
let M be MonoidalExtension of G;
:: original: SubStr
redefine mode SubStr of M -> SubStr of G;
coherence

proof end;

end;

definition

let G1 be multMagma ;
let G2 be SubStr of G1;
:: original: SubStr
redefine mode SubStr of G2 -> SubStr of G1;
coherence

proof end;

end;

definition

let G1 be multMagma ;
let G2 be MonoidalSubStr of G1;
:: original: SubStr
redefine mode SubStr of G2 -> SubStr of G1;
coherence

proof end;

end;

definition

let G be multMagma ;
let M be MonoidalSubStr of G;
:: original: MonoidalSubStr
redefine mode MonoidalSubStr of M -> MonoidalSubStr of G;
coherence

proof 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 end;

registration

let G be non empty constituted-Functions multMagma ;

cluster non empty -> non empty constituted-Functions for SubStr of G;

proof end;

cluster non empty -> non empty constituted-Functions for MonoidalSubStr of G;

proof end;

end;

registration

let G be non empty constituted-FinSeqs multMagma ;

cluster non empty -> non empty constituted-FinSeqs for SubStr of G;

proof end;

cluster non empty -> non empty constituted-FinSeqs for MonoidalSubStr of G;

proof end;

end;

registration

let M be non empty well-unital multLoopStr ;

cluster non empty -> non empty well-unital for MonoidalSubStr of M;

coherence by Th31;

end;

registration

let G be non empty commutative multMagma ;

cluster non empty -> non empty commutative for SubStr of G;

coherence by Th32;

cluster non empty -> non empty commutative for MonoidalSubStr of G;

proof end;

end;

registration

let G be non empty associative multMagma ;

cluster non empty -> non empty associative for SubStr of G;

coherence by Th33;

cluster non empty -> non empty associative for MonoidalSubStr of G;

proof end;

end;

registration

let G be non empty idempotent multMagma ;

cluster non empty -> non empty idempotent for SubStr of G;

coherence by Th34;

cluster non empty -> non empty idempotent for MonoidalSubStr of G;

proof end;

end;

registration

let G be non empty cancelable multMagma ;

cluster non empty -> non empty cancelable for SubStr of G;

coherence by Th35;

cluster non empty -> non empty cancelable for MonoidalSubStr of G;

proof 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 by Th37;

end;

Lm5: now :: thesis:

let G be non empty multMagma ; :: thesis:
let D be non empty Subset of G; :: thesis:
assume A1: for x, y being Element of D holds x * y in D ; :: thesis:
thus ex H being non empty strict SubStr of G st the carrier of H = D :: thesis:

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 object ; :: according to TARSKI:def 3 :: thesis:
assume x in rng ( the multF of G || D) ; :: thesis:
then consider y being object 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:

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:
thus the carrier of H = D ; :: thesis:

end;

scheme :: MONOID_0:sch 1
SubStrEx2{ F₁() -> non empty multMagma , P₁[ object ] } :

ex H being non empty strict SubStr of F₁() st
for x being Element of F₁() holds
( x in the carrier of H iff P₁[x] )

provided

A1: for x, y being Element of F₁() st P₁[x] & P₁[y] holds
P₁[x * y] and
A2: ex x being Element of F₁() st P₁[x]

proof end;

scheme :: MONOID_0:sch 2
MonoidalSubStrEx2{ F₁() -> non empty multLoopStr , P₁[ set ] } :

ex M being non empty strict MonoidalSubStr of F₁() st
for x being Element of F₁() holds
( x in the carrier of M iff P₁[x] )

provided

A1: for x, y being Element of F₁() st P₁[x] & P₁[y] holds
P₁[x * y] and
A2: P₁[ 1. F₁()]

proof end;

notation

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

end;

definition

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

coherence ;

end;

:: deftheorem defines <REAL,+> MONOID_0:def 26 :

registration

cluster <REAL,+> -> non empty strict unital associative commutative invertible cancelable ;

coherence by GROUP_1:46;

end;

theorem :: MONOID_0:38

for x being set holds
( x is Element of <REAL,+> iff x is Element of 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 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 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 ;

end;

definition

:: original: INT.Group
redefine func INT.Group -> non empty strict SubStr of <REAL,+> ;
coherence

proof end;

end;

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

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 ;

proof end;

uniqueness by Th26;

end;

:: deftheorem Def27 defines <NAT,+> MONOID_0:def 27 :

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

definition

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

existence ;
uniqueness by Th20;

end;

:: deftheorem defines <NAT,+,0> MONOID_0:def 28 :

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

definition

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

proof end;

end;

:: deftheorem defines addnat MONOID_0:def 29 :

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 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 end;

theorem :: MONOID_0:46

<NAT,+,0> = multLoopStr(# NAT,addnat,0 #)

proof end;

theorem :: MONOID_0:47

( addnat = addreal || NAT & addnat = addint || NAT )

proof end;

theorem :: MONOID_0:48

( 0 is_a_unity_wrt addnat & addnat is uniquely-decomposable )

proof end;

definition

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

coherence by Def10, Def11, Def12;

end;

:: deftheorem defines <REAL,*> MONOID_0:def 30 :

theorem :: MONOID_0:49

for x being set holds
( x is Element of <REAL,*> iff x is Element of 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 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 end;

definition

func <NAT,*> -> non empty strict unital uniquely-decomposable SubStr of <REAL,*> means :Def31: :: MONOID_0:def 31
the carrier of it = NAT ;

proof end;

uniqueness by Th26;

end;

:: deftheorem Def31 defines <NAT,*> MONOID_0:def 31 :

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

definition

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

uniqueness by Th20;
existence ;

end;

:: deftheorem defines <NAT,*,1> MONOID_0:def 32 :

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

definition

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

proof end;

end;

:: deftheorem defines multnat MONOID_0:def 33 :

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 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 end;

theorem :: MONOID_0:56

<NAT,*,1> = multLoopStr(# NAT,multnat,1 #)

proof 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 end;

definition

let D be non empty set ;

func D *+^ -> 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 ) );

proof end;

uniqueness

proof end;

end;

:: deftheorem Def34 defines *+^ MONOID_0:def 34 :

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 by Th20;

func D -concatenation -> BinOp of (D *) equals :: MONOID_0:def 36
the multF of (D *+^);

correctness

proof end;

end;

:: deftheorem defines *+^+<0> MONOID_0:def 35 :

:: deftheorem defines -concatenation MONOID_0:def 36 :

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 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 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 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 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 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 end;

theorem :: MONOID_0:66

for A, B being non empty set st A c= B holds
A *+^ is SubStr of B *+^

proof 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 end;

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 ) );

proof end;

uniqueness

proof end;

end;

:: deftheorem Def37 defines GPFuncs MONOID_0:def 37 :

registration

let X be set ;

cluster GPFuncs X -> non empty strict unital associative constituted-Functions ;

proof 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 ;
uniqueness by Th20;

func X -composition -> BinOp of (PFuncs (X,X)) equals :: MONOID_0:def 39
the multF of (GPFuncs X);

correctness

proof end;

end;

:: deftheorem defines MPFuncs MONOID_0:def 38 :

:: deftheorem defines -composition MONOID_0:def 39 :

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

theorem :: MONOID_0:68

for x, X being set holds
( x is Element of (GPFuncs X) iff x is PartFunc of X,X )

proof end;

theorem Th69: :: MONOID_0:69

for X being set holds the_unity_wrt the multF of (GPFuncs X) = id X

proof 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 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 end;

theorem :: MONOID_0:72

for X, Y being set st Y c= X holds
GPFuncs Y is SubStr of GPFuncs X

proof 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);

proof end;

uniqueness by Th26;

end;

:: deftheorem Def40 defines GFuncs MONOID_0:def 40 :

registration

let X be set ;

cluster GFuncs X -> non empty strict unital ;

proof end;

end;

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

definition

let X be set ;

func MFuncs X -> strict well-unital MonoidalExtension of GFuncs X means :: MONOID_0:def 41
verum;

correctness by Th20;

end;

:: deftheorem defines MFuncs MONOID_0:def 41 :

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

theorem :: MONOID_0:73

for x, X being set holds
( x is Element of (GFuncs X) iff x is Function of X,X )

proof end;

theorem Th74: :: MONOID_0:74

for X being set holds the multF of (GFuncs X) = (X -composition) || (Funcs (X,X))

proof end;

theorem Th75: :: MONOID_0:75

for X being set holds the_unity_wrt the multF of (GFuncs X) = id X

proof 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 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 );

proof end;

uniqueness

proof end;

end;

:: deftheorem Def42 defines GPerms MONOID_0:def 42 :

registration

let X be set ;

cluster GPerms X -> non empty strict unital invertible ;