:: MONOID_1 semantic presentation

deffunc H1( HGrStr ) -> M6([:the carrier of a1,the carrier of a1:],the carrier of a1) = the mult of a1;

deffunc H2( multLoopStr ) -> Element of the carrier of a1 = the unity of a1;

definition
let c1, c2, c3 be non empty set ;
mode Function of a1,a2,a3 is Function of [:a1,a2:],a3;
end;

definition
let c1 be Function;
let c2, c3, c4 be set ;
func c1 .. c2,c3,c4 -> set equals :: MONOID_1:def 1
a1 .. [a2,a3],a4;
correctness
coherence
c1 .. [c2,c3],c4 is set ;
;
end;

:: deftheorem Def1 defines .. MONOID_1:def 1 :
for b1 being Function
for b2, b3, b4 being set holds b1 .. b2,b3,b4 = b1 .. [b2,b3],b4;

theorem Th1: :: MONOID_1:1
for b1, b2 being Function
for b3, b4, b5 being set st [b3,b4] in dom b1 & b2 = b1 . b3,b4 & b5 in dom b2 holds
b1 .. b3,b4,b5 = b2 . b5 by FUNCT_6:44;

definition
let c1, c2, c3, c4 be non empty set ;
let c5 be Function of c2,c3, Funcs c1,c4;
let c6 be Element of c2;
let c7 be Element of c3;
let c8 be Element of c1;
redefine func .. as c5 .. c6,c7,c8 -> Element of a4;
coherence
c5 .. c6,c7,c8 is Element of c4
proof end;
end;

definition
let c1 be set ;
let c2, c3, c4 be non empty set ;
let c5 be Function of c2,c3,c4;
let c6 be Function of c1,c2;
let c7 be Function of c1,c3;
redefine func .: as c5 .: c6,c7 -> Element of Funcs a1,a4;
coherence
c5 .: c6,c7 is Element of Funcs c1,c4
proof end;
end;

notation
let c1 be non empty set ;
let c2 be Nat;
let c3 be Element of c1;
synonym c2 .--> c3 for c1 |-> c2;
end;

definition
let c1 be non empty set ;
let c2 be Nat;
let c3 be Element of c1;
redefine func .--> as c2 .--> c3 -> FinSequence of a1;
coherence
c3 .--> is FinSequence of c1 by FINSEQ_2:77;
end;

definition
let c1 be non empty set ;
let c2 be set ;
let c3 be Element of c1;
redefine func --> as c2 --> c3 -> Element of Funcs a2,a1;
coherence
c2 --> c3 is Element of Funcs c2,c1
proof end;
end;

definition
let c1 be set ;
let c2, c3, c4 be non empty set ;
let c5 be Function of c2,c3,c4;
let c6 be Element of c2;
let c7 be Function of c1,c3;
redefine func [;] as c5 [;] c6,c7 -> Element of Funcs a1,a4;
coherence
c5 [;] c6,c7 is Element of Funcs c1,c4
proof end;
end;

definition
let c1 be set ;
let c2, c3, c4 be non empty set ;
let c5 be Function of c2,c3,c4;
let c6 be Function of c1,c2;
let c7 be Element of c3;
redefine func [:] as c5 [:] c6,c7 -> Element of Funcs a1,a4;
coherence
c5 [:] c6,c7 is Element of Funcs c1,c4
proof end;
end;

theorem Th2: :: MONOID_1:2
for b1, b2 being Function
for b3 being set holds (b1 | b3) * b2 = b1 * (b3 | b2)
proof end;

scheme :: MONOID_1:sch 1
s1{ F1() -> set , F2() -> non empty set , P1[ set , set ] } :
ex b1 being Function of F1(),F2() st
for b2 being set st b2 in F1() holds
P1[b2,b1 . b2]
provided
E2: for b1 being set st b1 in F1() holds
ex b2 being Element of F2() st P1[b1,b2]
proof end;

