:: Monoid of Multisets and Subsets
:: by Grzegorz Bancerek
::
:: Received December 29, 1992
:: Copyright (c) 1992 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 D1, D2, D be non empty set ;
mode Function of D1,D2,D is Function of [:D1,D2:],D;

end;

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, o' being BinOp of D st o absorbs o' holds
o,D .: A absorbs o',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;