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


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

deffunc H2( 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:63;
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
for f, g being Function
for X being set holds (f | X) * g = f * (X |` g)
proof end;

scheme :: MONOID_1:sch 1
NonUniqFuncDEx{ F1() -> set , F2() -> non empty set , P1[ object , object ] } :
ex f being Function of F1(),F2() st
for x being object st x in F1() holds
P1[x,f . x]
provided
A1: for x being object st x in F1() holds
ex y being Element of F2() st P1[x,y]
proof end;

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 b1 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 b1 . (f1,f2) = f .: (f1,f2)
proof end;
uniqueness
for b1, b2 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 b1 . (f1,f2) = f .: (f1,f2) ) & ( for f1 being Element of Funcs (A,D1)
for f2 being Element of Funcs (A,D2) holds b2 . (f1,f2) = f .: (f1,f2) ) holds
b1 = b2
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 b6 being Function of [:(Funcs (A,D1)),(Funcs (A,D2)):],(Funcs (A,D)) holds
( b6 = (f,D) .: A iff for f1 being Element of Funcs (A,D1)
for f2 being Element of Funcs (A,D2) holds b6 . (f1,f2) = f .: (f1,f2) );

theorem :: MONOID_1:2
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 Th3: :: MONOID_1:3
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 Th4: :: MONOID_1:4
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 Th5: :: MONOID_1:5
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 Th6: :: MONOID_1:6
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 Th7: :: MONOID_1:7
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 Th8: :: MONOID_1:8
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 Th9: :: MONOID_1:9
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 Th10: :: MONOID_1:10
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 Th11: :: MONOID_1:11
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 Th12: :: MONOID_1:12
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 Th13: :: MONOID_1:13
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 Th14: :: MONOID_1:14
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:15
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 Th16: :: MONOID_1:16
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 b1 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 H3( non empty multMagma ) -> set = the carrier of $1;

theorem Th17: :: MONOID_1:17
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:18
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 Th19: :: MONOID_1:19
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 Th20: :: MONOID_1:20
for X being set
for G being non empty multMagma
for f, g being Element of (.: (G,X)) st ( for x being object 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 rng f -> non empty ;
coherence
not rng f is empty
proof end;
end;

theorem Th21: :: MONOID_1:21
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 Th22: :: MONOID_1:22
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 Th23: :: MONOID_1:23
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:24
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:25
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;

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 Th26: :: MONOID_1:26
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 Th27: :: MONOID_1:27
for x, X being set holds
( x is Multiset of X iff x is Function of X,NAT )
proof end;

theorem Th28: :: MONOID_1:28
for X being set
for m being Multiset of X holds
( dom m = X & rng m c= NAT )
proof end;

registration
let X be set ;
cluster -> NAT -valued for Element of the carrier of (MultiSet_over X);
coherence
for b1 being Multiset of X holds b1 is NAT -valued by Th28;
end;

theorem Th29: :: MONOID_1:29
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 Th30: :: MONOID_1:30
for X, Y 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 Th30;
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 Th31: :: MONOID_1:31
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 Th32: :: MONOID_1:32
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 b1 being non empty strict MonoidalSubStr of MultiSet_over A st
for f being Multiset of A holds
( f in the carrier of b1 iff f " (NAT \ {0}) is finite )
proof end;
uniqueness
for b1, b2 being non empty strict MonoidalSubStr of MultiSet_over A st ( for f being Multiset of A holds
( f in the carrier of b1 iff f " (NAT \ {0}) is finite ) ) & ( for f being Multiset of A holds
( f in the carrier of b2 iff f " (NAT \ {0}) is finite ) ) holds
b1 = b2
proof end;
end;

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

theorem Th33: :: MONOID_1:33
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 Th34: :: MONOID_1:34
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 Th35: :: MONOID_1:35
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 b1 being Multiset of A st
for a being Element of A holds b1 . a = card (dom ({a} |` p))
proof end;
uniqueness
for b1, b2 being Multiset of A st ( for a being Element of A holds b1 . a = card (dom ({a} |` p)) ) & ( for a being Element of A holds b2 . a = card (dom ({a} |` p)) ) holds
b1 = b2
proof end;
end;

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

theorem :: MONOID_1:36
for A being non empty set
for a being Element of A holds |.(<*> A).| . a = 0
proof end;

theorem Th37: :: MONOID_1:37
for A being non empty set holds |.(<*> A).| = A --> 0
proof end;

theorem :: MONOID_1:38
for A being non empty set
for a being Element of A holds |.<*a*>.| = chi a
proof end;

theorem Th39: :: MONOID_1:39
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 Th40: :: MONOID_1:40
for A being non empty set
for p, q being FinSequence of A holds |.(p ^ q).| = |.p.| [*] |.q.|
proof end;

theorem Th41: :: MONOID_1:41
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:42
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:43
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;

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 b1 being Function of [:(bool D1),(bool D2):],(bool D) st
for x being Element of [:(bool D1),(bool D2):] holds b1 . x = f .: [:(x `1),(x `2):]
proof end;
uniqueness
for b1, b2 being Function of [:(bool D1),(bool D2):],(bool D) st ( for x being Element of [:(bool D1),(bool D2):] holds b1 . x = f .: [:(x `1),(x `2):] ) & ( for x being Element of [:(bool D1),(bool D2):] holds b2 . x = f .: [:(x `1),(x `2):] ) holds
b1 = b2
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 b5 being Function of [:(bool D1),(bool D2):],(bool D) holds
( b5 = f .:^2 iff for x being Element of [:(bool D1),(bool D2):] holds b5 . x = f .: [:(x `1),(x `2):] );

theorem Th44: :: MONOID_1:44
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 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
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: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 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 Th47: :: MONOID_1:47
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 Th48: :: MONOID_1:48
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 Th49: :: MONOID_1:49
for D being non empty set
for o being BinOp of D st o is commutative holds
o .:^2 is commutative
proof end;

theorem Th50: :: MONOID_1:50
for D being non empty set
for o being BinOp of D st o is associative holds
o .:^2 is associative
proof end;

theorem Th51: :: MONOID_1:51
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 Th52: :: MONOID_1:52
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 Th53: :: MONOID_1:53
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 Th54: :: MONOID_1:54
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 b1 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 Th55: :: MONOID_1:55
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:56
for G being non empty unital multMagma holds 1. (bool G) = {(the_unity_wrt the multF of G)}
proof end;

theorem :: MONOID_1:57
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;