definition
let c1, c2, c3 be non empty set ;
let c4 be Function of c1,c2,c3;
let c5 be set ;
func c4,c3 .: c5 -> Function of (Funcs a5,a1),(Funcs a5,a2), Funcs a5,a3 means :Def2: :: MONOID_1:def 2
for b1 being Element of Funcs a5,a1
for b2 being Element of Funcs a5,a2 holds a6 . b1,b2 = a4 .: b1,b2;
existence
ex b1 being Function of (Funcs c5,c1),(Funcs c5,c2), Funcs c5,c3 st
for b2 being Element of Funcs c5,c1
for b3 being Element of Funcs c5,c2 holds b1 . b2,b3 = c4 .: b2,b3
proof end;
uniqueness
for b1, b2 being Function of (Funcs c5,c1),(Funcs c5,c2), Funcs c5,c3 st ( for b3 being Element of Funcs c5,c1
for b4 being Element of Funcs c5,c2 holds b1 . b3,b4 = c4 .: b3,b4 ) & ( for b3 being Element of Funcs c5,c1
for b4 being Element of Funcs c5,c2 holds b2 . b3,b4 = c4 .: b3,b4 ) holds
b1 = b2
proof end;
end;

:: deftheorem Def2 defines .: MONOID_1:def 2 :
for b1, b2, b3 being non empty set
for b4 being Function of b1,b2,b3
for b5 being set
for b6 being Function of (Funcs b5,b1),(Funcs b5,b2), Funcs b5,b3 holds
( b6 = b4,b3 .: b5 iff for b7 being Element of Funcs b5,b1
for b8 being Element of Funcs b5,b2 holds b6 . b7,b8 = b4 .: b7,b8 );

theorem Th3: :: MONOID_1:3
for b1, b2, b3 being non empty set
for b4 being Function of b1,b2,b3
for b5 being set
for b6 being Function of b5,b1
for b7 being Function of b5,b2
for b8 being set st b8 in b5 holds
(b4,b3 .: b5) .. b6,b7,b8 = b4 . (b6 . b8),(b7 . b8)
proof end;

theorem Th4: :: MONOID_1:4
for b1 being set
for b2 being non empty set
for b3 being BinOp of b2
for b4, b5 being Function of b1,b2 st b3 is commutative holds
b3 .: b4,b5 = b3 .: b5,b4
proof end;

theorem Th5: :: MONOID_1:5
for b1 being set
for b2 being non empty set
for b3 being BinOp of b2
for b4, b5, b6 being Function of b1,b2 st b3 is associative holds
b3 .: (b3 .: b4,b5),b6 = b3 .: b4,(b3 .: b5,b6)
proof end;

theorem Th6: :: MONOID_1:6
for b1 being set
for b2 being non empty set
for b3 being Element of b2
for b4 being BinOp of b2
for b5 being Function of b1,b2 st b3 is_a_unity_wrt b4 holds
( b4 [;] b3,b5 = b5 & b4 [:] b5,b3 = b5 )
proof end;

theorem Th7: :: MONOID_1:7
for b1 being set
for b2 being non empty set
for b3 being BinOp of b2
for b4 being Function of b1,b2 st b3 is idempotent holds
b3 .: b4,b4 = b4
proof end;

theorem Th8: :: MONOID_1:8
for b1 being set
for b2 being non empty set
for b3 being BinOp of b2 st b3 is commutative holds
b3,b2 .: b1 is commutative
proof end;

theorem Th9: :: MONOID_1:9
for b1 being set
for b2 being non empty set
for b3 being BinOp of b2 st b3 is associative holds
b3,b2 .: b1 is associative
proof end;

theorem Th10: :: MONOID_1:10
for b1 being set
for b2 being non empty set
for b3 being Element of b2
for b4 being BinOp of b2 st b3 is_a_unity_wrt b4 holds
b1 --> b3 is_a_unity_wrt b4,b2 .: b1
proof end;

theorem Th11: :: MONOID_1:11
for b1 being set
for b2 being non empty set
for b3 being BinOp of b2 st b3 has_a_unity holds
( the_unity_wrt (b3,b2 .: b1) = b1 --> (the_unity_wrt b3) & b3,b2 .: b1 has_a_unity )
proof end;

