:: Monoid of Multisets and Subsets
:: by Grzegorz Bancerek
::
:: Received December 29, 1992
:: Copyright (c) 1992-2011 Association of Mizar Users

begin

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

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

definition

let f be Function;
let x1, x2, y be set ;
func f .. (x1,x2,y) -> set equals :: MONOID_1:def 1
f .. ([x1,x2],y);
correctness
coherence
f .. ([x1,x2],y) is set ;
;

end;

:: deftheorem defines .. MONOID_1:def 1 :
for f being Function
for x1, x2, y being set holds f .. (x1,x2,y) = f .. ([x1,x2],y);

definition

let A, D1, D2, D be non empty set ;
let f be Function of [:D1,D2:],(Funcs (A,D));
let x1 be Element of D1;
let x2 be Element of D2;
let x be Element of A;
:: original: ..
redefine func f .. (x1,x2,x) -> Element of D;
coherence
f .. (x1,x2,x) is Element of D

proof end;

end;

definition

let A be set ;
let D1, D2, D be non empty set ;
let f be Function of [:D1,D2:],D;
let g1 be Function of A,D1;
let g2 be Function of A,D2;
:: original: .:
redefine func f .: (g1,g2) -> Element of Funcs (A,D);
coherence
f .: (g1,g2) is Element of Funcs (A,D)

proof end;

end;

notation

let A be non empty set ;
let n be Element of NAT ;
let x be Element of A;
synonym n .--> x for A |-> n;

end;

definition

let A be non empty set ;
let n be Element of NAT ;
let x be Element of A;
:: original: .-->
redefine func n .--> x -> FinSequence of A;
coherence
x .--> is FinSequence of A by FINSEQ_2:77;

end;

definition

let D be non empty set ;
let A be set ;
let d be Element of D;
:: original: -->
redefine func A --> d -> Element of Funcs (A,D);
coherence
A --> d is Element of Funcs (A,D)

proof end;

end;

definition

let A be set ;
let D1, D2, D be non empty set ;
let f be Function of [:D1,D2:],D;
let d be Element of D1;
let g be Function of A,D2;
:: original: [;]
redefine func f [;] (d,g) -> Element of Funcs (A,D);
coherence
f [;] (d,g) is Element of Funcs (A,D)

proof end;

end;

definition

let A be set ;
let D1, D2, D be non empty set ;
let f be Function of [:D1,D2:],D;
let g be Function of A,D1;
let d be Element of D2;
:: original: [:]
redefine func f [:] (g,d) -> Element of Funcs (A,D);
coherence
f [:] (g,d) is Element of Funcs (A,D)

proof end;

end;

theorem :: MONOID_1:1

canceled;

theorem :: MONOID_1:2

for f, g being Function
for X being set holds (f | X) * g = f * (X | g)

proof end;

scheme :: MONOID_1:sch 1
NonUniqFuncDEx{ F₁() -> set , F₂() -> non empty set , P₁[ set , set ] } :

ex f being Function of F₁(),F₂() st
for x being set st x in F₁() holds
P₁[x,f . x]

provided

A1: for x being set st x in F₁() holds
ex y being Element of F₂() st P₁[x,y]

proof end;

begin

definition

let D1, D2, D be non empty set ;
let f be Function of [:D1,D2:],D;
let A be set ;
func (f,D) .: A -> Function of [:(Funcs (A,D1)),(Funcs (A,D2)):],(Funcs (A,D)) means :Def2: :: MONOID_1:def 2
for f1 being Element of Funcs (A,D1)
for f2 being Element of Funcs (A,D2) holds it . (f1,f2) = f .: (f1,f2);
existence
ex b₁ being Function of [:(Funcs (A,D1)),(Funcs (A,D2)):],(Funcs (A,D)) st
for f1 being Element of Funcs (A,D1)
for f2 being Element of Funcs (A,D2) holds b₁ . (f1,f2) = f .: (f1,f2)

proof end;

