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


begin

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 ;
funcf .. (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 funcf .. (x1,x2,x) ->  Element of D;
coherence
 f .. (x1,x2,x) is Element of D
proofend;
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 funcf .: (g1,g2) ->  Element of Funcs (A,D);
coherence
 f .: (g1,g2) is Element of Funcs (A,D)
proofend;
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 funcn .--> 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 funcA --> d ->  Element of Funcs (A,D);
coherence
 A --> d is Element of Funcs (A,D)
proofend;
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 funcf [;] (d,g) ->  Element of Funcs (A,D);
coherence
 f [;] (d,g) is Element of Funcs (A,D)
proofend;
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 funcf [:] (g,d) ->  Element of Funcs (A,D);
coherence
 f [:] (g,d) is Element of Funcs (A,D)
proofend;
end;

theorem :: MONOID_1:1
for f, g being Function
for X being set holds (f | X) * g = f * (X |` g)
proofend;

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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 set st x in X holds
f . x = g . x ) holds
f = g
proofend;

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 funcf . a ->  Element of G;
coherence
 f . a is Element of G
proofend;
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
proofend;
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)
proofend;

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

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

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

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

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
proofend;
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 Th26: :: MONOID_1:26
for X being set holds
( the carrier of (MultiSet_over X) = Funcs (X,NAT) &amp; the multF of (MultiSet_over X) = (addnat,NAT) .: X &amp; 1. (MultiSet_over X) = X --> 0 )
proofend;

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

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

definition
let A be non empty set ;
let m be Multiset of A;
:: original:rng
redefine func rng m ->  Subset of NAT;
coherence
 rng m is Subset of NAT by Th19, MONOID_0:46;
let a be Element of A;
:: original:.
redefine funcm . a ->  Element of NAT ;
coherence
 m . a is Element of NAT
proofend;
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)
proofend;

theorem Th30: :: MONOID_1:30
for Y, X being set holds chi (Y,X) is Multiset of X
proofend;

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 funcX --> n ->  Multiset of X;
coherence
 X --> n is Multiset of X
proofend;
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 &amp; ( b <> a implies (chi a) . b = 0 ) )
proofend;

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

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 )
proofend;
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 ) ) &amp; ( for f being Multiset of A holds
( f in the carrier of b2 iff f " (NAT \ {0}) is finite ) ) holds
b1 = b2
proofend;
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)
proofend;

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

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

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))
proofend;
uniqueness
 for b1, b2 being Multiset of A st ( for a being Element of A holds b1 . a = card (dom ({a} |` p)) ) &amp; ( for a being Element of A holds b2 . a = card (dom ({a} |` p)) ) holds
b1 = b2
proofend;
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
proofend;

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

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

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

theorem Th40: :: MONOID_1:40
for A being non empty set
for p, q being FinSequence of A holds |.(p ^ q).| = |.p.| [*] |.q.|
proofend;

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 &amp; ( for b being Element of A st b <> a holds
|.(n .--> a).| . b = 0 ) )
proofend;

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

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

begin

definition
let D1, D2, D be non empty set ;
let f be Function of [:D1,D2:],D;
funcf .:^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):]
proofend;
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):] ) &amp; ( for x being Element of [:(bool D1),(bool D2):] holds b2 . x = f .: [:(x `1),(x `2):] ) holds
b1 = b2
proofend;
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:]
proofend;

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 &amp; x2 in X2 holds
f . (x1,x2) in (f .:^2) . (X1,X2)
proofend;

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 &amp; b in X2 )  }
proofend;

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:]
proofend;

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

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

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

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 &amp; o .: [:X,{a}:] = D /\ X )
proofend;

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 &amp; o .:^2 is having_a_unity &amp; the_unity_wrt (o .:^2) = {a} )
proofend;

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 &amp; {(the_unity_wrt o)} is_a_unity_wrt o .:^2 &amp; the_unity_wrt (o .:^2) = {(the_unity_wrt o)} )
proofend;

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

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 ) &amp; ( 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)} #) ) &amp; ( 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
proofend;
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
proofend;
end;

theorem Th55: :: MONOID_1:55
for G being non empty multMagma holds
( the carrier of (bool G) = bool the carrier of G &amp; the multF of (bool G) = the multF of G .:^2 )
proofend;

theorem :: MONOID_1:56
for G being non empty unital multMagma holds 1. (bool G) = {(the_unity_wrt the multF of G)}
proofend;

theorem :: MONOID_1:57
for G being non empty multMagma holds
( ( G is commutative implies bool G is commutative ) &amp; ( G is associative implies bool G is associative ) &amp; ( G is uniquely-decomposable implies bool G is uniquely-decomposable ) )
proofend;