theorem Th12: :: MONOID_1:12
for b1 being set
for b2 being non empty set
for b3 being BinOp of b2 st b3 is idempotent holds
b3,b2 .: b1 is idempotent
proof end;

theorem Th13: :: MONOID_1:13
for b1 being set
for b2 being non empty set
for b3 being BinOp of b2 st b3 is invertible holds
b3,b2 .: b1 is invertible
proof end;

theorem Th14: :: MONOID_1:14
for b1 being set
for b2 being non empty set
for b3 being BinOp of b2 st b3 is cancelable holds
b3,b2 .: b1 is cancelable
proof end;

theorem Th15: :: MONOID_1:15
for b1 being set
for b2 being non empty set
for b3 being BinOp of b2 st b3 is uniquely-decomposable holds
b3,b2 .: b1 is uniquely-decomposable
proof end;

theorem Th16: :: MONOID_1:16
for b1 being set
for b2 being non empty set
for b3, b4 being BinOp of b2 st b3 absorbs b4 holds
b3,b2 .: b1 absorbs b4,b2 .: b1
proof end;

theorem Th17: :: MONOID_1:17
for b1 being set
for b2, b3, b4, b5, b6, b7 being non empty set
for b8 being Function of b2,b3,b4
for b9 being Function of b5,b6,b7 st b8 <= b9 holds
b8,b4 .: b1 <= b9,b7 .: b1
proof end;

