:: by Grzegorz Bancerek

::

:: Received December 29, 1992

:: Copyright (c) 1992-2012 Association of Mizar Users

begin

deffunc H

deffunc H

definition

let IT be 1-sorted ;

end;
attr IT is constituted-Functions means :Def1: :: MONOID_0:def 1

for a being Element of IT holds a is Function;

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;

for a being Element of IT holds a is FinSequence;

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

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

for IT being 1-sorted holds

( IT is constituted-FinSeqs iff for a being Element of IT holds a is FinSequence );

registration

existence

ex b_{1} being 1-sorted st b_{1} is constituted-Functions

ex b_{1} being 1-sorted st b_{1} is constituted-FinSeqs

end;
ex b

proof end;

existence ex b

proof end;

registration

let X be constituted-Functions 1-sorted ;

coherence

for b_{1} being Element of X holds

( b_{1} is Function-like & b_{1} is Relation-like )
by Def1;

end;
coherence

for b

( b

registration

coherence

for b_{1} being 1-sorted st b_{1} is constituted-FinSeqs holds

b_{1} is constituted-Functions

end;
for b

b

proof end;

registration

let X be constituted-FinSeqs 1-sorted ;

coherence

for b_{1} being Element of X holds b_{1} is FinSequence-like
by Def2;

end;
coherence

for b

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 *

end;
let p, q be FinSequence of D;

:: original: ^

redefine func p ^ q -> Element of D * ;

coherence

p ^ q is Element of D *

proof end;

definition

let D be non empty set ;

let IT be BinOp of D;

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

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;

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

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;

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;

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;

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

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

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

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

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

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

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

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

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

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

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

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

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

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 )

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;

begin

definition

let IT be non empty multMagma ;

compatibility

( IT is unital iff the multF of IT is having_a_unity )

end;
compatibility

( IT is unital iff the multF of IT is having_a_unity )

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

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 ;

compatibility

( G is commutative iff the multF of G is commutative )

( G is associative iff the multF of G is associative )

end;
compatibility

( G is commutative iff the multF of G is commutative )

proof end;

compatibility ( G is associative iff the multF of G is associative )

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

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

for G being non empty multMagma holds

( G is associative iff the multF of G is associative );

definition

let IT be non empty multMagma ;

end;
attr IT is uniquely-decomposable means :Def20: :: MONOID_0:def 20

the multF of IT is uniquely-decomposable ;

the multF of IT is uniquely-decomposable ;

:: deftheorem defines idempotent MONOID_0:def 13 :

for IT being non empty multMagma holds

( IT is idempotent iff the multF of IT is idempotent );

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

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

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

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

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

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

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

for IT being non empty multMagma holds

( IT is uniquely-decomposable iff the multF of IT is uniquely-decomposable );

registration

ex b_{1} being non empty multMagma st

( b_{1} is unital & b_{1} is commutative & b_{1} is associative & b_{1} is cancelable & b_{1} is idempotent & b_{1} is invertible & b_{1} is uniquely-decomposable & b_{1} is constituted-Functions & b_{1} is constituted-FinSeqs & b_{1} is strict )
end;

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

existence ex b