uniqueness
for b₁, b₂ being Function of [:(Funcs (A,D1)),(Funcs (A,D2)):],(Funcs (A,D)) st ( for f1 being Element of Funcs (A,D1)
for f2 being Element of Funcs (A,D2) holds b₁ . (f1,f2) = f .: (f1,f2) ) & ( for f1 being Element of Funcs (A,D1)
for f2 being Element of Funcs (A,D2) holds b₂ . (f1,f2) = f .: (f1,f2) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def2 defines .: MONOID_1:def 2 :
for D1, D2, D being non empty set
for f being Function of [:D1,D2:],D
for A being set
for b₆ being Function of [:(Funcs (A,D1)),(Funcs (A,D2)):],(Funcs (A,D)) holds
( b₆ = (f,D) .: A iff for f1 being Element of Funcs (A,D1)
for f2 being Element of Funcs (A,D2) holds b₆ . (f1,f2) = f .: (f1,f2) );

theorem :: MONOID_1:3

for D1, D2, D being non empty set
for f being Function of [:D1,D2:],D
for A being set
for f1 being Function of A,D1
for f2 being Function of A,D2
for x being set st x in A holds
((f,D) .: A) .. (f1,f2,x) = f . ((f1 . x),(f2 . x))

proof end;

theorem Th4: :: MONOID_1:4

for A being set
for D being non empty set
for o being BinOp of D
for f, g being Function of A,D st o is commutative holds
o .: (f,g) = o .: (g,f)

proof end;

theorem Th5: :: MONOID_1:5

for A being set
for D being non empty set
for o being BinOp of D
for f, g, h being Function of A,D st o is associative holds
o .: ((o .: (f,g)),h) = o .: (f,(o .: (g,h)))

proof end;

theorem Th6: :: MONOID_1:6

for A being set
for D being non empty set
for a being Element of D
for o being BinOp of D
for f being Function of A,D st a is_a_unity_wrt o holds
( o [;] (a,f) = f & o [:] (f,a) = f )

proof end;

theorem Th7: :: MONOID_1:7

for A being set
for D being non empty set
for o being BinOp of D
for f being Function of A,D st o is idempotent holds
o .: (f,f) = f

proof end;

theorem Th8: :: MONOID_1:8

for A being set
for D being non empty set
for o being BinOp of D st o is commutative holds
(o,D) .: A is commutative

proof end;

theorem Th9: :: MONOID_1:9

for A being set
for D being non empty set
for o being BinOp of D st o is associative holds
(o,D) .: A is associative

proof end;

theorem Th10: :: MONOID_1:10

for A being set
for D being non empty set
for a being Element of D
for o being BinOp of D st a is_a_unity_wrt o holds
A --> a is_a_unity_wrt (o,D) .: A

proof end;

theorem Th11: :: MONOID_1:11

for A being set
for D being non empty set
for o being BinOp of D st o is having_a_unity holds
( the_unity_wrt ((o,D) .: A) = A --> (the_unity_wrt o) & (o,D) .: A is having_a_unity )

proof end;

theorem Th12: :: MONOID_1:12

for A being set
for D being non empty set
for o being BinOp of D st o is idempotent holds
(o,D) .: A is idempotent

proof end;

theorem Th13: :: MONOID_1:13

for A being set
for D being non empty set
for o being BinOp of D st o is invertible holds
(o,D) .: A is invertible

proof end;

theorem Th14: :: MONOID_1:14

for A being set
for D being non empty set
for o being BinOp of D st o is cancelable holds
(o,D) .: A is cancelable

proof end;

theorem Th15: :: MONOID_1:15

for A being set
for D being non empty set
for o being BinOp of D st o is uniquely-decomposable holds
(o,D) .: A is uniquely-decomposable

proof end;

theorem :: MONOID_1:16

for A being set
for D being non empty set
for o, o9 being BinOp of D st o absorbs o9 holds
(o,D) .: A absorbs (o9,D) .: A

proof end;

theorem Th17: :: MONOID_1:17

for A being set
for D1, D2, D, E1, E2, E being non empty set
for o1 being Function of [:D1,D2:],D
for o2 being Function of [:E1,E2:],E st o1 c= o2 holds
(o1,D) .: A c= (o2,E) .: A

proof end;

definition

let G be non empty multMagma ;
let A be set ;
func .: (G,A) -> multMagma equals :Def3: :: MONOID_1:def 3
multLoopStr(# (Funcs (A, the carrier of G)),(( the multF of G, the carrier of G) .: A),(A --> (the_unity_wrt the multF of G)) #) if G is unital
otherwise multMagma(# (Funcs (A, the carrier of G)),(( the multF of G, the carrier of G) .: A) #);
correctness
coherence
( ( G is unital implies multLoopStr(# (Funcs (A, the carrier of G)),(( the multF of G, the carrier of G) .: A),(A --> (the_unity_wrt the multF of G)) #) is multMagma ) & ( not G is unital implies multMagma(# (Funcs (A, the carrier of G)),(( the multF of G, the carrier of G) .: A) #) is multMagma ) );
consistency
for b₁ being multMagma holds verum;
;

end;

:: deftheorem Def3 defines .: MONOID_1:def 3 :
for G being non empty multMagma
for A being set holds
( ( G is unital implies .: (G,A) = multLoopStr(# (Funcs (A, the carrier of G)),(( the multF of G, the carrier of G) .: A),(A --> (the_unity_wrt the multF of G)) #) ) & ( not G is unital implies .: (G,A) = multMagma(# (Funcs (A, the carrier of G)),(( the multF of G, the carrier of G) .: A) #) ) );

registration

let G be non empty multMagma ;
let A be set ;
cluster .: (G,A) -> non empty ;
coherence
not .: (G,A) is empty

proof end;

end;

deffunc H₃( non empty multMagma ) -> set = the carrier of $1;

theorem Th18: :: MONOID_1:18

for X being set
for G being non empty multMagma holds
( the carrier of (.: (G,X)) = Funcs (X, the carrier of G) & the multF of (.: (G,X)) = ( the multF of G, the carrier of G) .: X )

proof end;

theorem :: MONOID_1:19

for x, X being set
for G being non empty multMagma holds
( x is Element of (.: (G,X)) iff x is Function of X, the carrier of G )

proof end;

Lm1: for X being set
for G being non empty multMagma holds .: (G,X) is constituted-Functions

proof end;

registration

let G be non empty multMagma ;
let A be set ;
cluster .: (G,A) -> constituted-Functions ;
coherence
.: (G,A) is constituted-Functions by Lm1;

end;

theorem Th20: :: MONOID_1:20

for X being set
for G being non empty multMagma
for f being Element of (.: (G,X)) holds
( dom f = X & rng f c= the carrier of G )

proof end;

theorem Th21: :: MONOID_1:21

for X being set
for G being non empty multMagma
for f, g being Element of (.: (G,X)) st ( for x being set st x in X holds
f . x = g . x ) holds
f = g

proof end;

definition

let G be non empty multMagma ;
let A be non empty set ;
let f be Element of (.: (G,A));
let a be Element of A;
:: original: .
redefine func f . a -> Element of G;
coherence
f . a is Element of G

proof end;

end;

registration

let G be non empty multMagma ;
let A be non empty set ;
let f be Element of (.: (G,A));
cluster proj2 f -> non empty ;
coherence
not rng f is empty

proof end;

end;

theorem Th22: :: MONOID_1:22

for D being non empty set
for G being non empty multMagma
for f1, f2 being Element of (.: (G,D))
for a being Element of D holds (f1 * f2) . a = (f1 . a) * (f2 . a)

proof end;

definition

let G be non empty unital multMagma ;
let A be set ;
:: original: .:
redefine func .: (G,A) -> non empty strict well-unital constituted-Functions multLoopStr ;
coherence
.: (G,A) is non empty strict well-unital constituted-Functions multLoopStr

proof end;

end;

theorem Th23: :: MONOID_1:23

for X being set
for G being non empty unital multMagma holds 1. (.: (G,X)) = X --> (the_unity_wrt the multF of G)

proof end;

theorem Th24: :: MONOID_1:24

for G being non empty multMagma
for A being set holds
( ( G is commutative implies .: (G,A) is commutative ) & ( G is associative implies .: (G,A) is associative ) & ( G is idempotent implies .: (G,A) is idempotent ) & ( G is invertible implies .: (G,A) is invertible ) & ( G is cancelable implies .: (G,A) is cancelable ) & ( G is uniquely-decomposable implies .: (G,A) is uniquely-decomposable ) )

proof end;

theorem :: MONOID_1:25

for X being set
for G being non empty multMagma
for H being non empty SubStr of G holds .: (H,X) is SubStr of .: (G,X)

proof end;

theorem :: MONOID_1:26

for X being set
for G being non empty unital multMagma
for H being non empty SubStr of G st the_unity_wrt the multF of G in the carrier of H holds
.: (H,X) is MonoidalSubStr of .: (G,X)

proof end;

definition

let G be non empty unital associative commutative cancelable uniquely-decomposable multMagma ;
let A be set ;
:: original: .:
redefine func .: (G,A) -> strict commutative constituted-Functions cancelable uniquely-decomposable Monoid;
coherence
.: (G,A) is strict commutative constituted-Functions cancelable uniquely-decomposable Monoid

proof end;

end;

begin

definition

let A be set ;
func MultiSet_over A -> strict commutative constituted-Functions cancelable uniquely-decomposable Monoid equals :: MONOID_1:def 4
.: (<NAT,+,0>,A);
correctness
coherence
.: (<NAT,+,0>,A) is strict commutative constituted-Functions cancelable uniquely-decomposable Monoid;
;

end;

:: deftheorem defines MultiSet_over MONOID_1:def 4 :
for A being set holds MultiSet_over A = .: (<NAT,+,0>,A);

theorem Th27: :: MONOID_1:27

for X being set holds
( the carrier of (MultiSet_over X) = Funcs (X,NAT) & the multF of (MultiSet_over X) = (addnat,NAT) .: X & 1. (MultiSet_over X) = X --> 0 )

proof end;

definition

let A be set ;
mode Multiset of A is Element of (MultiSet_over A);

end;

theorem Th28: :: MONOID_1:28

for x, X being set holds
( x is Multiset of X iff x is Function of X,NAT )

proof end;

theorem Th29: :: MONOID_1:29

for X being set
for m being Multiset of X holds
( dom m = X & rng m c= NAT )

proof end;

definition

let A be non empty set ;
let m be Multiset of A;
:: original: proj2
redefine func rng m -> Subset of NAT;
coherence
proj2 m is Subset of NAT by Th20, MONOID_0:52;
let a be Element of A;
:: original: .
redefine func m . a -> Element of NAT ;
coherence
m . a is Element of NAT

proof end;

end;

theorem Th30: :: MONOID_1:30

for D being non empty set
for m1, m2 being Multiset of D
for a being Element of D holds (m1 [*] m2) . a = (m1 . a) + (m2 . a)

proof end;

theorem Th31: :: MONOID_1:31

for Y, X being set holds chi (Y,X) is Multiset of X

proof end;

definition

let Y, X be set ;
:: original: chi
redefine func chi (Y,X) -> Multiset of X;
coherence
chi (Y,X) is Multiset of X by Th31;

end;

definition

let X be set ;
let n be Element of NAT ;
:: original: -->
redefine func X --> n -> Multiset of X;
coherence
X --> n is Multiset of X

proof end;

end;

definition

let A be non empty set ;
let a be Element of A;
func chi a -> Multiset of A equals :: MONOID_1:def 5
chi ({a},A);
coherence
chi ({a},A) is Multiset of A ;

end;

:: deftheorem defines chi MONOID_1:def 5 :
for A being non empty set
for a being Element of A holds chi a = chi ({a},A);

theorem Th32: :: MONOID_1:32

for A being non empty set
for a, b being Element of A holds
( (chi a) . a = 1 & ( b <> a implies (chi a) . b = 0 ) )

proof end;

theorem Th33: :: MONOID_1:33

for A being non empty set
for m1, m2 being Multiset of A st ( for a being Element of A holds m1 . a = m2 . a ) holds
m1 = m2

proof end;

definition

let A be set ;
func finite-MultiSet_over A -> non empty strict MonoidalSubStr of MultiSet_over A means :Def6: :: MONOID_1:def 6
for f being Multiset of A holds
( f in the carrier of it iff f " (NAT \ {0}) is finite );
existence
ex b₁ being non empty strict MonoidalSubStr of MultiSet_over A st
for f being Multiset of A holds
( f in the carrier of b₁ iff f " (NAT \ {0}) is finite )

proof end;

uniqueness
for b₁, b₂ being non empty strict MonoidalSubStr of MultiSet_over A st ( for f being Multiset of A holds
( f in the carrier of b₁ iff f " (NAT \ {0}) is finite ) ) & ( for f being Multiset of A holds
( f in the carrier of b₂ iff f " (NAT \ {0}) is finite ) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def6 defines finite-MultiSet_over MONOID_1:def 6 :
for A being set
for b₂ being non empty strict MonoidalSubStr of MultiSet_over A holds
( b₂ = finite-MultiSet_over A iff for f being Multiset of A holds
( f in the carrier of b₂ iff f " (NAT \ {0}) is finite ) );

theorem Th34: :: MONOID_1:34

for A being non empty set
for a being Element of A holds chi a is Element of (finite-MultiSet_over A)

proof end;

theorem Th35: :: MONOID_1:35

for x being set
for A being non empty set
for p being FinSequence of A holds dom ({x} | (p ^ <*x*>)) = (dom ({x} | p)) \/ {((len p) + 1)}

proof end;

theorem Th36: :: MONOID_1:36

for x, y being set
for A being non empty set
for p being FinSequence of A st x <> y holds
dom ({x} | (p ^ <*y*>)) = dom ({x} | p)

proof end;

definition

let A be non empty set ;
let p be FinSequence of A;
func |.p.| -> Multiset of A means :Def7: :: MONOID_1:def 7
for a being Element of A holds it . a = card (dom ({a} | p));
existence
ex b₁ being Multiset of A st
for a being Element of A holds b₁ . a = card (dom ({a} | p))

proof end;

uniqueness
for b₁, b₂ being Multiset of A st ( for a being Element of A holds b₁ . a = card (dom ({a} | p)) ) & ( for a being Element of A holds b₂ . a = card (dom ({a} | p)) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def7 defines |. MONOID_1:def 7 :
for A being non empty set
for p being FinSequence of A
for b₃ being Multiset of A holds
( b₃ = |.p.| iff for a being Element of A holds b₃ . a = card (dom ({a} | p)) );

theorem :: MONOID_1:37

for A being non empty set
for a being Element of A holds |.(<*> A).| . a = 0

proof end;

theorem Th38: :: MONOID_1:38

for A being non empty set holds |.(<*> A).| = A --> 0

proof end;

theorem :: MONOID_1:39

for A being non empty set
for a being Element of A holds |.<*a*>.| = chi a

proof end;

theorem Th40: :: MONOID_1:40

for A being non empty set
for a being Element of A
for p being FinSequence of A holds |.(p ^ <*a*>).| = |.p.| [*] (chi a)

proof end;

theorem Th41: :: MONOID_1:41

for A being non empty set
for p, q being FinSequence of A holds |.(p ^ q).| = |.p.| [*] |.q.|

proof end;

theorem Th42: :: MONOID_1:42

for n being Element of NAT
for A being non empty set
for a being Element of A holds
( |.(n .--> a).| . a = n & ( for b being Element of A st b <> a holds
|.(n .--> a).| . b = 0 ) )

proof end;

theorem :: MONOID_1:43

for A being non empty set
for p being FinSequence of A holds |.p.| is Element of (finite-MultiSet_over A)

proof end;

theorem :: MONOID_1:44

for x being set
for A being non empty set st x is Element of (finite-MultiSet_over A) holds
ex p being FinSequence of A st x = |.p.|

proof end;

begin

definition

let D1, D2, D be non empty set ;
let f be Function of [:D1,D2:],D;
func f .:^2 -> Function of [:(bool D1),(bool D2):],(bool D) means :Def8: :: MONOID_1:def 8
for x being Element of [:(bool D1),(bool D2):] holds it . x = f .: [:(x `1),(x `2):];
existence
ex b₁ being Function of [:(bool D1),(bool D2):],(bool D) st
for x being Element of [:(bool D1),(bool D2):] holds b₁ . x = f .: [:(x `1),(x `2):]

proof end;

uniqueness
for b₁, b₂ being Function of [:(bool D1),(bool D2):],(bool D) st ( for x being Element of [:(bool D1),(bool D2):] holds b₁ . x = f .: [:(x `1),(x `2):] ) & ( for x being Element of [:(bool D1),(bool D2):] holds b₂ . x = f .: [:(x `1),(x `2):] ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def8 defines .:^2 MONOID_1:def 8 :
for D1, D2, D being non empty set
for f being Function of [:D1,D2:],D
for b₅ being Function of [:(bool D1),(bool D2):],(bool D) holds
( b₅ = f .:^2 iff for x being Element of [:(bool D1),(bool D2):] holds b₅ . x = f .: [:(x `1),(x `2):] );

theorem Th45: :: MONOID_1:45

for D1, D2, D being non empty set
for f being Function of [:D1,D2:],D
for X1 being Subset of D1
for X2 being Subset of D2 holds (f .:^2) . (X1,X2) = f .: [:X1,X2:]

proof end;

theorem Th46: :: MONOID_1:46

for D1, D2, D being non empty set
for f being Function of [:D1,D2:],D
for X1 being Subset of D1
for X2 being Subset of D2
for x1, x2 being set st x1 in X1 & x2 in X2 holds
f . (x1,x2) in (f .:^2) . (X1,X2)

proof end;

theorem :: MONOID_1:47

for D1, D2, D being non empty set
for f being Function of [:D1,D2:],D
for X1 being Subset of D1
for X2 being Subset of D2 holds (f .:^2) . (X1,X2) = { (f . (a,b)) where a is Element of D1, b is Element of D2 : ( a in X1 & b in X2 ) }

proof end;

theorem Th48: :: MONOID_1:48

for X, Y being set
for D being non empty set
for o being BinOp of D st o is commutative holds
o .: [:X,Y:] = o .: [:Y,X:]

proof end;

theorem Th49: :: MONOID_1:49

for X, Y, Z being set
for D being non empty set
for o being BinOp of D st o is associative holds
o .: [:(o .: [:X,Y:]),Z:] = o .: [:X,(o .: [:Y,Z:]):]

proof end;

theorem Th50: :: MONOID_1:50

for D being non empty set
for o being BinOp of D st o is commutative holds
o .:^2 is commutative

proof end;

theorem Th51: :: MONOID_1:51

for D being non empty set
for o being BinOp of D st o is associative holds
o .:^2 is associative

proof end;

theorem Th52: :: MONOID_1:52

for X being set
for D being non empty set
for o being BinOp of D
for a being Element of D st a is_a_unity_wrt o holds
( o .: [:{a},X:] = D /\ X & o .: [:X,{a}:] = D /\ X )

proof end;

theorem Th53: :: MONOID_1:53

for D being non empty set
for o being BinOp of D
for a being Element of D st a is_a_unity_wrt o holds
( {a} is_a_unity_wrt o .:^2 & o .:^2 is having_a_unity & the_unity_wrt (o .:^2) = {a} )

proof end;

theorem Th54: :: MONOID_1:54

for D being non empty set
for o being BinOp of D st o is having_a_unity holds
( o .:^2 is having_a_unity & {(the_unity_wrt o)} is_a_unity_wrt o .:^2 & the_unity_wrt (o .:^2) = {(the_unity_wrt o)} )

proof end;

theorem Th55: :: MONOID_1:55

for D being non empty set
for o being BinOp of D st o is uniquely-decomposable holds
o .:^2 is uniquely-decomposable

proof end;

definition

let G be non empty multMagma ;
func bool G -> multMagma equals :Def9: :: MONOID_1:def 9
multLoopStr(# (bool the carrier of G),( the multF of G .:^2),{(the_unity_wrt the multF of G)} #) if G is unital
otherwise multMagma(# (bool the carrier of G),( the multF of G .:^2) #);
correctness
coherence
( ( G is unital implies multLoopStr(# (bool the carrier of G),( the multF of G .:^2),{(the_unity_wrt the multF of G)} #) is multMagma ) & ( not G is unital implies multMagma(# (bool the carrier of G),( the multF of G .:^2) #) is multMagma ) );
consistency
for b₁ being multMagma holds verum;
;

end;

:: deftheorem Def9 defines bool MONOID_1:def 9 :
for G being non empty multMagma holds
( ( G is unital implies bool G = multLoopStr(# (bool the carrier of G),( the multF of G .:^2),{(the_unity_wrt the multF of G)} #) ) & ( not G is unital implies bool G = multMagma(# (bool the carrier of G),( the multF of G .:^2) #) ) );

registration

let G be non empty multMagma ;
cluster bool G -> non empty ;
coherence
not bool G is empty

proof end;

end;

definition

let G be non empty unital multMagma ;
:: original: bool
redefine func bool G -> non empty strict well-unital multLoopStr ;
coherence
bool G is non empty strict well-unital multLoopStr

proof end;

end;

theorem Th56: :: MONOID_1:56

for G being non empty multMagma holds
( the carrier of (bool G) = bool the carrier of G & the multF of (bool G) = the multF of G .:^2 )

proof end;

theorem :: MONOID_1:57

for G being non empty unital multMagma holds 1. (bool G) = {(the_unity_wrt the multF of G)}

proof end;

theorem :: MONOID_1:58

for G being non empty multMagma holds
( ( G is commutative implies bool G is commutative ) & ( G is associative implies bool G is associative ) & ( G is uniquely-decomposable implies bool G is uniquely-decomposable ) )

proof end;