definition
let c1 be non empty HGrStr ;
let c2 be set ;
func .: c1,c2 -> HGrStr equals :Def3: :: MONOID_1:def 3
 multLoopStr(# (Funcs a2,the carrier of a1),(the mult of a1,the carrier of a1 .: a2),(a2 --> (the_unity_wrt the mult of a1)) #) if a1 is unital
otherwise HGrStr(# (Funcs a2,the carrier of a1),(the mult of a1,the carrier of a1 .: a2) #);
correctness
coherence
( ( c1 is unital implies multLoopStr(# (Funcs c2,the carrier of c1),(the mult of c1,the carrier of c1 .: c2),(c2 --> (the_unity_wrt the mult of c1)) #) is HGrStr ) & ( not c1 is unital implies HGrStr(# (Funcs c2,the carrier of c1),(the mult of c1,the carrier of c1 .: c2) #) is HGrStr ) );
consistency
for b1 being HGrStr holds verum;
;
end;

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

registration
let c1 be non empty HGrStr ;
let c2 be set ;
cluster .: a1,a2 -> non empty ;
coherence
not .: c1,c2 is empty
proof end;
end;

deffunc H3( non empty HGrStr ) -> set = the carrier of a1;

theorem Th18: :: MONOID_1:18
for b1 being set
for b2 being non empty HGrStr holds
( the carrier of (.: b2,b1) = Funcs b1,the carrier of b2 & the mult of (.: b2,b1) = the mult of b2,the carrier of b2 .: b1 )
proof end;

theorem Th19: :: MONOID_1:19
for b1, b2 being set
for b3 being non empty HGrStr holds
( b1 is Element of (.: b3,b2) iff b1 is Function of b2,the carrier of b3 )
proof end;

Lemma18: for b1 being set
for b2 being non empty HGrStr holds .: b2,b1 is constituted-Functions
proof end;

registration
let c1 be non empty HGrStr ;
let c2 be set ;
cluster .: a1,a2 -> non empty constituted-Functions ;
coherence
.: c1,c2 is constituted-Functions by Lemma18;
end;

theorem Th20: :: MONOID_1:20
for b1 being set
for b2 being non empty HGrStr
for b3 being Element of (.: b2,b1) holds
( dom b3 = b1 & rng b3 c= the carrier of b2 )
proof end;

theorem Th21: :: MONOID_1:21
for b1 being set
for b2 being non empty HGrStr
for b3, b4 being Element of (.: b2,b1) st ( for b5 being set st b5 in b1 holds
b3 . b5 = b4 . b5 ) holds
b3 = b4
proof end;

definition
let c1 be non empty HGrStr ;
let c2 be non empty set ;
let c3 be Element of (.: c1,c2);
let c4 be Element of c2;
redefine func . as c3 . c4 -> Element of a1;
coherence
c3 . c4 is Element of c1
proof end;
end;

registration
let c1 be non empty HGrStr ;
let c2 be non empty set ;
let c3 be Element of (.: c1,c2);
cluster rng a3 -> non empty ;
coherence
not rng c3 is empty
proof end;
end;

theorem Th22: :: MONOID_1:22
for b1 being non empty set
for b2 being non empty HGrStr
for b3, b4 being Element of (.: b2,b1)
for b5 being Element of b1 holds (b3 * b4) . b5 = (b3 . b5) * (b4 . b5)
proof end;

definition
let c1 be non empty unital HGrStr ;
let c2 be set ;
redefine func .: as .: c1,c2 -> non empty strict well-unital constituted-Functions multLoopStr ;
coherence
.: c1,c2 is non empty strict well-unital constituted-Functions multLoopStr
proof end;
end;

theorem Th23: :: MONOID_1:23
for b1 being set
for b2 being non empty unital HGrStr holds the unity of (.: b2,b1) = b1 --> (the_unity_wrt the mult of b2)
proof end;

theorem Th24: :: MONOID_1:24
for b1 being non empty HGrStr
for b2 being set holds
( ( b1 is commutative implies .: b1,b2 is commutative ) & ( b1 is associative implies .: b1,b2 is associative ) & ( b1 is idempotent implies .: b1,b2 is idempotent ) & ( b1 is invertible implies .: b1,b2 is invertible ) & ( b1 is cancelable implies .: b1,b2 is cancelable ) & ( b1 is uniquely-decomposable implies .: b1,b2 is uniquely-decomposable ) )
proof end;

theorem Th25: :: MONOID_1:25
for b1 being set
for b2 being non empty HGrStr
for b3 being non empty SubStr of b2 holds .: b3,b1 is SubStr of .: b2,b1
proof end;

theorem Th26: :: MONOID_1:26
for b1 being set
for b2 being non empty unital HGrStr
for b3 being non empty SubStr of b2 st the_unity_wrt the mult of b2 in the carrier of b3 holds
.: b3,b1 is MonoidalSubStr of .: b2,b1
proof end;

definition
let c1 be non empty unital associative commutative cancelable uniquely-decomposable HGrStr ;
let c2 be set ;
redefine func .: as .: c1,c2 -> commutative strict constituted-Functions cancelable uniquely-decomposable Monoid;
coherence
.: c1,c2 is commutative strict constituted-Functions cancelable uniquely-decomposable Monoid
proof end;
end;

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

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

theorem Th27: :: MONOID_1:27
for b1 being set holds
( the carrier of (MultiSet_over b1) = Funcs b1,NAT & the mult of (MultiSet_over b1) = addnat ,NAT .: b1 & the unity of (MultiSet_over b1) = b1 --> 0 )
proof end;

definition
let c1 be set ;
mode Multiset of a1 is Element of (MultiSet_over a1);
end;

theorem Th28: :: MONOID_1:28
for b1, b2 being set holds
( b1 is Multiset of b2 iff b1 is Function of b2, NAT )
proof end;

theorem Th29: :: MONOID_1:29
for b1 being set
for b2 being Multiset of b1 holds
( dom b2 = b1 & rng b2 c= NAT )
proof end;

definition
let c1 be non empty set ;
let c2 be Multiset of c1;
redefine func rng as rng c2 -> non empty Subset of NAT ;
coherence
rng c2 is non empty Subset of NAT
proof end;
let c3 be Element of c1;
redefine func . as c2 . c3 -> Nat;
coherence
c2 . c3 is Nat
proof end;
end;

theorem Th30: :: MONOID_1:30
for b1 being non empty set
for b2, b3 being Multiset of b1
for b4 being Element of b1 holds (b2 [*] b3) . b4 = (b2 . b4) + (b3 . b4)
proof end;

theorem Th31: :: MONOID_1:31
for b1, b2 being set holds chi b1,b2 is Multiset of b2
proof end;

definition
let c1, c2 be set ;
redefine func chi as chi c1,c2 -> Multiset of a2;
coherence
chi c1,c2 is Multiset of c2 by Th31;
end;

definition
let c1 be set ;
let c2 be Nat;
redefine func --> as c1 --> c2 -> Multiset of a1;
coherence
c1 --> c2 is Multiset of c1
proof end;
end;

definition
let c1 be non empty set ;
let c2 be Element of c1;
func chi c2 -> Multiset of a1 equals :: MONOID_1:def 5
 chi {a2},a1;
coherence
chi {c2},c1 is Multiset of c1 ;
end;

:: deftheorem Def5 defines chi MONOID_1:def 5 :
for b1 being non empty set
for b2 being Element of b1 holds chi b2 = chi {b2},b1;

theorem Th32: :: MONOID_1:32
for b1 being non empty set
for b2, b3 being Element of b1 holds
( (chi b2) . b2 = 1 & ( b3 <> b2 implies (chi b2) . b3 = 0 ) )
proof end;

theorem Th33: :: MONOID_1:33
for b1 being non empty set
for b2, b3 being Multiset of b1 st ( for b4 being Element of b1 holds b2 . b4 = b3 . b4 ) holds
b2 = b3
proof end;

definition
let c1 be set ;
func finite-MultiSet_over c1 -> non empty strict MonoidalSubStr of MultiSet_over a1 means :Def6: :: MONOID_1:def 6
for b1 being Multiset of a1 holds
( b1 in the carrier of a2 iff b1 " (NAT \ {0}) is finite );
existence
ex b1 being non empty strict MonoidalSubStr of MultiSet_over c1 st
for b2 being Multiset of c1 holds
( b2 in the carrier of b1 iff b2 " (NAT \ {0}) is finite )
proof end;
uniqueness
for b1, b2 being non empty strict MonoidalSubStr of MultiSet_over c1 st ( for b3 being Multiset of c1 holds
( b3 in the carrier of b1 iff b3 " (NAT \ {0}) is finite ) ) & ( for b3 being Multiset of c1 holds
( b3 in the carrier of b2 iff b3 " (NAT \ {0}) is finite ) ) holds
b1 = b2
proof end;
end;

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

theorem Th34: :: MONOID_1:34
for b1 being non empty set
for b2 being Element of b1 holds chi b2 is Element of (finite-MultiSet_over b1)
proof end;

theorem Th35: :: MONOID_1:35
for b1 being set
for b2 being non empty set
for b3 being FinSequence of b2 holds dom ({b1} | (b3 ^ <*b1*>)) = (dom ({b1} | b3)) \/ {((len b3) + 1)}
proof end;

theorem Th36: :: MONOID_1:36
for b1, b2 being set
for b3 being non empty set
for b4 being FinSequence of b3 st b1 <> b2 holds
dom ({b1} | (b4 ^ <*b2*>)) = dom ({b1} | b4)
proof end;

registration
let c1 be set ;
let c2 be finite Relation;
cluster a1 | a2 -> finite ;
coherence
c1 | c2 is finite
proof end;
end;

definition
let c1 be non empty set ;
let c2 be FinSequence of c1;
func |.c2.| -> Multiset of a1 means :Def7: :: MONOID_1:def 7
for b1 being Element of a1 holds a3 . b1 = card (dom ({b1} | a2));
existence
ex b1 being Multiset of c1 st
for b2 being Element of c1 holds b1 . b2 = card (dom ({b2} | c2))
proof end;
uniqueness
for b1, b2 being Multiset of c1 st ( for b3 being Element of c1 holds b1 . b3 = card (dom ({b3} | c2)) ) & ( for b3 being Element of c1 holds b2 . b3 = card (dom ({b3} | c2)) ) holds
b1 = b2
proof end;
end;

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

theorem Th37: :: MONOID_1:37
for b1 being non empty set
for b2 being Element of b1 holds |.(<*> b1).| . b2 = 0
proof end;

theorem Th38: :: MONOID_1:38
for b1 being non empty set holds |.(<*> b1).| = b1 --> 0
proof end;

theorem Th39: :: MONOID_1:39
for b1 being non empty set
for b2 being Element of b1 holds |.<*b2*>.| = chi b2
proof end;

theorem Th40: :: MONOID_1:40
for b1 being non empty set
for b2 being Element of b1
for b3 being FinSequence of b1 holds |.(b3 ^ <*b2*>).| = |.b3.| [*] (chi b2)
proof end;

theorem Th41: :: MONOID_1:41
for b1 being non empty set
for b2, b3 being FinSequence of b1 holds |.(b2 ^ b3).| = |.b2.| [*] |.b3.|
proof end;

theorem Th42: :: MONOID_1:42
for b1 being Nat
for b2 being non empty set
for b3 being Element of b2 holds
( |.(b1 .--> b3).| . b3 = b1 & ( for b4 being Element of b2 st b4 <> b3 holds
|.(b1 .--> b3).| . b4 = 0 ) )
proof end;

theorem Th43: :: MONOID_1:43
for b1 being non empty set
for b2 being FinSequence of b1 holds |.b2.| is Element of (finite-MultiSet_over b1)
proof end;

theorem Th44: :: MONOID_1:44
for b1 being set
for b2 being non empty set st b1 is Element of (finite-MultiSet_over b2) holds
ex b3 being FinSequence of b2 st b1 = |.b3.|
proof end;

definition
let c1, c2, c3 be non empty set ;
let c4 be Function of c1,c2,c3;
func c4 .:^2 -> Function of (bool a1),(bool a2), bool a3 means :Def8: :: MONOID_1:def 8
for b1 being Element of [:(bool a1),(bool a2):] holds a5 . b1 = a4 .: [:(b1 `1 ),(b1 `2 ):];
existence
ex b1 being Function of (bool c1),(bool c2), bool c3 st
for b2 being Element of [:(bool c1),(bool c2):] holds b1 . b2 = c4 .: [:(b2 `1 ),(b2 `2 ):]
proof end;
uniqueness
for b1, b2 being Function of (bool c1),(bool c2), bool c3 st ( for b3 being Element of [:(bool c1),(bool c2):] holds b1 . b3 = c4 .: [:(b3 `1 ),(b3 `2 ):] ) & ( for b3 being Element of [:(bool c1),(bool c2):] holds b2 . b3 = c4 .: [:(b3 `1 ),(b3 `2 ):] ) holds
b1 = b2
proof end;
end;

:: deftheorem Def8 defines .:^2 MONOID_1:def 8 :
for b1, b2, b3 being non empty set
for b4 being Function of b1,b2,b3
for b5 being Function of (bool b1),(bool b2), bool b3 holds
( b5 = b4 .:^2 iff for b6 being Element of [:(bool b1),(bool b2):] holds b5 . b6 = b4 .: [:(b6 `1 ),(b6 `2 ):] );

theorem Th45: :: MONOID_1:45
for b1, b2, b3 being non empty set
for b4 being Function of b1,b2,b3
for b5 being Subset of b1
for b6 being Subset of b2 holds (b4 .:^2 ) . b5,b6 = b4 .: [:b5,b6:]
proof end;

theorem Th46: :: MONOID_1:46
for b1, b2, b3 being non empty set
for b4 being Function of b1,b2,b3
for b5 being Subset of b1
for b6 being Subset of b2
for b7, b8 being set st b7 in b5 & b8 in b6 holds
b4 . b7,b8 in (b4 .:^2 ) . b5,b6
proof end;

theorem Th47: :: MONOID_1:47
for b1, b2, b3 being non empty set
for b4 being Function of b1,b2,b3
for b5 being Subset of b1
for b6 being Subset of b2 holds (b4 .:^2 ) . b5,b6 = { (b4 . b7,b8) where B is Element of b1, B is Element of b2 : ( b7 in b5 & b8 in b6 ) }
proof end;

theorem Th48: :: MONOID_1:48
for b1, b2 being set
for b3 being non empty set
for b4 being BinOp of b3 st b4 is commutative holds
b4 .: [:b1,b2:] = b4 .: [:b2,b1:]
proof end;

theorem Th49: :: MONOID_1:49
for b1, b2, b3 being set
for b4 being non empty set
for b5 being BinOp of b4 st b5 is associative holds
b5 .: [:(b5 .: [:b1,b2:]),b3:] = b5 .: [:b1,(b5 .: [:b2,b3:]):]
proof end;

theorem Th50: :: MONOID_1:50
for b1 being non empty set
for b2 being BinOp of b1 st b2 is commutative holds
b2 .:^2 is commutative
proof end;

theorem Th51: :: MONOID_1:51
for b1 being non empty set
for b2 being BinOp of b1 st b2 is associative holds
b2 .:^2 is associative
proof end;

theorem Th52: :: MONOID_1:52
for b1 being set
for b2 being non empty set
for b3 being BinOp of b2
for b4 being Element of b2 st b4 is_a_unity_wrt b3 holds
( b3 .: [:{b4},b1:] = b2 /\ b1 & b3 .: [:b1,{b4}:] = b2 /\ b1 )
proof end;

theorem Th53: :: MONOID_1:53
for b1 being non empty set
for b2 being BinOp of b1
for b3 being Element of b1 st b3 is_a_unity_wrt b2 holds
( {b3} is_a_unity_wrt b2 .:^2 & b2 .:^2 has_a_unity & the_unity_wrt (b2 .:^2 ) = {b3} )
proof end;

theorem Th54: :: MONOID_1:54
for b1 being non empty set
for b2 being BinOp of b1 st b2 has_a_unity holds
( b2 .:^2 has_a_unity & {(the_unity_wrt b2)} is_a_unity_wrt b2 .:^2 & the_unity_wrt (b2 .:^2 ) = {(the_unity_wrt b2)} )
proof end;

theorem Th55: :: MONOID_1:55
for b1 being non empty set
for b2 being BinOp of b1 st b2 is uniquely-decomposable holds
b2 .:^2 is uniquely-decomposable
proof end;

definition
let c1 be non empty HGrStr ;
func bool c1 -> HGrStr equals :Def9: :: MONOID_1:def 9
 multLoopStr(# (bool the carrier of a1),(the mult of a1 .:^2 ),{(the_unity_wrt the mult of a1)} #) if a1 is unital
otherwise HGrStr(# (bool the carrier of a1),(the mult of a1 .:^2 ) #);
correctness
coherence
( ( c1 is unital implies multLoopStr(# (bool the carrier of c1),(the mult of c1 .:^2 ),{(the_unity_wrt the mult of c1)} #) is HGrStr ) & ( not c1 is unital implies HGrStr(# (bool the carrier of c1),(the mult of c1 .:^2 ) #) is HGrStr ) );
consistency
for b1 being HGrStr holds verum;
;
end;

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

registration
let c1 be non empty HGrStr ;
cluster bool a1 -> non empty ;
coherence
not bool c1 is empty
proof end;
end;

definition
let c1 be non empty unital HGrStr ;
redefine func bool as bool c1 -> non empty strict well-unital multLoopStr ;
coherence
bool c1 is non empty strict well-unital multLoopStr
proof end;
end;

theorem Th56: :: MONOID_1:56
for b1 being non empty HGrStr holds
( the carrier of (bool b1) = bool the carrier of b1 & the mult of (bool b1) = the mult of b1 .:^2 )
proof end;

theorem Th57: :: MONOID_1:57
for b1 being non empty unital HGrStr holds the unity of (bool b1) = {(the_unity_wrt the mult of b1)}
proof end;

theorem Th58: :: MONOID_1:58
for b1 being non empty HGrStr holds
( ( b1 is commutative implies bool b1 is commutative ) & ( b1 is associative implies bool b1 is associative ) & ( b1 is uniquely-decomposable implies bool b1 is uniquely-decomposable ) )
proof end;