( b

proof 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

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

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

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

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

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

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

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

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

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

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

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

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

( G is invertible iff ( G is unital & the multF of G is having_an_inverseOp ) )

proof end;

Lm3: for G being non empty multMagma holds

( G is invertible iff ( G is left-invertible & G is right-invertible ) )

proof end;

Lm4: for G being non empty multMagma holds

( G is cancelable iff ( G is left-cancelable & G is right-cancelable ) )

proof end;

Lm5: for G being non empty multMagma st G is associative & G is invertible holds

G is Group-like

proof end;

registration

coherence

for b_{1} being non empty multMagma st b_{1} is associative & b_{1} is Group-like holds

b_{1} is invertible

for b_{1} being non empty multMagma st b_{1} is associative & b_{1} is invertible holds

b_{1} is Group-like
by Lm5;

end;
for b

b

proof end;

coherence for b

b

registration

coherence

for b_{1} being non empty multMagma st b_{1} is invertible holds

( b_{1} is left-invertible & b_{1} is right-invertible )
by Lm3;

coherence

for b_{1} being non empty multMagma st b_{1} is left-invertible & b_{1} is right-invertible holds

b_{1} is invertible
by Lm3;

coherence

for b_{1} being non empty multMagma st b_{1} is cancelable holds

( b_{1} is left-cancelable & b_{1} is right-cancelable )
by Lm4;

coherence

for b_{1} being non empty multMagma st b_{1} is left-cancelable & b_{1} is right-cancelable holds

b_{1} is cancelable
by Lm4;

coherence

for b_{1} being non empty multMagma st b_{1} is associative & b_{1} is invertible holds

( b_{1} is unital & b_{1} is cancelable )

end;
for b

( b

coherence

for b

b

coherence

for b

( b

coherence

for b

b

coherence

for b

( b

proof end;

begin

deffunc H

definition

let IT be non empty multLoopStr ;

( IT is well-unital iff 1. IT is_a_unity_wrt the multF of IT )

end;
redefine attr IT is well-unital means :Def21: :: MONOID_0:def 21

1. IT is_a_unity_wrt the multF of IT;

compatibility 1. IT is_a_unity_wrt the multF of IT;

( IT is well-unital iff 1. IT is_a_unity_wrt the multF of IT )

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

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

( M is well-unital iff for a being Element of M holds

( (1. M) * a = a & a * (1. M) = a ) )

proof end;

registration

ex b_{1} being non empty multLoopStr st

( b_{1} is well-unital & b_{1} is commutative & b_{1} is associative & b_{1} is cancelable & b_{1} is idempotent & b_{1} is invertible & b_{1} is uniquely-decomposable & b_{1} is unital & b_{1} is constituted-Functions & b_{1} is constituted-FinSeqs & b_{1} is strict )
end;

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

existence ex b

( b

proof end;

definition

let G be multMagma ;

ex b_{1} being multLoopStr st multMagma(# the carrier of b_{1}, the multF of b_{1} #) = multMagma(# the carrier of G, the multF of G #)

end;
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 multMagma(# the carrier of it, the multF of it #) = multMagma(# the carrier of G, the multF of G #);

ex b

proof end;

:: deftheorem Def22 defines MonoidalExtension MONOID_0:def 22 :

for G being multMagma

for b_{2} being multLoopStr holds

( b_{2} is MonoidalExtension of G iff multMagma(# the carrier of b_{2}, the multF of b_{2} #) = multMagma(# the carrier of G, the multF of G #) );

for G being multMagma

for b

( b

registration

let G be non empty multMagma ;

coherence

for b_{1} being MonoidalExtension of G holds not b_{1} is empty

end;
coherence

for b

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

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

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 ;

coherence

for b_{1} being MonoidalExtension of G holds b_{1} is constituted-Functions

end;
coherence

for b

proof end;

registration

let G be constituted-FinSeqs multMagma ;

coherence

for b_{1} being MonoidalExtension of G holds b_{1} is constituted-FinSeqs

end;
coherence

for b

proof end;

registration

let G be non empty unital multMagma ;

coherence

for b_{1} being MonoidalExtension of G holds b_{1} is unital
by Th19;

end;
coherence

for b

registration

let G be non empty associative multMagma ;

coherence

for b_{1} being MonoidalExtension of G holds b_{1} is associative
by Th19;

end;
coherence

for b

registration

let G be non empty commutative multMagma ;

coherence

for b_{1} being MonoidalExtension of G holds b_{1} is commutative
by Th19;

end;
coherence

for b

registration

let G be non empty invertible multMagma ;

coherence

for b_{1} being MonoidalExtension of G holds b_{1} is invertible
by Th19;

end;
coherence

for b

registration

let G be non empty cancelable multMagma ;

coherence

for b_{1} being MonoidalExtension of G holds b_{1} is cancelable
by Th19;

end;
coherence

for b

registration

let G be non empty uniquely-decomposable multMagma ;

coherence

for b_{1} being MonoidalExtension of G holds b_{1} is uniquely-decomposable
by Th19;

end;
coherence

for b

registration

let G be non empty unital multMagma ;

existence

ex b_{1} being MonoidalExtension of G st

( b_{1} is well-unital & b_{1} is strict )

end;
existence

ex b

( b

proof 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

for M1, M2 being strict well-unital MonoidalExtension of G holds M1 = M2

proof end;

begin

definition
end;

:: deftheorem Def23 defines SubStr MONOID_0:def 23 :

for G, b_{2} being multMagma holds

( b_{2} is SubStr of G iff the multF of b_{2} c= the multF of G );

for G, b

( b

registration
end;

registration

let G be non empty multMagma ;

existence

ex b_{1} being SubStr of G st

( b_{1} is strict & not b_{1} is empty )

end;
existence

ex b

( b

proof end;

registration

let G be non empty unital multMagma ;

ex b_{1} being non empty SubStr of G st

( b_{1} is unital & b_{1} is associative & b_{1} is commutative & b_{1} is cancelable & b_{1} is idempotent & b_{1} is invertible & b_{1} is uniquely-decomposable & b_{1} is strict )

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

existence ex b

( b

proof end;

definition

let G be multMagma ;

ex b_{1} being multLoopStr st

( the multF of b_{1} c= the multF of G & ( for M being multLoopStr st G = M holds

1. b_{1} = 1. M ) )

end;
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 ( the multF of it c= the multF of G & ( for M being multLoopStr st G = M holds

1. it = 1. M ) );

ex b

( the multF of b

1. b

proof end;

:: deftheorem Def24 defines MonoidalSubStr MONOID_0:def 24 :

for G being multMagma

for b_{2} being multLoopStr holds

( b_{2} is MonoidalSubStr of G iff ( the multF of b_{2} c= the multF of G & ( for M being multLoopStr st G = M holds

1. b_{2} = 1. M ) ) );

for G being multMagma

for b

( b

1. b

registration
end;

registration

let G be non empty multMagma ;

existence

ex b_{1} being MonoidalSubStr of G st

( b_{1} is strict & not b_{1} is empty )

end;
existence

ex b

( b

proof end;

definition

let M be multLoopStr ;

for b_{1} being multLoopStr holds

( b_{1} is MonoidalSubStr of M iff ( the multF of b_{1} c= the multF of M & 1. b_{1} = 1. M ) )

end;
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 ( the multF of it c= the multF of M & 1. it = 1. M );

for b

( b

proof end;

:: deftheorem Def25 defines MonoidalSubStr MONOID_0:def 25 :

for M, b_{2} being multLoopStr holds

( b_{2} is MonoidalSubStr of M iff ( the multF of b_{2} c= the multF of M & 1. b_{2} = 1. M ) );

for M, b

( b

registration

let G be non empty well-unital multLoopStr ;

ex b_{1} being non empty MonoidalSubStr of G st

( b_{1} is well-unital & b_{1} is associative & b_{1} is commutative & b_{1} is cancelable & b_{1} is idempotent & b_{1} is invertible & b_{1} is uniquely-decomposable & b_{1} is strict )

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

existence ex b

( b

proof end;

definition

let G be multMagma ;

let M be MonoidalExtension of G;

:: original: SubStr

redefine mode SubStr of M -> SubStr of G;

coherence

for b_{1} being SubStr of M holds b_{1} is SubStr of G

end;
let M be MonoidalExtension of G;

:: original: SubStr

redefine mode SubStr of M -> SubStr of G;

coherence

for b

proof end;

definition

let G1 be multMagma ;

let G2 be SubStr of G1;

:: original: SubStr

redefine mode SubStr of G2 -> SubStr of G1;

coherence

for b_{1} being SubStr of G2 holds b_{1} is SubStr of G1

end;
let G2 be SubStr of G1;

:: original: SubStr

redefine mode SubStr of G2 -> SubStr of G1;

coherence

for b

proof end;

definition

let G1 be multMagma ;

let G2 be MonoidalSubStr of G1;

:: original: SubStr

redefine mode SubStr of G2 -> SubStr of G1;

coherence

for b_{1} being SubStr of G2 holds b_{1} is SubStr of G1

end;
let G2 be MonoidalSubStr of G1;

:: original: SubStr

redefine mode SubStr of G2 -> SubStr of G1;

coherence

for b

proof end;

definition

let G be multMagma ;

let M be MonoidalSubStr of G;

:: original: MonoidalSubStr

redefine mode MonoidalSubStr of M -> MonoidalSubStr of G;

coherence

for b_{1} being MonoidalSubStr of M holds b_{1} is MonoidalSubStr of G

end;
let M be MonoidalSubStr of G;

:: original: MonoidalSubStr

redefine mode MonoidalSubStr of M -> MonoidalSubStr of G;

coherence

for b

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

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 )

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

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

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

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

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

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

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 )

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

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

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

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

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

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

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

for N being non empty MonoidalSubStr of M holds N is uniquely-decomposable

proof end;

registration

let G be non empty constituted-Functions multMagma ;

coherence

for b_{1} being non empty SubStr of G holds b_{1} is constituted-Functions

for b_{1} being non empty MonoidalSubStr of G holds b_{1} is constituted-Functions

end;
coherence

for b

proof end;

coherence for b

proof end;

registration

let G be non empty constituted-FinSeqs multMagma ;

coherence

for b_{1} being non empty SubStr of G holds b_{1} is constituted-FinSeqs

for b_{1} being non empty MonoidalSubStr of G holds b_{1} is constituted-FinSeqs

end;
coherence

for b

proof end;

coherence for b

proof end;

registration

let M be non empty well-unital multLoopStr ;

coherence

for b_{1} being non empty MonoidalSubStr of M holds b_{1} is well-unital
by Th31;

end;
coherence

for b

registration

let G be non empty commutative multMagma ;

coherence

for b_{1} being non empty SubStr of G holds b_{1} is commutative
by Th32;

coherence

for b_{1} being non empty MonoidalSubStr of G holds b_{1} is commutative

end;
coherence

for b

coherence

for b

proof end;

registration

let G be non empty associative multMagma ;

coherence

for b_{1} being non empty SubStr of G holds b_{1} is associative
by Th33;

coherence

for b_{1} being non empty MonoidalSubStr of G holds b_{1} is associative

end;
coherence

for b

coherence

for b

proof end;

registration

let G be non empty idempotent multMagma ;

coherence

for b_{1} being non empty SubStr of G holds b_{1} is idempotent
by Th34;

coherence

for b_{1} being non empty MonoidalSubStr of G holds b_{1} is idempotent

end;
coherence

for b

coherence

for b

proof end;

registration

let G be non empty cancelable multMagma ;

coherence

for b_{1} being non empty SubStr of G holds b_{1} is cancelable
by Th35;

coherence

for b_{1} being non empty MonoidalSubStr of G holds b_{1} is cancelable

end;
coherence

for b

coherence

for b

proof end;

registration

let M be non empty well-unital uniquely-decomposable multLoopStr ;

coherence

for b_{1} being non empty MonoidalSubStr of M holds b_{1} is uniquely-decomposable
by Th37;

end;
coherence

for b

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

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

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

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

dom ( the multF of G || D) = [:D,D:]
by A2, RELAT_1:62;
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;
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

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

scheme :: MONOID_0:sch 1

SubStrEx2{ F_{1}() -> non empty multMagma , P_{1}[ set ] } :

SubStrEx2{ F

ex H being non empty strict SubStr of F_{1}() st

for x being Element of F_{1}() holds

( x in the carrier of H iff P_{1}[x] )

providedfor x being Element of F

( x in the carrier of H iff P

A1:
for x, y being Element of F_{1}() st P_{1}[x] & P_{1}[y] holds

P_{1}[x * y]
and

A2: ex x being Element of F_{1}() st P_{1}[x]

P

A2: ex x being Element of F

proof end;

scheme :: MONOID_0:sch 2

MonoidalSubStrEx2{ F_{1}() -> non empty multLoopStr , P_{1}[ set ] } :

MonoidalSubStrEx2{ F

ex M being non empty strict MonoidalSubStr of F_{1}() st

for x being Element of F_{1}() holds

( x in the carrier of M iff P_{1}[x] )

providedfor x being Element of F

( x in the carrier of M iff P

A1:
for x, y being Element of F_{1}() st P_{1}[x] & P_{1}[y] holds

P_{1}[x * y]
and

A2: P_{1}[ 1. F_{1}()]

P

A2: P

proof end;

begin

registration

coherence

( <REAL,+> is unital & <REAL,+> is associative & <REAL,+> is invertible & <REAL,+> is commutative & <REAL,+> is cancelable & <REAL,+> is strict ) by GROUP_1:46;

end;
( <REAL,+> is unital & <REAL,+> is associative & <REAL,+> is invertible & <REAL,+> is commutative & <REAL,+> is cancelable & <REAL,+> is strict ) by GROUP_1:46;

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

for a, b being Element of N

for x, y being Real st a = x & b = y holds

a * b = x + y

proof end;

registration

let G be non empty unital multMagma ;

coherence

for b_{1} being non empty SubStr of G st b_{1} is associative & b_{1} is invertible holds

( b_{1} is unital & b_{1} is cancelable & b_{1} is Group-like )
;

end;
coherence

for b

( b

definition

:: original: INT.Group

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

coherence

INT.Group is non empty strict SubStr of <REAL,+>

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

coherence

INT.Group is non empty strict SubStr of <REAL,+>

proof end;

:: corollary

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

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

theorem :: MONOID_0:41

theorem :: MONOID_0:42

definition

ex b_{1} being non empty strict unital uniquely-decomposable SubStr of INT.Group st the carrier of b_{1} = NAT

for b_{1}, b_{2} being non empty strict unital uniquely-decomposable SubStr of INT.Group st the carrier of b_{1} = NAT & the carrier of b_{2} = NAT holds

b_{1} = b_{2}
by Th26;

end;

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

the carrier of it = NAT ;

existence the carrier of it = NAT ;

ex b

proof end;

uniqueness for b

b

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

for b_{1} being non empty strict unital uniquely-decomposable SubStr of INT.Group holds

( b_{1} = <NAT,+> iff the carrier of b_{1} = NAT );

for b

( b

:: corollary

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

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

definition

ex b_{1} being non empty strict well-unital MonoidalExtension of <NAT,+> st verum
;

uniqueness

for b_{1}, b_{2} being non empty strict well-unital MonoidalExtension of <NAT,+> holds b_{1} = b_{2}
by Th20;

end;

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

verum;

existence verum;

ex b

uniqueness

for b

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

for b_{1} being non empty strict well-unital MonoidalExtension of <NAT,+> holds

( b_{1} = <NAT,+,0> iff verum );

for b

( b

:: corollary

:: <NAT,+,0> is

:: well-unital commutative associative cancelable uniquely-decomposable;

:: <NAT,+,0> is

:: well-unital commutative associative cancelable uniquely-decomposable;

definition

compatibility

for b_{1} being Element of bool [:[:NAT,NAT:],NAT:] holds

( b_{1} = addnat iff b_{1} = the multF of <NAT,+> )

end;
for b

( b

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

for m1, m2 being Element of <NAT,+,0> st n1 = m1 & n2 = m2 holds

m1 * m2 = n1 + n2

proof end;

definition

multMagma(# REAL,multreal #) is non empty strict unital associative commutative multMagma by Def10, Def11, Def12;

end;

func <REAL,*> -> non empty strict unital associative commutative multMagma equals :: MONOID_0:def 30

multMagma(# REAL,multreal #);

coherence multMagma(# REAL,multreal #);

multMagma(# REAL,multreal #) is non empty strict unital associative commutative multMagma by Def10, Def11, Def12;

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

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 )

( the_unity_wrt the multF of N = 0 or the_unity_wrt the multF of N = 1 )

proof end;

definition

ex b_{1} being non empty strict unital uniquely-decomposable SubStr of <REAL,*> st the carrier of b_{1} = NAT

for b_{1}, b_{2} being non empty strict unital uniquely-decomposable SubStr of <REAL,*> st the carrier of b_{1} = NAT & the carrier of b_{2} = NAT holds

b_{1} = b_{2}
by Th26;

end;

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

the carrier of it = NAT ;

existence the carrier of it = NAT ;

ex b

proof end;

uniqueness for b

b

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

for b_{1} being non empty strict unital uniquely-decomposable SubStr of <REAL,*> holds

( b_{1} = <NAT,*> iff the carrier of b_{1} = NAT );

for b

( b

:: corollary

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

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

definition

for b_{1}, b_{2} being non empty strict well-unital MonoidalExtension of <NAT,*> holds b_{1} = b_{2}
by Th20;

existence

ex b_{1} being non empty strict well-unital MonoidalExtension of <NAT,*> st verum
;

end;

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

verum;

uniqueness verum;

for b

existence

ex b

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

for b_{1} being non empty strict well-unital MonoidalExtension of <NAT,*> holds

( b_{1} = <NAT,*,1> iff verum );

for b

( b

:: corollary

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

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

definition

compatibility

for b_{1} being Element of bool [:[:NAT,NAT:],NAT:] holds

( b_{1} = multnat iff b_{1} = the multF of <NAT,*> )

end;
for b

( b

proof end;

theorem :: MONOID_0:53

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

for m1, m2 being Element of <NAT,*,1> st n1 = m1 & n2 = m2 holds

m1 * m2 = n1 * n2

proof end;

begin

definition

let D be non empty set ;

ex b_{1} being non empty strict unital associative constituted-FinSeqs cancelable uniquely-decomposable multMagma st

( the carrier of b_{1} = D * & ( for p, q being Element of b_{1} holds p [*] q = p ^ q ) )

for b_{1}, b_{2} being non empty strict unital associative constituted-FinSeqs cancelable uniquely-decomposable multMagma st the carrier of b_{1} = D * & ( for p, q being Element of b_{1} holds p [*] q = p ^ q ) & the carrier of b_{2} = D * & ( for p, q being Element of b_{2} holds p [*] q = p ^ q ) holds

b_{1} = b_{2}

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

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

ex b

( the carrier of b

proof end;

uniqueness for b

b

proof end;

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

for D being non empty set

for b_{2} being non empty strict unital associative constituted-FinSeqs cancelable uniquely-decomposable multMagma holds

( b_{2} = D *+^ iff ( the carrier of b_{2} = D * & ( for p, q being Element of b_{2} holds p [*] q = p ^ q ) ) );

for D being non empty set

for b

( b

definition

let D be non empty set ;

existence

ex b_{1} being non empty strict well-unital MonoidalExtension of D *+^ st verum;

uniqueness

for b_{1}, b_{2} being non empty strict well-unital MonoidalExtension of D *+^ holds b_{1} = b_{2};

by Th20;

correctness

coherence

the multF of (D *+^) is BinOp of (D *);

end;
func D *+^+<0> -> non empty strict well-unital MonoidalExtension of D *+^ means :: MONOID_0:def 35

verum;

correctness verum;

existence

ex b

uniqueness

for b

by Th20;

correctness

coherence

the multF of (D *+^) is BinOp of (D *);

proof end;

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

for D being non empty set

for b_{2} being non empty strict well-unital MonoidalExtension of D *+^ holds

( b_{2} = D *+^+<0> iff verum );

for D being non empty set

for b

( b

:: deftheorem defines -concatenation MONOID_0:def 36 :

for D being non empty set holds D -concatenation = the multF of (D *+^);

for D being non empty set holds D -concatenation = the multF of (D *+^);

theorem :: MONOID_0:59

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>) = {} )

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

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

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 = {}

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 = {} )

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:67

for D being non empty set holds

( D -concatenation is having_a_unity & the_unity_wrt (D -concatenation) = {} & D -concatenation is associative )

( D -concatenation is having_a_unity & the_unity_wrt (D -concatenation) = {} & D -concatenation is associative )

proof end;

begin

definition

let X be set ;

ex b_{1} being strict constituted-Functions multMagma st

( the carrier of b_{1} = PFuncs (X,X) & ( for f, g being Element of b_{1} holds f [*] g = g (*) f ) )

for b_{1}, b_{2} being strict constituted-Functions multMagma st the carrier of b_{1} = PFuncs (X,X) & ( for f, g being Element of b_{1} holds f [*] g = g (*) f ) & the carrier of b_{2} = PFuncs (X,X) & ( for f, g being Element of b_{2} holds f [*] g = g (*) f ) holds

b_{1} = b_{2}

end;
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 ( the carrier of it = PFuncs (X,X) & ( for f, g being Element of it holds f [*] g = g (*) f ) );

ex b

( the carrier of b

proof end;

uniqueness for b

b

proof end;

:: deftheorem Def37 defines GPFuncs MONOID_0:def 37 :

for X being set

for b_{2} being strict constituted-Functions multMagma holds

( b_{2} = GPFuncs X iff ( the carrier of b_{2} = PFuncs (X,X) & ( for f, g being Element of b_{2} holds f [*] g = g (*) f ) ) );

for X being set

for b

( b

registration

let X be set ;

coherence

( GPFuncs X is unital & GPFuncs X is associative & not GPFuncs X is empty )

end;
coherence

( GPFuncs X is unital & GPFuncs X is associative & not GPFuncs X is empty )

proof end;

definition

let X be set ;

ex b_{1} being non empty strict well-unital MonoidalExtension of GPFuncs X st verum
;

uniqueness

for b_{1}, b_{2} being non empty strict well-unital MonoidalExtension of GPFuncs X holds b_{1} = b_{2}
by Th20;

correctness

coherence

the multF of (GPFuncs X) is BinOp of (PFuncs (X,X));

end;
func MPFuncs X -> non empty strict well-unital MonoidalExtension of GPFuncs X means :: MONOID_0:def 38

verum;

existence verum;

ex b

uniqueness

for b

correctness

coherence

the multF of (GPFuncs X) is BinOp of (PFuncs (X,X));

proof end;

:: deftheorem defines MPFuncs MONOID_0:def 38 :

for X being set

for b_{2} being non empty strict well-unital MonoidalExtension of GPFuncs X holds

( b_{2} = MPFuncs X iff verum );

for X being set

for b

( b

:: deftheorem defines -composition MONOID_0:def 39 :

for X being set holds X -composition = the multF of (GPFuncs X);

for X being set holds X -composition = the multF of (GPFuncs X);

:: corollary

:: MPFuncs X is constituted-Functions strict Monoid;

:: MPFuncs X is constituted-Functions strict Monoid;

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

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 )

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;

definition

let X be set ;

ex b_{1} being strict SubStr of GPFuncs X st the carrier of b_{1} = Funcs (X,X)

for b_{1}, b_{2} being strict SubStr of GPFuncs X st the carrier of b_{1} = Funcs (X,X) & the carrier of b_{2} = Funcs (X,X) holds

b_{1} = b_{2}
by Th26;

end;
func GFuncs X -> strict SubStr of GPFuncs X means :Def40: :: MONOID_0:def 40

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

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

ex b

proof end;

uniqueness for b

b

:: deftheorem Def40 defines GFuncs MONOID_0:def 40 :

for X being set

for b_{2} being strict SubStr of GPFuncs X holds

( b_{2} = GFuncs X iff the carrier of b_{2} = Funcs (X,X) );

for X being set

for b

( b

registration
end;

:: corollary

:: GFuncs X is unital associative constituted-Functions;

:: GFuncs X is unital associative constituted-Functions;

definition

let X be set ;

correctness

existence

ex b_{1} being strict well-unital MonoidalExtension of GFuncs X st verum;

uniqueness

for b_{1}, b_{2} being strict well-unital MonoidalExtension of GFuncs X holds b_{1} = b_{2};

by Th20;

end;
correctness

existence

ex b

uniqueness

for b

by Th20;

:: deftheorem defines MFuncs MONOID_0:def 41 :

for X being set

for b_{2} being strict well-unital MonoidalExtension of GFuncs X holds

( b_{2} = MFuncs X iff verum );

for X being set

for b

( b

:: corollary

:: GFuncs X is constituted-Functions Monoid;

:: GFuncs X is constituted-Functions Monoid;

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 )

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

ex b_{1} being non empty strict SubStr of GFuncs X st

for f being Element of (GFuncs X) holds

( f in the carrier of b_{1} iff f is Permutation of X )

for b_{1}, b_{2} being non empty strict SubStr of GFuncs X st ( for f being Element of (GFuncs X) holds

( f in the carrier of b_{1} iff f is Permutation of X ) ) & ( for f being Element of (GFuncs X) holds

( f in the carrier of b_{2} iff f is Permutation of X ) ) holds

b_{1} = b_{2}

end;
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 for f being Element of (GFuncs X) holds

( f in the carrier of it iff f is Permutation of X );

ex b

for f being Element of (GFuncs X) holds

( f in the carrier of b

proof end;

uniqueness for b

( f in the carrier of b

( f in the carrier of b

b

proof end;

:: deftheorem Def42 defines GPerms MONOID_0:def 42 :

for X being set

for b_{2} being non empty strict SubStr of GFuncs X holds

( b_{2} = GPerms X iff for f being Element of (GFuncs X) holds

( f in the carrier of b_{2} iff f is Permutation of X ) );

for X being set

for b

( b

( f in the carrier of b

registration
end;

:: corollary

:: GPerms X is constituted-Functions Group;

:: GPerms X is constituted-Functions Group;

:: 2005.05.13, A.T.

theorem :: MONOID_0:81

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

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

::: cluster INT.Group -> unital invertible;

::: coherence;

:::end;