:: MONOID_1 semantic presentation

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
proof
reconsider g = f . (x1,x2) as Element of Funcs (A,D) ;
A1: [x1,x2] in [:D1,D2:] ;
 ( dom f = [:D1,D2:] & dom g = A ) by FUNCT_2:def_1;
then  f .. (x1,x2,x) = g . x by A1, FUNCT_5:38;
hence  f .. (x1,x2,x) is Element of D ; ::_thesis: verum
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 funcf .: (g1,g2) ->  Element of Funcs (A,D);
coherence
 f .: (g1,g2) is Element of Funcs (A,D)
proof
 f .: (g1,g2) = f * <:g1,g2:> by FUNCOP_1:def_3;
then  ( dom (f .: (g1,g2)) = A & rng (f .: (g1,g2)) c= D ) by FUNCT_2:def_1, RELAT_1:def_19;
hence  f .: (g1,g2) is Element of Funcs (A,D) by FUNCT_2:def_2; ::_thesis: verum
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 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)
proof
 ( dom (A --> d) = A & rng (A --> d) c= {d} ) by FUNCOP_1:13;
hence  A --> d is Element of Funcs (A,D) by FUNCT_2:def_2; ::_thesis: verum
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 funcf [;] (d,g) ->  Element of Funcs (A,D);
coherence
 f [;] (d,g) is Element of Funcs (A,D)
proof
 dom g = A by FUNCT_2:def_1;
then  f [;] (d,g) = f * <:(A --> d),g:> by FUNCOP_1:def_5;
then  ( dom (f [;] (d,g)) = A & rng (f [;] (d,g)) c= D ) by FUNCT_2:def_1, RELAT_1:def_19;
hence  f [;] (d,g) is Element of Funcs (A,D) by FUNCT_2:def_2; ::_thesis: verum
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 funcf [:] (g,d) ->  Element of Funcs (A,D);
coherence
 f [:] (g,d) is Element of Funcs (A,D)
proof
 dom g = A by FUNCT_2:def_1;
then  f [:] (g,d) = f * <:g,(A --> d):> by FUNCOP_1:def_4;
then  ( dom (f [:] (g,d)) = A & rng (f [:] (g,d)) c= D ) by FUNCT_2:def_1, RELAT_1:def_19;
hence  f [:] (g,d) is Element of Funcs (A,D) by FUNCT_2:def_2; ::_thesis: verum
end;
end;

theorem :: MONOID_1:1
for f, g being Function
for X being set holds (f | X) * g = f * (X |` g)
proof
let f, g be Function; ::_thesis: for X being set holds (f | X) * g = f * (X |` g)
let X be set ; ::_thesis: (f | X) * g = f * (X |` g)
A1: dom (f | X) = (dom f) /\ X by RELAT_1:61;
A2: dom ((f | X) * g) = dom (f * (X |` g))
proof
thus  dom ((f | X) * g) c= dom (f * (X |` g)) :: according to XBOOLE_0:def_10 ::_thesis: dom (f * (X |` g)) c= dom ((f | X) * g)
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in dom ((f | X) * g) or x in dom (f * (X |` g)) )
assume A3: x in dom ((f | X) * g) ; ::_thesis: x in dom (f * (X |` g))
then A4: x in dom g by FUNCT_1:11;
A5: g . x in dom (f | X) by A3, FUNCT_1:11;
then A6: g . x in dom f by A1, XBOOLE_0:def_4;
 g . x in X by A1, A5, XBOOLE_0:def_4;
then A7: x in dom (X |` g) by A4, FUNCT_1:53;
then  g . x = (X |` g) . x by FUNCT_1:53;
hence  x in dom (f * (X |` g)) by A6, A7, FUNCT_1:11; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in dom (f * (X |` g)) or x in dom ((f | X) * g) )
assume A8: x in dom (f * (X |` g)) ; ::_thesis: x in dom ((f | X) * g)
then A9: x in dom (X |` g) by FUNCT_1:11;
then A10: x in dom g by FUNCT_1:53;
 (X |` g) . x in dom f by A8, FUNCT_1:11;
then A11: g . x in dom f by A9, FUNCT_1:53;
 g . x in X by A9, FUNCT_1:53;
then  g . x in dom (f | X) by A1, A11, XBOOLE_0:def_4;
hence  x in dom ((f | X) * g) by A10, FUNCT_1:11; ::_thesis: verum
end;
now__::_thesis:_for_x_being_set_st_x_in_dom_((f_|_X)_*_g)_holds_
((f_|_X)_*_g)_._x_=_(f_*_(X_|`_g))_._x
let x be set ; ::_thesis: ( x in dom ((f | X) * g) implies ((f | X) * g) . x = (f * (X |` g)) . x )
assume A12: x in dom ((f | X) * g) ; ::_thesis: ((f | X) * g) . x = (f * (X |` g)) . x
then  ( ((f | X) * g) . x = (f | X) . (g . x) & g . x in dom (f | X) ) by FUNCT_1:11, FUNCT_1:12;
then A13: ((f | X) * g) . x = f . (g . x) by FUNCT_1:47;
 ( (f * (X |` g)) . x = f . ((X |` g) . x) & x in dom (X |` g) ) by A2, A12, FUNCT_1:11, FUNCT_1:12;
hence  ((f | X) * g) . x = (f * (X |` g)) . x by A13, FUNCT_1:53; ::_thesis: verum
end;
hence  (f | X) * g = f * (X |` g) by A2, FUNCT_1:2; ::_thesis: verum
end;

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]
proof
A2: for x being set st x in F1() holds
ex y being set st
( y in F2() & P1[x,y] )
proof
let x be set ; ::_thesis: ( x in F1() implies ex y being set st
( y in F2() & P1[x,y] ) )
assume  x in F1() ; ::_thesis: ex y being set st
( y in F2() & P1[x,y] )
then consider y being Element of F2() such that
A3: P1[x,y] by A1;
take  y ; ::_thesis: ( y in F2() & P1[x,y] )
thus  ( y in F2() & P1[x,y] ) by A3; ::_thesis: verum
end;
consider f being Function such that
A4: ( dom f = F1() & rng f c= F2() & ( for x being set st x in F1() holds
P1[x,f . x] ) ) from FUNCT_1:sch_5(A2);
reconsider f = f as Function of F1(),F2() by A4, FUNCT_2:def_1, RELSET_1:4;
take  f ; ::_thesis: for x being set st x in F1() holds
P1[x,f . x]
thus  for x being set st x in F1() holds
P1[x,f . x] by A4; ::_thesis: verum
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 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
deffunc H3( Element of Funcs (A,D1), Element of Funcs (A,D2)) ->  Element of Funcs (A,D) = f .: ($1,$2);
consider b being Function of [:(Funcs (A,D1)),(Funcs (A,D2)):],(Funcs (A,D)) such that
A1: for f1 being Element of Funcs (A,D1)
for f2 being Element of Funcs (A,D2) holds b . (f1,f2) = H3(f1,f2) from BINOP_1:sch_4();
take  b ; ::_thesis: for f1 being Element of Funcs (A,D1)
for f2 being Element of Funcs (A,D2) holds b . (f1,f2) = f .: (f1,f2)
let f1 be Element of Funcs (A,D1); ::_thesis: for f2 being Element of Funcs (A,D2) holds b . (f1,f2) = f .: (f1,f2)
let f2 be Element of Funcs (A,D2); ::_thesis: b . (f1,f2) = f .: (f1,f2)
thus  b . (f1,f2) = f .: (f1,f2) by A1; ::_thesis: verum
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
let o1, o2 be Function of [:(Funcs (A,D1)),(Funcs (A,D2)):],(Funcs (A,D)); ::_thesis: ( ( for f1 being Element of Funcs (A,D1)
for f2 being Element of Funcs (A,D2) holds o1 . (f1,f2) = f .: (f1,f2) ) & ( for f1 being Element of Funcs (A,D1)
for f2 being Element of Funcs (A,D2) holds o2 . (f1,f2) = f .: (f1,f2) ) implies o1 = o2 )
assume that
A2: for f1 being Element of Funcs (A,D1)
for f2 being Element of Funcs (A,D2) holds o1 . (f1,f2) = f .: (f1,f2) and
A3: for f1 being Element of Funcs (A,D1)
for f2 being Element of Funcs (A,D2) holds o2 . (f1,f2) = f .: (f1,f2) ; ::_thesis: o1 = o2
now__::_thesis:_for_f1_being_Element_of_Funcs_(A,D1)
for_f2_being_Element_of_Funcs_(A,D2)_holds_o1_._(f1,f2)_=_o2_._(f1,f2)
let f1 be Element of Funcs (A,D1); ::_thesis: for f2 being Element of Funcs (A,D2) holds o1 . (f1,f2) = o2 . (f1,f2)
let f2 be Element of Funcs (A,D2); ::_thesis: o1 . (f1,f2) = o2 . (f1,f2)
thus o1 . (f1,f2) = f .: (f1,f2) by A2
.= o2 . (f1,f2) by A3 ; ::_thesis: verum
end;
hence  o1 = o2 by BINOP_1:2; ::_thesis: verum
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
let D1, D2, D be non empty set ; ::_thesis: 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))
let f be Function of [:D1,D2:],D; ::_thesis: 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))
let A be set ; ::_thesis: 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))
let f1 be Function of A,D1; ::_thesis: 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))
let f2 be Function of A,D2; ::_thesis: for x being set st x in A holds
((f,D) .: A) .. (f1,f2,x) = f . ((f1 . x),(f2 . x))
 ( dom f2 = A & rng f2 c= D2 ) by FUNCT_2:def_1;
then reconsider f2 = f2 as Element of Funcs (A,D2) by FUNCT_2:def_2;
 ( dom f1 = A & rng f1 c= D1 ) by FUNCT_2:def_1;
then reconsider f1 = f1 as Element of Funcs (A,D1) by FUNCT_2:def_2;
A1: dom (f .: (f1,f2)) = A by FUNCT_2:def_1;
A2: ( ((f,D) .: A) . (f1,f2) = f .: (f1,f2) & [f1,f2] = [f1,f2] ) by Def2;
let x be set ; ::_thesis: ( x in A implies ((f,D) .: A) .. (f1,f2,x) = f . ((f1 . x),(f2 . x)) )
assume A3: x in A ; ::_thesis: ((f,D) .: A) .. (f1,f2,x) = f . ((f1 . x),(f2 . x))
 ( dom ((f,D) .: A) = [:(Funcs (A,D1)),(Funcs (A,D2)):] & (f .: (f1,f2)) . x = f . ((f1 . x),(f2 . x)) ) by A3, A1, FUNCOP_1:22, FUNCT_2:def_1;
hence  ((f,D) .: A) .. (f1,f2,x) = f . ((f1 . x),(f2 . x)) by A3, A1, A2, FUNCT_5:38; ::_thesis: verum
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
let A be set ; ::_thesis: 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)
let D be non empty set ; ::_thesis: 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)
let o be BinOp of D; ::_thesis: for f, g being Function of A,D st o is commutative holds
o .: (f,g) = o .: (g,f)
let f, g be Function of A,D; ::_thesis: ( o is commutative implies o .: (f,g) = o .: (g,f) )
A1: dom (o .: (f,g)) = A by FUNCT_2:def_1;
A2: ( dom f = A & dom g = A ) by FUNCT_2:def_1;
A3: dom (o .: (g,f)) = A by FUNCT_2:def_1;
assume A4: for a, b being Element of D holds o . (a,b) = o . (b,a) ; :: according to BINOP_1:def_2 ::_thesis: o .: (f,g) = o .: (g,f)
now__::_thesis:_for_x_being_set_st_x_in_A_holds_
(o_.:_(f,g))_._x_=_(o_.:_(g,f))_._x
let x be set ; ::_thesis: ( x in A implies (o .: (f,g)) . x = (o .: (g,f)) . x )
assume A5: x in A ; ::_thesis: (o .: (f,g)) . x = (o .: (g,f)) . x
then  ( f . x in rng f & g . x in rng g ) by A2, FUNCT_1:def_3;
then reconsider a = f . x, b = g . x as Element of D ;
thus (o .: (f,g)) . x = o . (a,b) by A1, A5, FUNCOP_1:22
.= o . (b,a) by A4
.= (o .: (g,f)) . x by A3, A5, FUNCOP_1:22 ; ::_thesis: verum
end;
hence  o .: (f,g) = o .: (g,f) by A1, A3, FUNCT_1:2; ::_thesis: verum
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
let A be set ; ::_thesis: 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)))
let D be non empty set ; ::_thesis: 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)))
let o be BinOp of D; ::_thesis: for f, g, h being Function of A,D st o is associative holds
o .: ((o .: (f,g)),h) = o .: (f,(o .: (g,h)))
let f, g, h be Function of A,D; ::_thesis: ( o is associative implies o .: ((o .: (f,g)),h) = o .: (f,(o .: (g,h))) )
A1: dom (o .: (f,g)) = A by FUNCT_2:def_1;
A2: dom (o .: (g,h)) = A by FUNCT_2:def_1;
A3: ( dom f = A & dom g = A ) by FUNCT_2:def_1;
A4: dom (o .: ((o .: (f,g)),h)) = A by FUNCT_2:def_1;
A5: dom h = A by FUNCT_2:def_1;
A6: dom (o .: (f,(o .: (g,h)))) = A by FUNCT_2:def_1;
assume A7: for a, b, c being Element of D holds o . ((o . (a,b)),c) = o . (a,(o . (b,c))) ; :: according to BINOP_1:def_3 ::_thesis: o .: ((o .: (f,g)),h) = o .: (f,(o .: (g,h)))
now__::_thesis:_for_x_being_set_st_x_in_A_holds_
(o_.:_((o_.:_(f,g)),h))_._x_=_(o_.:_(f,(o_.:_(g,h))))_._x
let x be set ; ::_thesis: ( x in A implies (o .: ((o .: (f,g)),h)) . x = (o .: (f,(o .: (g,h)))) . x )
assume A8: x in A ; ::_thesis: (o .: ((o .: (f,g)),h)) . x = (o .: (f,(o .: (g,h)))) . x
then A9: h . x in rng h by A5, FUNCT_1:def_3;
 ( f . x in rng f & g . x in rng g ) by A3, A8, FUNCT_1:def_3;
then reconsider a = f . x, b = g . x, c = h . x as Element of D by A9;
thus (o .: ((o .: (f,g)),h)) . x = o . (((o .: (f,g)) . x),c) by A4, A8, FUNCOP_1:22
.= o . ((o . (a,b)),c) by A1, A8, FUNCOP_1:22
.= o . (a,(o . (b,c))) by A7
.= o . (a,((o .: (g,h)) . x)) by A2, A8, FUNCOP_1:22
.= (o .: (f,(o .: (g,h)))) . x by A6, A8, FUNCOP_1:22 ; ::_thesis: verum
end;
hence  o .: ((o .: (f,g)),h) = o .: (f,(o .: (g,h))) by A4, A6, FUNCT_1:2; ::_thesis: verum
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
let A be set ; ::_thesis: 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 )
let D be non empty set ; ::_thesis: 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 )
let a be Element of D; ::_thesis: 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 )
let o be BinOp of D; ::_thesis: for f being Function of A,D st a is_a_unity_wrt o holds
( o [;] (a,f) = f & o [:] (f,a) = f )
let f be Function of A,D; ::_thesis: ( a is_a_unity_wrt o implies ( o [;] (a,f) = f & o [:] (f,a) = f ) )
assume A1: a is_a_unity_wrt o ; ::_thesis: ( o [;] (a,f) = f & o [:] (f,a) = f )
A2: dom f = A by FUNCT_2:def_1;
A3: dom (o [;] (a,f)) = A by FUNCT_2:def_1;
now__::_thesis:_for_x_being_set_st_x_in_A_holds_
(o_[;]_(a,f))_._x_=_f_._x
let x be set ; ::_thesis: ( x in A implies (o [;] (a,f)) . x = f . x )
assume A4: x in A ; ::_thesis: (o [;] (a,f)) . x = f . x
then  f . x in rng f by A2, FUNCT_1:def_3;
then reconsider b = f . x as Element of D ;
thus (o [;] (a,f)) . x = o . (a,b) by A3, A4, FUNCOP_1:32
.= f . x by A1, BINOP_1:3 ; ::_thesis: verum
end;
hence  o [;] (a,f) = f by A3, A2, FUNCT_1:2; ::_thesis: o [:] (f,a) = f
A5: dom (o [:] (f,a)) = A by FUNCT_2:def_1;
now__::_thesis:_for_x_being_set_st_x_in_A_holds_
(o_[:]_(f,a))_._x_=_f_._x
let x be set ; ::_thesis: ( x in A implies (o [:] (f,a)) . x = f . x )
assume A6: x in A ; ::_thesis: (o [:] (f,a)) . x = f . x
then  f . x in rng f by A2, FUNCT_1:def_3;
then reconsider b = f . x as Element of D ;
thus (o [:] (f,a)) . x = o . (b,a) by A5, A6, FUNCOP_1:27
.= f . x by A1, BINOP_1:3 ; ::_thesis: verum
end;
hence  o [:] (f,a) = f by A5, A2, FUNCT_1:2; ::_thesis: verum
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
let A be set ; ::_thesis: 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
let D be non empty set ; ::_thesis: for o being BinOp of D
for f being Function of A,D st o is idempotent holds
o .: (f,f) = f
let o be BinOp of D; ::_thesis: for f being Function of A,D st o is idempotent holds
o .: (f,f) = f
let f be Function of A,D; ::_thesis: ( o is idempotent implies o .: (f,f) = f )
A1: dom (o .: (f,f)) = A by FUNCT_2:def_1;
assume A2: for a being Element of D holds o . (a,a) = a ; :: according to BINOP_1:def_4 ::_thesis: o .: (f,f) = f
A3: now__::_thesis:_for_x_being_set_st_x_in_A_holds_
(o_.:_(f,f))_._x_=_f_._x
let x be set ; ::_thesis: ( x in A implies (o .: (f,f)) . x = f . x )
assume A4: x in A ; ::_thesis: (o .: (f,f)) . x = f . x
then reconsider a = f . x as Element of D by FUNCT_2:5;
thus (o .: (f,f)) . x = o . (a,a) by A1, A4, FUNCOP_1:22
.= f . x by A2 ; ::_thesis: verum
end;
 dom f = A by FUNCT_2:def_1;
hence  o .: (f,f) = f by A1, A3, FUNCT_1:2; ::_thesis: verum
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
let A be set ; ::_thesis: for D being non empty set
for o being BinOp of D st o is commutative holds
(o,D) .: A is commutative
let D be non empty set ; ::_thesis: for o being BinOp of D st o is commutative holds
(o,D) .: A is commutative
let o be BinOp of D; ::_thesis: ( o is commutative implies (o,D) .: A is commutative )
assume A1: o is commutative ; ::_thesis: (o,D) .: A is commutative
set h = (o,D) .: A;
let f, g be Element of Funcs (A,D); :: according to BINOP_1:def_2 ::_thesis: ((o,D) .: A) . (f,g) = ((o,D) .: A) . (g,f)
thus ((o,D) .: A) . (f,g) = o .: (f,g) by Def2
.= o .: (g,f) by A1, Th3
.= ((o,D) .: A) . (g,f) by Def2 ; ::_thesis: verum
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
let A be set ; ::_thesis: for D being non empty set
for o being BinOp of D st o is associative holds
(o,D) .: A is associative
let D be non empty set ; ::_thesis: for o being BinOp of D st o is associative holds
(o,D) .: A is associative
let o be BinOp of D; ::_thesis: ( o is associative implies (o,D) .: A is associative )
assume A1: o is associative ; ::_thesis: (o,D) .: A is associative
set F = (o,D) .: A;
let f, g, h be Element of Funcs (A,D); :: according to BINOP_1:def_3 ::_thesis: ((o,D) .: A) . (f,(((o,D) .: A) . (g,h))) = ((o,D) .: A) . ((((o,D) .: A) . (f,g)),h)
thus ((o,D) .: A) . ((((o,D) .: A) . (f,g)),h) = ((o,D) .: A) . ((o .: (f,g)),h) by Def2
.= o .: ((o .: (f,g)),h) by Def2
.= o .: (f,(o .: (g,h))) by A1, Th4
.= ((o,D) .: A) . (f,(o .: (g,h))) by Def2
.= ((o,D) .: A) . (f,(((o,D) .: A) . (g,h))) by Def2 ; ::_thesis: verum
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
let A be set ; ::_thesis: 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
let D be non empty set ; ::_thesis: 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
let a be Element of D; ::_thesis: for o being BinOp of D st a is_a_unity_wrt o holds
A --> a is_a_unity_wrt (o,D) .: A
let o be BinOp of D; ::_thesis: ( a is_a_unity_wrt o implies A --> a is_a_unity_wrt (o,D) .: A )
set e = A --> a;
set F = (o,D) .: A;
assume A1: a is_a_unity_wrt o ; ::_thesis: A --> a is_a_unity_wrt (o,D) .: A
now__::_thesis:_for_f_being_Element_of_Funcs_(A,D)_holds_
(_((o,D)_.:_A)_._((A_-->_a),f)_=_f_&_((o,D)_.:_A)_._(f,(A_-->_a))_=_f_)
let f be Element of Funcs (A,D); ::_thesis: ( ((o,D) .: A) . ((A --> a),f) = f & ((o,D) .: A) . (f,(A --> a)) = f )
A2: dom f = A by FUNCT_2:def_1;
thus ((o,D) .: A) . ((A --> a),f) = o .: ((A --> a),f) by Def2
.= o [;] (a,f) by A2, FUNCOP_1:31
.= f by A1, Th5 ; ::_thesis: ((o,D) .: A) . (f,(A --> a)) = f
thus ((o,D) .: A) . (f,(A --> a)) = o .: (f,(A --> a)) by Def2
.= o [:] (f,a) by A2, FUNCOP_1:26
.= f by A1, Th5 ; ::_thesis: verum
end;
hence  A --> a is_a_unity_wrt (o,D) .: A by BINOP_1:3; ::_thesis: verum
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
let A be set ; ::_thesis: 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 )
let D be non empty set ; ::_thesis: 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 )
let o be BinOp of D; ::_thesis: ( o is having_a_unity implies ( the_unity_wrt ((o,D) .: A) = A --> (the_unity_wrt o) & (o,D) .: A is having_a_unity ) )
given a being Element of D such that A1: a is_a_unity_wrt o ; :: according to SETWISEO:def_2 ::_thesis: ( the_unity_wrt ((o,D) .: A) = A --> (the_unity_wrt o) & (o,D) .: A is having_a_unity )
 ( a = the_unity_wrt o & A --> a is_a_unity_wrt (o,D) .: A ) by A1, Th9, BINOP_1:def_8;
hence  the_unity_wrt ((o,D) .: A) = A --> (the_unity_wrt o) by BINOP_1:def_8; ::_thesis: (o,D) .: A is having_a_unity
take  A --> a ; :: according to SETWISEO:def_2 ::_thesis: A --> a is_a_unity_wrt (o,D) .: A
thus  A --> a is_a_unity_wrt (o,D) .: A by A1, Th9; ::_thesis: verum
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
let A be set ; ::_thesis: for D being non empty set
for o being BinOp of D st o is idempotent holds
(o,D) .: A is idempotent
let D be non empty set ; ::_thesis: for o being BinOp of D st o is idempotent holds
(o,D) .: A is idempotent
let o be BinOp of D; ::_thesis: ( o is idempotent implies (o,D) .: A is idempotent )
assume A1: o is idempotent ; ::_thesis: (o,D) .: A is idempotent
let f be Element of Funcs (A,D); :: according to BINOP_1:def_4 ::_thesis: ((o,D) .: A) . (f,f) = f
thus ((o,D) .: A) . (f,f) = o .: (f,f) by Def2
.= f by A1, Th6 ; ::_thesis: verum
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
let A be set ; ::_thesis: for D being non empty set
for o being BinOp of D st o is invertible holds
(o,D) .: A is invertible
let D be non empty set ; ::_thesis: for o being BinOp of D st o is invertible holds
(o,D) .: A is invertible
let o be BinOp of D; ::_thesis: ( o is invertible implies (o,D) .: A is invertible )
assume A1: for a, b being Element of D ex r, l being Element of D st
( o . (a,r) = b & o . (l,a) = b ) ; :: according to MONOID_0:def_5 ::_thesis: (o,D) .: A is invertible
let f, g be Element of Funcs (A,D); :: according to MONOID_0:def_5 ::_thesis: ex b1, b2 being Element of Funcs (A,D) st
( ((o,D) .: A) . (f,b1) = g & ((o,D) .: A) . (b2,f) = g )
defpred S1[ set , set ] means o . ((f . $1),$2) = g . $1;
A2: for x being set st x in A holds
ex c being Element of D st S1[x,c]
proof
let x be set ; ::_thesis: ( x in A implies ex c being Element of D st S1[x,c] )
assume  x in A ; ::_thesis: ex c being Element of D st S1[x,c]
then reconsider a = f . x, b = g . x as Element of D by FUNCT_2:5;
consider r, l being Element of D such that
A3: o . (a,r) = b and
 o . (l,a) = b by A1;
take  r ; ::_thesis: S1[x,r]
thus  S1[x,r] by A3; ::_thesis: verum
end;
consider h1 being Function of A,D such that
A4: for x being set st x in A holds
S1[x,h1 . x] from MONOID_1:sch_1(A2);
defpred S2[ set , set ] means o . ($2,(f . $1)) = g . $1;
A5: for x being set st x in A holds
ex c being Element of D st S2[x,c]
proof
let x be set ; ::_thesis: ( x in A implies ex c being Element of D st S2[x,c] )
assume  x in A ; ::_thesis: ex c being Element of D st S2[x,c]
then reconsider a = f . x, b = g . x as Element of D by FUNCT_2:5;
consider r, l being Element of D such that
 o . (a,r) = b and
A6: o . (l,a) = b by A1;
take  l ; ::_thesis: S2[x,l]
thus  S2[x,l] by A6; ::_thesis: verum
end;
consider h2 being Function of A,D such that
A7: for x being set st x in A holds
S2[x,h2 . x] from MONOID_1:sch_1(A5);
A8: ( dom h1 = A & dom h2 = A ) by FUNCT_2:def_1;
 ( rng h1 c= D & rng h2 c= D ) ;
then reconsider h1 = h1, h2 = h2 as Element of Funcs (A,D) by A8, FUNCT_2:def_2;
take  h1 ; ::_thesis: ex b1 being Element of Funcs (A,D) st
( ((o,D) .: A) . (f,h1) = g & ((o,D) .: A) . (b1,f) = g )
take  h2 ; ::_thesis: ( ((o,D) .: A) . (f,h1) = g & ((o,D) .: A) . (h2,f) = g )
A9: dom g = A by FUNCT_2:def_1;
A10: dom (o .: (f,h1)) = A by FUNCT_2:def_1;
A11: now__::_thesis:_for_x_being_set_st_x_in_A_holds_
(o_.:_(f,h1))_._x_=_g_._x
let x be set ; ::_thesis: ( x in A implies (o .: (f,h1)) . x = g . x )
assume A12: x in A ; ::_thesis: (o .: (f,h1)) . x = g . x
hence (o .: (f,h1)) . x = o . ((f . x),(h1 . x)) by A10, FUNCOP_1:22
.= g . x by A4, A12 ;
::_thesis: verum
end;
 o .: (f,h1) = ((o,D) .: A) . (f,h1) by Def2;
hence  ((o,D) .: A) . (f,h1) = g by A10, A9, A11, FUNCT_1:2; ::_thesis: ((o,D) .: A) . (h2,f) = g
A13: dom (o .: (h2,f)) = A by FUNCT_2:def_1;
A14: now__::_thesis:_for_x_being_set_st_x_in_A_holds_
(o_.:_(h2,f))_._x_=_g_._x
let x be set ; ::_thesis: ( x in A implies (o .: (h2,f)) . x = g . x )
assume A15: x in A ; ::_thesis: (o .: (h2,f)) . x = g . x
hence (o .: (h2,f)) . x = o . ((h2 . x),(f . x)) by A13, FUNCOP_1:22
.= g . x by A7, A15 ;
::_thesis: verum
end;
 o .: (h2,f) = ((o,D) .: A) . (h2,f) by Def2;
hence  ((o,D) .: A) . (h2,f) = g by A13, A9, A14, FUNCT_1:2; ::_thesis: verum
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
let A be set ; ::_thesis: for D being non empty set
for o being BinOp of D st o is cancelable holds
(o,D) .: A is cancelable
let D be non empty set ; ::_thesis: for o being BinOp of D st o is cancelable holds
(o,D) .: A is cancelable
let o be BinOp of D; ::_thesis: ( o is cancelable implies (o,D) .: A is cancelable )
assume A1: for a, b, c being Element of D st ( o . (a,b) = o . (a,c) or o . (b,a) = o . (c,a) ) holds
b = c ; :: according to MONOID_0:def_8 ::_thesis: (o,D) .: A is cancelable
let f, g, h be Element of Funcs (A,D); :: according to MONOID_0:def_8 ::_thesis: ( ( not ((o,D) .: A) . (f,g) = ((o,D) .: A) . (f,h) & not ((o,D) .: A) . (g,f) = ((o,D) .: A) . (h,f) ) or g = h )
assume A2: ( ((o,D) .: A) . (f,g) = ((o,D) .: A) . (f,h) or ((o,D) .: A) . (g,f) = ((o,D) .: A) . (h,f) ) ; ::_thesis: g = h
A3: ( A = dom (o .: (g,f)) & A = dom (o .: (h,f)) ) by FUNCT_2:def_1;
A4: ( ((o,D) .: A) . (f,h) = o .: (f,h) & ((o,D) .: A) . (h,f) = o .: (h,f) ) by Def2;
A5: ( A = dom (o .: (f,g)) & A = dom (o .: (f,h)) ) by FUNCT_2:def_1;
A6: ( ((o,D) .: A) . (f,g) = o .: (f,g) & ((o,D) .: A) . (g,f) = o .: (g,f) ) by Def2;
A7: now__::_thesis:_for_x_being_set_st_x_in_A_holds_
g_._x_=_h_._x
let x be set ; ::_thesis: ( x in A implies g . x = h . x )
assume A8: x in A ; ::_thesis: g . x = h . x
then reconsider a = f . x, b = g . x, c = h . x as Element of D by FUNCT_2:5;
A9: ( (o .: (g,f)) . x = o . (b,a) & (o .: (h,f)) . x = o . (c,a) ) by A3, A8, FUNCOP_1:22;
 ( (o .: (f,g)) . x = o . (a,b) & (o .: (f,h)) . x = o . (a,c) ) by A5, A8, FUNCOP_1:22;
hence  g . x = h . x by A1, A2, A6, A4, A9; ::_thesis: verum
end;
 ( dom g = A & dom h = A ) by FUNCT_2:def_1;
hence  g = h by A7, FUNCT_1:2; ::_thesis: verum
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
let A be set ; ::_thesis: for D being non empty set
for o being BinOp of D st o is uniquely-decomposable holds
(o,D) .: A is uniquely-decomposable
let D be non empty set ; ::_thesis: for o being BinOp of D st o is uniquely-decomposable holds
(o,D) .: A is uniquely-decomposable
let o be BinOp of D; ::_thesis: ( o is uniquely-decomposable implies (o,D) .: A is uniquely-decomposable )
assume that
A1: o is having_a_unity and
A2: for a, b being Element of D st o . (a,b) = the_unity_wrt o holds
( a = b & b = the_unity_wrt o ) ; :: according to MONOID_0:def_9 ::_thesis: (o,D) .: A is uniquely-decomposable
A3: the_unity_wrt ((o,D) .: A) = A --> (the_unity_wrt o) by A1, Th10;
thus  (o,D) .: A is having_a_unity by A1, Th10; :: according to MONOID_0:def_9 ::_thesis: for b1, b2 being Element of Funcs (A,D) holds
( not ((o,D) .: A) . (b1,b2) = the_unity_wrt ((o,D) .: A) or ( b1 = b2 & b2 = the_unity_wrt ((o,D) .: A) ) )
let f, g be Element of Funcs (A,D); ::_thesis: ( not ((o,D) .: A) . (f,g) = the_unity_wrt ((o,D) .: A) or ( f = g & g = the_unity_wrt ((o,D) .: A) ) )
assume A4: ((o,D) .: A) . (f,g) = the_unity_wrt ((o,D) .: A) ; ::_thesis: ( f = g & g = the_unity_wrt ((o,D) .: A) )
A5: dom (o .: (f,g)) = A by FUNCT_2:def_1;
A6: ((o,D) .: A) . (f,g) = o .: (f,g) by Def2;
A7: now__::_thesis:_for_x_being_set_st_x_in_A_holds_
f_._x_=_g_._x
let x be set ; ::_thesis: ( x in A implies f . x = g . x )
assume A8: x in A ; ::_thesis: f . x = g . x
then reconsider a = f . x, b = g . x as Element of D by FUNCT_2:5;
 ( (o .: (f,g)) . x = o . (a,b) & (A --> (the_unity_wrt o)) . x = the_unity_wrt o ) by A5, A8, FUNCOP_1:7, FUNCOP_1:22;
hence  f . x = g . x by A2, A4, A6, A3; ::_thesis: verum
end;
A9: now__::_thesis:_for_x_being_set_st_x_in_A_holds_
g_._x_=_(A_-->_(the_unity_wrt_o))_._x
let x be set ; ::_thesis: ( x in A implies g . x = (A --> (the_unity_wrt o)) . x )
assume A10: x in A ; ::_thesis: g . x = (A --> (the_unity_wrt o)) . x
then reconsider a = f . x, b = g . x as Element of D by FUNCT_2:5;
 ( (o .: (f,g)) . x = o . (a,b) & (A --> (the_unity_wrt o)) . x = the_unity_wrt o ) by A5, A10, FUNCOP_1:7, FUNCOP_1:22;
hence  g . x = (A --> (the_unity_wrt o)) . x by A2, A4, A6, A3; ::_thesis: verum
end;
A11: dom g = A by FUNCT_2:def_1;
 dom f = A by FUNCT_2:def_1;
hence  f = g by A11, A7, FUNCT_1:2; ::_thesis: g = the_unity_wrt ((o,D) .: A)
 dom (A --> (the_unity_wrt o)) = A by FUNCT_2:def_1;
hence  g = the_unity_wrt ((o,D) .: A) by A3, A11, A9, FUNCT_1:2; ::_thesis: verum
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
let A be set ; ::_thesis: 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
let D be non empty set ; ::_thesis: for o, o9 being BinOp of D st o absorbs o9 holds
(o,D) .: A absorbs (o9,D) .: A
let o, o9 be BinOp of D; ::_thesis: ( o absorbs o9 implies (o,D) .: A absorbs (o9,D) .: A )
assume A1: for a, b being Element of D holds o . (a,(o9 . (a,b))) = a ; :: according to LATTICE2:def_1 ::_thesis: (o,D) .: A absorbs (o9,D) .: A
let f, g be Element of Funcs (A,D); :: according to LATTICE2:def_1 ::_thesis: ((o,D) .: A) . (f,(((o9,D) .: A) . (f,g))) = f
A2: dom (o .: (f,(o9 .: (f,g)))) = A by FUNCT_2:def_1;
A3: dom (o9 .: (f,g)) = A by FUNCT_2:def_1;
A4: now__::_thesis:_for_x_being_set_st_x_in_A_holds_
f_._x_=_(o_.:_(f,(o9_.:_(f,g))))_._x
let x be set ; ::_thesis: ( x in A implies f . x = (o .: (f,(o9 .: (f,g)))) . x )
assume A5: x in A ; ::_thesis: f . x = (o .: (f,(o9 .: (f,g)))) . x
then reconsider a = f . x, b = g . x as Element of D by FUNCT_2:5;
 ( (o .: (f,(o9 .: (f,g)))) . x = o . (a,((o9 .: (f,g)) . x)) & (o9 .: (f,g)) . x = o9 . (a,b) ) by A3, A2, A5, FUNCOP_1:22;
hence  f . x = (o .: (f,(o9 .: (f,g)))) . x by A1; ::_thesis: verum
end;
A6: dom f = A by FUNCT_2:def_1;
 ( ((o9,D) .: A) . (f,g) = o9 .: (f,g) & ((o,D) .: A) . (f,(o9 .: (f,g))) = o .: (f,(o9 .: (f,g))) ) by Def2;
hence  ((o,D) .: A) . (f,(((o9,D) .: A) . (f,g))) = f by A6, A2, A4, FUNCT_1:2; ::_thesis: verum
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
let A be set ; ::_thesis: 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
let D1, D2, D, E1, E2, E be non empty set ; ::_thesis: 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
let o1 be Function of [:D1,D2:],D; ::_thesis: for o2 being Function of [:E1,E2:],E st o1 c= o2 holds
(o1,D) .: A c= (o2,E) .: A
let o2 be Function of [:E1,E2:],E; ::_thesis: ( o1 c= o2 implies (o1,D) .: A c= (o2,E) .: A )
A1: dom o1 = [:D1,D2:] by FUNCT_2:def_1;
assume A2: o1 c= o2 ; ::_thesis: (o1,D) .: A c= (o2,E) .: A
then A3: dom o1 c= dom o2 by GRFUNC_1:2;
A4: dom o2 = [:E1,E2:] by FUNCT_2:def_1;
then  D2 c= E2 by A3, A1, ZFMISC_1:114;
then A5: Funcs (A,D2) c= Funcs (A,E2) by FUNCT_5:56;
 D1 c= E1 by A3, A1, A4, ZFMISC_1:114;
then A6: Funcs (A,D1) c= Funcs (A,E1) by FUNCT_5:56;
A7: now__::_thesis:_for_x_being_set_st_x_in_dom_((o1,D)_.:_A)_holds_
((o1,D)_.:_A)_._x_=_((o2,E)_.:_A)_._x
let x be set ; ::_thesis: ( x in dom ((o1,D) .: A) implies ((o1,D) .: A) . x = ((o2,E) .: A) . x )
assume  x in dom ((o1,D) .: A) ; ::_thesis: ((o1,D) .: A) . x = ((o2,E) .: A) . x
then reconsider y = x as Element of [:(Funcs (A,D1)),(Funcs (A,D2)):] ;
reconsider g2 = y `2 as Element of Funcs (A,E2) by A5, TARSKI:def_3;
reconsider f2 = y `2 as Element of Funcs (A,D2) ;
reconsider g1 = y `1 as Element of Funcs (A,E1) by A6, TARSKI:def_3;
reconsider f1 = y `1 as Element of Funcs (A,D1) ;
A8: ( dom (o2 .: (g1,g2)) = A & dom (o1 .: (f1,f2)) = A ) by FUNCT_2:def_1;
A9: ( dom f1 = A & dom f2 = A ) by FUNCT_2:def_1;
A10: now__::_thesis:_for_z_being_set_st_z_in_A_holds_
(o2_.:_(g1,g2))_._z_=_(o1_.:_(f1,f2))_._z
let z be set ; ::_thesis: ( z in A implies (o2 .: (g1,g2)) . z = (o1 .: (f1,f2)) . z )
assume A11: z in A ; ::_thesis: (o2 .: (g1,g2)) . z = (o1 .: (f1,f2)) . z
then  ( f1 . z in rng f1 & f2 . z in rng f2 ) by A9, FUNCT_1:def_3;
then A12: [(f1 . z),(f2 . z)] in dom o1 by A1, ZFMISC_1:87;
 ( (o2 .: (g1,g2)) . z = o2 . ((g1 . z),(g2 . z)) & (o1 .: (f1,f2)) . z = o1 . ((f1 . z),(f2 . z)) ) by A8, A11, FUNCOP_1:22;
hence  (o2 .: (g1,g2)) . z = (o1 .: (f1,f2)) . z by A2, A12, GRFUNC_1:2; ::_thesis: verum
end;
A13: [f1,f2] = x by MCART_1:21;
 ( ((o1,D) .: A) . (f1,f2) = o1 .: (f1,f2) & ((o2,E) .: A) . (g1,g2) = o2 .: (g1,g2) ) by Def2;
hence  ((o1,D) .: A) . x = ((o2,E) .: A) . x by A8, A10, A13, FUNCT_1:2; ::_thesis: verum
end;
 ( dom ((o1,D) .: A) = [:(Funcs (A,D1)),(Funcs (A,D2)):] & dom ((o2,E) .: A) = [:(Funcs (A,E1)),(Funcs (A,E2)):] ) by FUNCT_2:def_1;
then  dom ((o1,D) .: A) c= dom ((o2,E) .: A) by A6, A5, ZFMISC_1:96;
hence  (o1,D) .: A c= (o2,E) .: A by A7, GRFUNC_1:2; ::_thesis: verum
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
percases ( G is unital or not G is unital ) ;
suppose G is unital ; ::_thesis: not .: (G,A) is empty
then  .: (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)) #) by Def3;
hence  not the carrier of (.: (G,A)) is empty ; :: according to STRUCT_0:def_1 ::_thesis: verum
end;
suppose not G is unital ; ::_thesis: not .: (G,A) is empty
then  .: (G,A) = multMagma(# (Funcs (A, the carrier of G)),(( the multF of G, the carrier of G) .: A) #) by Def3;
hence  not the carrier of (.: (G,A)) is empty ; :: according to STRUCT_0:def_1 ::_thesis: verum
end;
end;
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
let X be set ; ::_thesis: 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 )
let G be non empty multMagma ; ::_thesis: ( 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 )
A1: ( not G is unital implies .: (G,X) = multMagma(# (Funcs (X,H3(G))),((H1(G),H3(G)) .: X) #) ) by Def3;
 ( G is unital implies .: (G,X) = multLoopStr(# (Funcs (X,H3(G))),((H1(G),H3(G)) .: X),(X --> (the_unity_wrt H1(G))) #) ) by Def3;
hence  ( 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 ) by A1; ::_thesis: verum
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
let x, X be set ; ::_thesis: for G being non empty multMagma holds
( x is Element of (.: (G,X)) iff x is Function of X, the carrier of G )
let G be non empty multMagma ; ::_thesis: ( x is Element of (.: (G,X)) iff x is Function of X, the carrier of G )
 ( x is Element of (.: (G,X)) implies x is Element of Funcs (X,H3(G)) ) by Th17;
hence  ( x is Element of (.: (G,X)) implies x is Function of X,H3(G) ) ; ::_thesis: ( x is Function of X, the carrier of G implies x is Element of (.: (G,X)) )
assume  x is Function of X,H3(G) ; ::_thesis: x is Element of (.: (G,X))
then reconsider f = x as Function of X,H3(G) ;
A1: rng f c= H3(G) ;
 ( H3( .: (G,X)) = Funcs (X,H3(G)) & dom f = X ) by Th17, FUNCT_2:def_1;
hence  x is Element of (.: (G,X)) by A1, FUNCT_2:def_2; ::_thesis: verum
end;

Lm1:  for X being set
for G being non empty multMagma holds .: (G,X) is constituted-Functions
proof
let X be set ; ::_thesis: for G being non empty multMagma holds .: (G,X) is constituted-Functions
let G be non empty multMagma ; ::_thesis: .: (G,X) is constituted-Functions
let a be Element of (.: (G,X)); :: according to MONOID_0:def_1 ::_thesis: a is set
 a is Element of Funcs (X,H3(G)) by Th17;
hence  a is set ; ::_thesis: verum
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
let X be set ; ::_thesis: for G being non empty multMagma
for f being Element of (.: (G,X)) holds
( dom f = X & rng f c= the carrier of G )
let G be non empty multMagma ; ::_thesis: for f being Element of (.: (G,X)) holds
( dom f = X & rng f c= the carrier of G )
let f be Element of (.: (G,X)); ::_thesis: ( dom f = X & rng f c= the carrier of G )
reconsider f = f as Element of Funcs (X,H3(G)) by Th17;
 f = f ;
hence  ( dom f = X & rng f c= the carrier of G ) by FUNCT_2:def_1, RELAT_1:def_19; ::_thesis: verum
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 set st x in X holds
f . x = g . x ) holds
f = g
proof
let X be set ; ::_thesis: 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
let G be non empty multMagma ; ::_thesis: 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
let f, g be Element of (.: (G,X)); ::_thesis: ( ( for x being set st x in X holds
f . x = g . x ) implies f = g )
 ( dom f = X & dom g = X ) by Th19;
hence  ( ( for x being set st x in X holds
f . x = g . x ) implies f = g ) by FUNCT_1:2; ::_thesis: verum
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 funcf . a ->  Element of G;
coherence
 f . a is Element of G
proof
 dom f = A by Th19;
then A1: f . a in rng f by FUNCT_1:def_3;
 rng f c= H3(G) by Th19;
hence  f . a is Element of G by A1; ::_thesis: verum
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
set a = the Element of A;
 dom f = A by Th19;
then  f . the Element of A in rng f by FUNCT_1:def_3;
hence  not rng f is empty ; ::_thesis: verum
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
let D be non empty set ; ::_thesis: 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)
let G be non empty multMagma ; ::_thesis: for f1, f2 being Element of (.: (G,D))
for a being Element of D holds (f1 * f2) . a = (f1 . a) * (f2 . a)
let f1, f2 be Element of (.: (G,D)); ::_thesis: for a being Element of D holds (f1 * f2) . a = (f1 . a) * (f2 . a)
let a be Element of D; ::_thesis: (f1 * f2) . a = (f1 . a) * (f2 . a)
reconsider g1 = f1, g2 = f2 as Element of Funcs (D,H3(G)) by Th17;
 H1( .: (G,D)) = (H1(G),H3(G)) .: D by Th17;
then  ( dom (H1(G) .: (g1,g2)) = D & f1 * f2 = H1(G) .: (g1,g2) ) by Def2, FUNCT_2:def_1;
hence  (f1 * f2) . a = (f1 . a) * (f2 . a) by FUNCOP_1:22; ::_thesis: verum
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
set M = multLoopStr(# (Funcs (A,H3(G))),((H1(G),H3(G)) .: A),(A --> (the_unity_wrt H1(G))) #);
 H1(G) is having_a_unity by MONOID_0:def_10;
then consider a being Element of G such that
A1: a is_a_unity_wrt H1(G) by SETWISEO:def_2;
A2: ( 1. multLoopStr(# (Funcs (A,H3(G))),((H1(G),H3(G)) .: A),(A --> (the_unity_wrt H1(G))) #) = A --> (the_unity_wrt the multF of G) & .: (G,A) = multLoopStr(# (Funcs (A,H3(G))),((H1(G),H3(G)) .: A),(A --> (the_unity_wrt H1(G))) #) ) by Def3;
 ( a = the_unity_wrt H1(G) & A --> a is_a_unity_wrt (H1(G),H3(G)) .: A ) by A1, Th9, BINOP_1:def_8;
hence  .: (G,A) is non empty strict well-unital constituted-Functions multLoopStr by A2, MONOID_0:def_21; ::_thesis: verum
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
let X be set ; ::_thesis: for G being non empty unital multMagma holds 1. (.: (G,X)) = X --> (the_unity_wrt the multF of G)
let G be non empty unital multMagma ; ::_thesis: 1. (.: (G,X)) = X --> (the_unity_wrt the multF of G)
 .: (G,X) = multLoopStr(# (Funcs (X,H3(G))),((H1(G),H3(G)) .: X),(X --> (the_unity_wrt H1(G))) #) by Def3;
hence  1. (.: (G,X)) = X --> (the_unity_wrt the multF of G) ; ::_thesis: verum
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
let G be non empty multMagma ; ::_thesis: 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 ) )
let A be set ; ::_thesis: ( ( 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 ) )
A1: ( H1( .: (G,A)) = (H1(G),H3(G)) .: A & H3( .: (G,A)) = Funcs (A,H3(G)) ) by Th17;
thus  ( G is commutative implies .: (G,A) is commutative ) ::_thesis: ( ( 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
assume  H1(G) is commutative ; :: according to MONOID_0:def_11 ::_thesis: .: (G,A) is commutative
hence  H1( .: (G,A)) is commutative by A1, Th7; :: according to MONOID_0:def_11 ::_thesis: verum
end;
thus  ( G is associative implies .: (G,A) is associative ) ::_thesis: ( ( 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
assume  H1(G) is associative ; :: according to MONOID_0:def_12 ::_thesis: .: (G,A) is associative
hence  H1( .: (G,A)) is associative by A1, Th8; :: according to MONOID_0:def_12 ::_thesis: verum
end;
thus  ( G is idempotent implies .: (G,A) is idempotent ) ::_thesis: ( ( 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
assume  H1(G) is idempotent ; :: according to MONOID_0:def_13 ::_thesis: .: (G,A) is idempotent
hence  H1( .: (G,A)) is idempotent by A1, Th11; :: according to MONOID_0:def_13 ::_thesis: verum
end;
thus  ( G is invertible implies .: (G,A) is invertible ) ::_thesis: ( ( G is cancelable implies .: (G,A) is cancelable ) & ( G is uniquely-decomposable implies .: (G,A) is uniquely-decomposable ) )
proof
assume  H1(G) is invertible ; :: according to MONOID_0:def_16 ::_thesis: .: (G,A) is invertible
hence  H1( .: (G,A)) is invertible by A1, Th12; :: according to MONOID_0:def_16 ::_thesis: verum
end;
thus  ( G is cancelable implies .: (G,A) is cancelable ) ::_thesis: ( G is uniquely-decomposable implies .: (G,A) is uniquely-decomposable )
proof
assume  H1(G) is cancelable ; :: according to MONOID_0:def_19 ::_thesis: .: (G,A) is cancelable
hence  H1( .: (G,A)) is cancelable by A1, Th13; :: according to MONOID_0:def_19 ::_thesis: verum
end;
assume  H1(G) is uniquely-decomposable ; :: according to MONOID_0:def_20 ::_thesis: .: (G,A) is uniquely-decomposable
hence  H1( .: (G,A)) is uniquely-decomposable by A1, Th14; :: according to MONOID_0:def_20 ::_thesis: verum
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
let X be set ; ::_thesis: for G being non empty multMagma
for H being non empty SubStr of G holds .: (H,X) is SubStr of .: (G,X)
let G be non empty multMagma ; ::_thesis: for H being non empty SubStr of G holds .: (H,X) is SubStr of .: (G,X)
let H be non empty SubStr of G; ::_thesis: .: (H,X) is SubStr of .: (G,X)
A1: H1( .: (H,X)) = (H1(H),H3(H)) .: X by Th17;
 ( H1(H) c= H1(G) & H1( .: (G,X)) = (H1(G),H3(G)) .: X ) by Th17, MONOID_0:def_23;
hence  H1( .: (H,X)) c= H1( .: (G,X)) by A1, Th16; :: according to MONOID_0:def_23 ::_thesis: verum
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
let X be set ; ::_thesis: 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)
let G be non empty unital multMagma ; ::_thesis: 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)
let H be non empty SubStr of G; ::_thesis: ( the_unity_wrt the multF of G in the carrier of H implies .: (H,X) is MonoidalSubStr of .: (G,X) )
assume A1: the_unity_wrt the multF of G in H3(H) ; ::_thesis: .: (H,X) is MonoidalSubStr of .: (G,X)
then reconsider G9 = G, H9 = H as non empty unital multMagma by MONOID_0:30;
A2: the_unity_wrt H1(H9) = the_unity_wrt H1(G9) by A1, MONOID_0:30;
A3: H1( .: (H,X)) = (H1(H),H3(H)) .: X by Th17;
 ( H1(H) c= H1(G) & H1( .: (G,X)) = (H1(G),H3(G)) .: X ) by Th17, MONOID_0:def_23;
then A4: H1( .: (H,X)) c= H1( .: (G,X)) by A3, Th16;
 ( 1. (.: (G9,X)) = X --> (the_unity_wrt H1(G)) & 1. (.: (H9,X)) = X --> (the_unity_wrt H1(H)) ) by Th22;
hence  .: (H,X) is MonoidalSubStr of .: (G,X) by A2, A4, MONOID_0:def_25; ::_thesis: verum
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
 ( .: (G,A) is commutative & .: (G,A) is cancelable ) by Th23;
hence  .: (G,A) is strict commutative constituted-Functions cancelable uniquely-decomposable Monoid by Th23; ::_thesis: verum
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 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
let X be set ; ::_thesis: ( the carrier of (MultiSet_over X) = Funcs (X,NAT) & the multF of (MultiSet_over X) = (addnat,NAT) .: X & 1. (MultiSet_over X) = X --> 0 )
 ( multMagma(# the carrier of <NAT,+,0>, the multF of <NAT,+,0> #) = <NAT,+> & the_unity_wrt H1( <NAT,+> ) = 0 ) by MONOID_0:40, MONOID_0:def_22;
hence  ( the carrier of (MultiSet_over X) = Funcs (X,NAT) & the multF of (MultiSet_over X) = (addnat,NAT) .: X & 1. (MultiSet_over X) = X --> 0 ) by Th17, Th22, MONOID_0:46; ::_thesis: verum
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
let x, X be set ; ::_thesis: ( x is Multiset of X iff x is Function of X,NAT )
A1: now__::_thesis:_for_x_being_Function_of_X,NAT_holds_x_is_Element_of_Funcs_(X,NAT)
let x be Function of X,NAT; ::_thesis: x is Element of Funcs (X,NAT)
 ( dom x = X & rng x c= NAT ) by FUNCT_2:def_1;
hence  x is Element of Funcs (X,NAT) by FUNCT_2:def_2; ::_thesis: verum
end;
 ( x is Multiset of X iff x is Element of Funcs (X,NAT) ) by Th26;
hence  ( x is Multiset of X iff x is Function of X,NAT ) by A1; ::_thesis: verum
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
let X be set ; ::_thesis: for m being Multiset of X holds
( dom m = X & rng m c= NAT )
let m be Multiset of X; ::_thesis: ( dom m = X & rng m c= NAT )
 m is Function of X,NAT by Th27;
hence  ( dom m = X & rng m c= NAT ) by FUNCT_2:def_1, RELAT_1:def_19; ::_thesis: verum
end;

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
proof
 dom m = A by Th19;
then A1: m . a in rng m by FUNCT_1:def_3;
 rng m c= NAT by Th19, MONOID_0:46;
hence  m . a is Element of NAT by A1; ::_thesis: verum
end;
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
let D be non empty set ; ::_thesis: for m1, m2 being Multiset of D
for a being Element of D holds (m1 [*] m2) . a = (m1 . a) + (m2 . a)
reconsider N = <NAT,+,0> as non empty multMagma ;
let m1, m2 be Multiset of D; ::_thesis: for a being Element of D holds (m1 [*] m2) . a = (m1 . a) + (m2 . a)
let a be Element of D; ::_thesis: (m1 [*] m2) . a = (m1 . a) + (m2 . a)
reconsider f1 = m1, f2 = m2 as Element of (.: (N,D)) ;
thus (m1 [*] m2) . a = (f1 . a) * (f2 . a) by Th21
.= (m1 . a) + (m2 . a) by MONOID_0:45 ; ::_thesis: verum
end;

theorem Th30: :: MONOID_1:30
for Y, X being set holds chi (Y,X) is Multiset of X
proof
let Y, X be set ; ::_thesis: chi (Y,X) is Multiset of X
 rng (chi (Y,X)) c= {0,1} ;
then A1: rng (chi (Y,X)) c= NAT by XBOOLE_1:1;
 ( dom (chi (Y,X)) = X & H3( MultiSet_over X) = Funcs (X,NAT) ) by Th26, FUNCT_3:def_3;
hence  chi (Y,X) is Multiset of X by A1, FUNCT_2:def_2; ::_thesis: verum
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 funcX --> n ->  Multiset of X;
coherence
 X --> n is Multiset of X
proof
thus  X --> n is Multiset of X by Th27; ::_thesis: verum
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
let A be non empty set ; ::_thesis: for a, b being Element of A holds
( (chi a) . a = 1 & ( b <> a implies (chi a) . b = 0 ) )
let a, b be Element of A; ::_thesis: ( (chi a) . a = 1 & ( b <> a implies (chi a) . b = 0 ) )
A1: ( b <> a implies not b in {a} ) by TARSKI:def_1;
 a in {a} by TARSKI:def_1;
hence  ( (chi a) . a = 1 & ( b <> a implies (chi a) . b = 0 ) ) by A1, FUNCT_3:def_3; ::_thesis: verum
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
let A be non empty set ; ::_thesis: for m1, m2 being Multiset of A st ( for a being Element of A holds m1 . a = m2 . a ) holds
m1 = m2
let m1, m2 be Multiset of A; ::_thesis: ( ( for a being Element of A holds m1 . a = m2 . a ) implies m1 = m2 )
assume  for a being Element of A holds m1 . a = m2 . a ; ::_thesis: m1 = m2
then  for x being set st x in A holds
m1 . x = m2 . x ;
hence  m1 = m2 by Th20; ::_thesis: verum
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
reconsider e = A --> 0 as Function of A,NAT by Th27;
defpred S1[ set ] means  ex f being Function of A,NAT st
( $1 = f & f " (NAT \ {0}) is finite );
A1: for a, b being Multiset of A st S1[a] & S1[b] holds
S1[a [*] b]
proof
let a, b be Multiset of A; ::_thesis: ( S1[a] & S1[b] implies S1[a [*] b] )
reconsider h = a [*] b as Function of A,NAT by Th27;
given f being Function of A,NAT such that A2: a = f and
A3: f " (NAT \ {0}) is finite ; ::_thesis: ( not S1[b] or S1[a [*] b] )
given g being Function of A,NAT such that A4: b = g and
A5: g " (NAT \ {0}) is finite ; ::_thesis: S1[a [*] b]
take  h ; ::_thesis: ( a [*] b = h & h " (NAT \ {0}) is finite )
A6: ( dom f = A & dom g = A ) by FUNCT_2:def_1;
 h " (NAT \ {0}) c= (f " (NAT \ {0})) \/ (g " (NAT \ {0}))
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in h " (NAT \ {0}) or x in (f " (NAT \ {0})) \/ (g " (NAT \ {0})) )
assume A7: x in h " (NAT \ {0}) ; ::_thesis: x in (f " (NAT \ {0})) \/ (g " (NAT \ {0}))
then  h . x in NAT \ {0} by FUNCT_1:def_7;
then A8: not h . x in {0} by XBOOLE_0:def_5;
 ( f . x in rng f & g . x in rng g ) by A6, A7, FUNCT_1:def_3;
then reconsider n = f . x, m = g . x as Element of NAT ;
 h . x = n + m by A2, A4, A7, Th29;
then  ( n <> 0 or m <> 0 ) by A8, TARSKI:def_1;
then  ( not n in {0} or not m in {0} ) by TARSKI:def_1;
then  ( n in NAT \ {0} or m in NAT \ {0} ) by XBOOLE_0:def_5;
then  ( x in f " (NAT \ {0}) or x in g " (NAT \ {0}) ) by A6, A7, FUNCT_1:def_7;
hence  x in (f " (NAT \ {0})) \/ (g " (NAT \ {0})) by XBOOLE_0:def_3; ::_thesis: verum
end;
hence  ( a [*] b = h & h " (NAT \ {0}) is finite ) by A3, A5; ::_thesis: verum
end;
A9: dom e = A by FUNCOP_1:13;
now__::_thesis:_not_e_"_(NAT_\_{0})_<>_{}
set x = the Element of e " (NAT \ {0});
assume A10: e " (NAT \ {0}) <> {} ; ::_thesis: contradiction
then  e . the Element of e " (NAT \ {0}) in NAT \ {0} by FUNCT_1:def_7;
then A11: not e . the Element of e " (NAT \ {0}) in {0} by XBOOLE_0:def_5;
 the Element of e " (NAT \ {0}) in A by A9, A10, FUNCT_1:def_7;
then  e . the Element of e " (NAT \ {0}) = 0 by FUNCOP_1:7;
hence  contradiction by A11, TARSKI:def_1; ::_thesis: verum
end;
then A12: S1[ 1. (MultiSet_over A)] by Th26;
consider M being non empty strict MonoidalSubStr of MultiSet_over A such that
A13: for a being Multiset of A holds
( a in the carrier of M iff S1[a] ) from MONOID_0:sch_2(A1, A12);
reconsider M = M as non empty strict MonoidalSubStr of MultiSet_over A ;
take  M ; ::_thesis: for f being Multiset of A holds
( f in the carrier of M iff f " (NAT \ {0}) is finite )
let f be Multiset of A; ::_thesis: ( f in the carrier of M iff f " (NAT \ {0}) is finite )
thus  ( f in H3(M) implies f " (NAT \ {0}) is finite ) ::_thesis: ( f " (NAT \ {0}) is finite implies f in the carrier of M )
proof
assume  f in H3(M) ; ::_thesis: f " (NAT \ {0}) is finite
then  ex g being Function of A,NAT st
( f = g & g " (NAT \ {0}) is finite ) by A13;
hence  f " (NAT \ {0}) is finite ; ::_thesis: verum
end;
reconsider g = f as Function of A,NAT by Th27;
assume  f " (NAT \ {0}) is finite ; ::_thesis: f in the carrier of M
then  g " (NAT \ {0}) is finite ;
hence  f in the carrier of M by A13; ::_thesis: verum
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
set M = MultiSet_over A;
let M1, M2 be non empty strict MonoidalSubStr of MultiSet_over A; ::_thesis: ( ( for f being Multiset of A holds
( f in the carrier of M1 iff f " (NAT \ {0}) is finite ) ) & ( for f being Multiset of A holds
( f in the carrier of M2 iff f " (NAT \ {0}) is finite ) ) implies M1 = M2 )
assume that
A14: for f being Multiset of A holds
( f in H3(M1) iff f " (NAT \ {0}) is finite ) and
A15: for f being Multiset of A holds
( f in H3(M2) iff f " (NAT \ {0}) is finite ) ; ::_thesis: M1 = M2
A16: H3(M2) c= H3( MultiSet_over A) by MONOID_0:23;
A17: H3(M1) c= H3( MultiSet_over A) by MONOID_0:23;
 H3(M1) = H3(M2)
proof
thus  H3(M1) c= H3(M2) :: according to XBOOLE_0:def_10 ::_thesis: H3(M2) c= H3(M1)
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in H3(M1) or x in H3(M2) )
assume A18: x in H3(M1) ; ::_thesis: x in H3(M2)
then reconsider f = x as Multiset of A by A17;
 f " (NAT \ {0}) is finite by A14, A18;
hence  x in H3(M2) by A15; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in H3(M2) or x in H3(M1) )
assume A19: x in H3(M2) ; ::_thesis: x in H3(M1)
then reconsider f = x as Multiset of A by A16;
 f " (NAT \ {0}) is finite by A15, A19;
hence  x in H3(M1) by A14; ::_thesis: verum
end;
hence  M1 = M2 by MONOID_0:27; ::_thesis: verum
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
let A be non empty set ; ::_thesis: for a being Element of A holds chi a is Element of (finite-MultiSet_over A)
let a be Element of A; ::_thesis: chi a is Element of (finite-MultiSet_over A)
 (chi a) " (NAT \ {0}) c= {a}
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in (chi a) " (NAT \ {0}) or x in {a} )
assume A1: x in (chi a) " (NAT \ {0}) ; ::_thesis: x in {a}
then  x in dom (chi a) by FUNCT_1:def_7;
then reconsider y = x as Element of A by Th28;
 (chi a) . x in NAT \ {0} by A1, FUNCT_1:def_7;
then  not (chi a) . y in {0} by XBOOLE_0:def_5;
then  (chi a) . y <> 0 by TARSKI:def_1;
then  y = a by Th31;
hence  x in {a} by TARSKI:def_1; ::_thesis: verum
end;
hence  chi a is Element of (finite-MultiSet_over A) by Def6; ::_thesis: verum
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
let x be set ; ::_thesis: for A being non empty set
for p being FinSequence of A holds dom ({x} |` (p ^ <*x*>)) = (dom ({x} |` p)) \/ {((len p) + 1)}
let A be non empty set ; ::_thesis: for p being FinSequence of A holds dom ({x} |` (p ^ <*x*>)) = (dom ({x} |` p)) \/ {((len p) + 1)}
let p be FinSequence of A; ::_thesis: dom ({x} |` (p ^ <*x*>)) = (dom ({x} |` p)) \/ {((len p) + 1)}
thus  dom ({x} |` (p ^ <*x*>)) c= (dom ({x} |` p)) \/ {((len p) + 1)} :: according to XBOOLE_0:def_10 ::_thesis: (dom ({x} |` p)) \/ {((len p) + 1)} c= dom ({x} |` (p ^ <*x*>))
proof
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in dom ({x} |` (p ^ <*x*>)) or a in (dom ({x} |` p)) \/ {((len p) + 1)} )
A1: len <*x*> = 1 by FINSEQ_1:40;
A2: Seg (len p) = dom p by FINSEQ_1:def_3;
assume A3: a in dom ({x} |` (p ^ <*x*>)) ; ::_thesis: a in (dom ({x} |` p)) \/ {((len p) + 1)}
then A4: a in dom (p ^ <*x*>) by FUNCT_1:54;
then  a in Seg ((len p) + (len <*x*>)) by FINSEQ_1:def_7;
then  a in (Seg (len p)) \/ {((len p) + 1)} by A1, FINSEQ_1:9;
then A5: ( a in dom p or a in {((len p) + 1)} ) by A2, XBOOLE_0:def_3;
A6: (p ^ <*x*>) . a in {x} by A3, FUNCT_1:54;
reconsider a = a as Element of NAT by A4;
 ( a in dom p implies (p ^ <*x*>) . a = p . a ) by FINSEQ_1:def_7;
then  ( a in dom p implies a in dom ({x} |` p) ) by A6, FUNCT_1:54;
hence  a in (dom ({x} |` p)) \/ {((len p) + 1)} by A5, XBOOLE_0:def_3; ::_thesis: verum
end;
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in (dom ({x} |` p)) \/ {((len p) + 1)} or a in dom ({x} |` (p ^ <*x*>)) )
 len <*x*> = 1 by FINSEQ_1:40;
then A7: dom (p ^ <*x*>) = Seg ((len p) + 1) by FINSEQ_1:def_7;
assume A8: a in (dom ({x} |` p)) \/ {((len p) + 1)} ; ::_thesis: a in dom ({x} |` (p ^ <*x*>))
then  ( a in dom ({x} |` p) or a in {((len p) + 1)} ) by XBOOLE_0:def_3;
then A9: ( ( a in dom p & p . a in {x} ) or ( a in {((len p) + 1)} & a = (len p) + 1 & x in {x} ) ) by FUNCT_1:54, TARSKI:def_1;
 ( Seg (len p) = dom p & Seg ((len p) + 1) = (Seg (len p)) \/ {((len p) + 1)} ) by FINSEQ_1:9, FINSEQ_1:def_3;
then A10: ( (p ^ <*x*>) . ((len p) + 1) = x & a in dom (p ^ <*x*>) ) by A9, A7, FINSEQ_1:42, XBOOLE_0:def_3;
reconsider a = a as Element of NAT by A8;
 ( a in dom p implies (p ^ <*x*>) . a = p . a ) by FINSEQ_1:def_7;
hence  a in dom ({x} |` (p ^ <*x*>)) by A9, A10, FUNCT_1:54; ::_thesis: verum
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
let x, y be set ; ::_thesis: for A being non empty set
for p being FinSequence of A st x <> y holds
dom ({x} |` (p ^ <*y*>)) = dom ({x} |` p)
let A be non empty set ; ::_thesis: for p being FinSequence of A st x <> y holds
dom ({x} |` (p ^ <*y*>)) = dom ({x} |` p)
let p be FinSequence of A; ::_thesis: ( x <> y implies dom ({x} |` (p ^ <*y*>)) = dom ({x} |` p) )
assume A1: x <> y ; ::_thesis: dom ({x} |` (p ^ <*y*>)) = dom ({x} |` p)
thus  dom ({x} |` (p ^ <*y*>)) c= dom ({x} |` p) :: according to XBOOLE_0:def_10 ::_thesis: dom ({x} |` p) c= dom ({x} |` (p ^ <*y*>))
proof
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in dom ({x} |` (p ^ <*y*>)) or a in dom ({x} |` p) )
A2: len <*y*> = 1 by FINSEQ_1:40;
A3: Seg (len p) = dom p by FINSEQ_1:def_3;
assume A4: a in dom ({x} |` (p ^ <*y*>)) ; ::_thesis: a in dom ({x} |` p)
then A5: a in dom (p ^ <*y*>) by FUNCT_1:54;
then  a in Seg ((len p) + (len <*y*>)) by FINSEQ_1:def_7;
then  a in (Seg (len p)) \/ {((len p) + 1)} by A2, FINSEQ_1:9;
then A6: ( a in dom p or a in {((len p) + 1)} ) by A3, XBOOLE_0:def_3;
A7: (p ^ <*y*>) . a in {x} by A4, FUNCT_1:54;
reconsider a = a as Element of NAT by A5;
A8: ( (p ^ <*y*>) . ((len p) + 1) = y & not y in {x} ) by A1, FINSEQ_1:42, TARSKI:def_1;
then  (p ^ <*y*>) . a = p . a by A7, A6, FINSEQ_1:def_7, TARSKI:def_1;
hence  a in dom ({x} |` p) by A7, A6, A8, FUNCT_1:54, TARSKI:def_1; ::_thesis: verum
end;
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in dom ({x} |` p) or a in dom ({x} |` (p ^ <*y*>)) )
assume A9: a in dom ({x} |` p) ; ::_thesis: a in dom ({x} |` (p ^ <*y*>))
then A10: a in dom p by FUNCT_1:54;
 len <*y*> = 1 by FINSEQ_1:40;
then A11: dom (p ^ <*y*>) = Seg ((len p) + 1) by FINSEQ_1:def_7;
 ( Seg (len p) = dom p & Seg ((len p) + 1) = (Seg (len p)) \/ {((len p) + 1)} ) by FINSEQ_1:9, FINSEQ_1:def_3;
then A12: a in dom (p ^ <*y*>) by A10, A11, XBOOLE_0:def_3;
A13: p . a in {x} by A9, FUNCT_1:54;
reconsider a = a as Element of NAT by A9;
 (p ^ <*y*>) . a = p . a by A10, FINSEQ_1:def_7;
hence  a in dom ({x} |` (p ^ <*y*>)) by A13, A12, FUNCT_1:54; ::_thesis: verum
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
deffunc H4( Element of A) ->  Element of NAT = card (dom ({$1} |` p));
consider m being Function of A,NAT such that
A1: for a being Element of A holds m . a = H4(a) from FUNCT_2:sch_4();
 m is Multiset of A by Th27;
hence  ex b1 being Multiset of A st
for a being Element of A holds b1 . a = card (dom ({a} |` p)) by A1; ::_thesis: verum
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
let m1, m2 be Multiset of A; ::_thesis: ( ( for a being Element of A holds m1 . a = card (dom ({a} |` p)) ) & ( for a being Element of A holds m2 . a = card (dom ({a} |` p)) ) implies m1 = m2 )
assume that
A2: for a being Element of A holds m1 . a = card (dom ({a} |` p)) and
A3: for a being Element of A holds m2 . a = card (dom ({a} |` p)) ; ::_thesis: m1 = m2
now__::_thesis:_for_a_being_Element_of_A_holds_m1_._a_=_m2_._a
let a be Element of A; ::_thesis: m1 . a = m2 . a
thus m1 . a = card (dom ({a} |` p)) by A2
.= m2 . a by A3 ; ::_thesis: verum
end;
hence  m1 = m2 by Th32; ::_thesis: verum
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
let A be non empty set ; ::_thesis: for a being Element of A holds |.(<*> A).| . a = 0
let a be Element of A; ::_thesis: |.(<*> A).| . a = 0
 dom ({a} |` {}) c= dom {} by FUNCT_1:56;
then  dom ({a} |` (<*> A)) = {} ;
hence  |.(<*> A).| . a = 0 by Def7, CARD_1:27; ::_thesis: verum
end;

theorem Th37: :: MONOID_1:37
for A being non empty set holds |.(<*> A).| = A --> 0
proof
let A be non empty set ; ::_thesis: |.(<*> A).| = A --> 0
A1: now__::_thesis:_for_x_being_set_st_x_in_A_holds_
|.(<*>_A).|_._x_=_0
let x be set ; ::_thesis: ( x in A implies |.(<*> A).| . x = 0 )
assume  x in A ; ::_thesis: |.(<*> A).| . x = 0
then reconsider a = x as Element of A ;
thus |.(<*> A).| . x = card (dom ({a} |` {})) by Def7
.= 0 by CARD_1:27, RELAT_1:38, RELAT_1:107 ; ::_thesis: verum
end;
 dom |.(<*> A).| = A by Th28;
hence  |.(<*> A).| = A --> 0 by A1, FUNCOP_1:11; ::_thesis: verum
end;

theorem :: MONOID_1:38
for A being non empty set
for a being Element of A holds |.<*a*>.| = chi a
proof
let A be non empty set ; ::_thesis: for a being Element of A holds |.<*a*>.| = chi a
let a be Element of A; ::_thesis: |.<*a*>.| = chi a
A1: rng <*a*> = {a} by FINSEQ_1:39;
now__::_thesis:_for_b_being_Element_of_A_holds_|.<*a*>.|_._b_=_(chi_a)_._b
let b be Element of A; ::_thesis: |.<*a*>.| . b = (chi a) . b
set x = b;
A2: ( dom <*a*> = Seg 1 & card (Seg 1) = 1 ) by FINSEQ_1:38, FINSEQ_1:57;
 ( a <> b implies {b} misses {a} ) by ZFMISC_1:11;
then A3: ( a <> b implies {b} /\ {a} = {} ) by XBOOLE_0:def_7;
A4: ( (chi a) . a = 1 & {a} |` <*a*> = <*a*> ) by A1, Th31, RELAT_1:94;
 <*a*> = (rng <*a*>) |` <*a*> ;
then  {b} |` <*a*> = ({b} /\ (rng <*a*>)) |` <*a*> by RELAT_1:96;
then  ( b <> a implies ( {b} |` <*a*> = {} & (chi a) . b = 0 ) ) by A1, A3, Th31;
hence  |.<*a*>.| . b = (chi a) . b by A2, A4, Def7, CARD_1:27, RELAT_1:38; ::_thesis: verum
end;
hence  |.<*a*>.| = chi a by Th32; ::_thesis: verum
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
let A be non empty set ; ::_thesis: for a being Element of A
for p being FinSequence of A holds |.(p ^ <*a*>).| = |.p.| [*] (chi a)
let a be Element of A; ::_thesis: for p being FinSequence of A holds |.(p ^ <*a*>).| = |.p.| [*] (chi a)
let p be FinSequence of A; ::_thesis: |.(p ^ <*a*>).| = |.p.| [*] (chi a)
now__::_thesis:_for_b_being_Element_of_A_holds_|.(p_^_<*a*>).|_._b_=_(|.p.|_[*]_(chi_a))_._b
reconsider pa = p ^ <*a*> as FinSequence of A ;
let b be Element of A; ::_thesis: |.(p ^ <*a*>).| . b = (|.p.| [*] (chi a)) . b
 ( len p < (len p) + 1 & dom ({b} |` p) c= dom p ) by FUNCT_1:56, NAT_1:13;
then A1: not (len p) + 1 in dom ({b} |` p) by FINSEQ_3:25;
A2: ( |.(p ^ <*a*>).| . b = card (dom ({b} |` pa)) & |.p.| . b = card (dom ({b} |` p)) ) by Def7;
A3: ( a <> b implies ( dom ({b} |` (p ^ <*a*>)) = dom ({b} |` p) & (chi a) . b = 0 ) ) by Th31, Th35;
A4: (|.p.| [*] (chi a)) . b = (|.p.| . b) + ((chi a) . b) by Th29;
 ( dom ({a} |` (p ^ <*a*>)) = (dom ({a} |` p)) \/ {((len p) + 1)} & (chi a) . a = 1 ) by Th31, Th34;
hence  |.(p ^ <*a*>).| . b = (|.p.| [*] (chi a)) . b by A1, A2, A3, A4, CARD_2:41; ::_thesis: verum
end;
hence  |.(p ^ <*a*>).| = |.p.| [*] (chi a) by Th32; ::_thesis: verum
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
let A be non empty set ; ::_thesis: for p, q being FinSequence of A holds |.(p ^ q).| = |.p.| [*] |.q.|
let p, q be FinSequence of A; ::_thesis: |.(p ^ q).| = |.p.| [*] |.q.|
defpred S1[ Element of NAT ] means  for q being FinSequence of A st len q = $1 holds
|.(p ^ q).| = |.p.| [*] |.q.|;
A1: len q = len q ;
A2: for n being Element of NAT st S1[n] holds
S1[n + 1]
proof
let n be Element of NAT ; ::_thesis: ( S1[n] implies S1[n + 1] )
assume A3: for q being FinSequence of A st len q = n holds
|.(p ^ q).| = |.p.| [*] |.q.| ; ::_thesis: S1[n + 1]
let q be FinSequence of A; ::_thesis: ( len q = n + 1 implies |.(p ^ q).| = |.p.| [*] |.q.| )
assume A4: len q = n + 1 ; ::_thesis: |.(p ^ q).| = |.p.| [*] |.q.|
then  q <> {} ;
then consider r being FinSequence, x being set  such that
A5: q = r ^ <*x*> by FINSEQ_1:46;
 rng <*x*> = {x} by FINSEQ_1:39;
then  {x} c= rng q by A5, FINSEQ_1:30;
then A6: {x} c= A by XBOOLE_1:1;
reconsider r = r as FinSequence of A by A5, FINSEQ_1:36;
 len <*x*> = 1 by FINSEQ_1:40;
then A7: n + 1 = (len r) + 1 by A4, A5, FINSEQ_1:22;
reconsider x = x as Element of A by A6, ZFMISC_1:31;
thus |.(p ^ q).| = |.((p ^ r) ^ <*x*>).| by A5, FINSEQ_1:32
.= |.(p ^ r).| [*] (chi x) by Th39
.= (|.p.| [*] |.r.|) [*] (chi x) by A3, A7
.= |.p.| [*] (|.r.| [*] (chi x)) by GROUP_1:def_3
.= |.p.| [*] |.q.| by A5, Th39 ; ::_thesis: verum
end;
A8: S1[ 0 ]
proof
let q be FinSequence of A; ::_thesis: ( len q = 0 implies |.(p ^ q).| = |.p.| [*] |.q.| )
A9: ( |.(<*> A).| = A --> 0 & A --> 0 = H2( MultiSet_over A) ) by Th26, Th37;
assume  len q = 0 ; ::_thesis: |.(p ^ q).| = |.p.| [*] |.q.|
then A10: q = {} ;
then  p ^ q = p by FINSEQ_1:34;
hence  |.(p ^ q).| = |.p.| [*] |.q.| by A10, A9, MONOID_0:16; ::_thesis: verum
end;
 for n being Element of NAT holds S1[n] from NAT_1:sch_1(A8, A2);
hence  |.(p ^ q).| = |.p.| [*] |.q.| by A1; ::_thesis: verum
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
let n be Element of NAT ; ::_thesis: 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 ) )
let A be non empty set ; ::_thesis: 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 ) )
let a be Element of A; ::_thesis: ( |.(n .--> a).| . a = n & ( for b being Element of A st b <> a holds
|.(n .--> a).| . b = 0 ) )
defpred S1[ Element of NAT ] means |.($1 .--> a).| . a = $1;
A1: ( 0 .--> a = {} & {} = <*> A ) by FINSEQ_2:58;
A2: for n being Element of NAT st S1[n] holds
S1[n + 1]
proof
let n be Element of NAT ; ::_thesis: ( S1[n] implies S1[n + 1] )
assume A3: |.(n .--> a).| . a = n ; ::_thesis: S1[n + 1]
thus |.((n + 1) .--> a).| . a = |.((n .--> a) ^ <*a*>).| . a by FINSEQ_2:60
.= (|.(n .--> a).| [*] (chi a)) . a by Th39
.= n + ((chi a) . a) by A3, Th29
.= n + 1 by Th31 ; ::_thesis: verum
end;
 (A --> 0) . a = 0 by FUNCOP_1:7;
then A4: S1[ 0 ] by A1, Th37;
 for n being Element of NAT holds S1[n] from NAT_1:sch_1(A4, A2);
hence  |.(n .--> a).| . a = n ; ::_thesis: for b being Element of A st b <> a holds
|.(n .--> a).| . b = 0
let b be Element of A; ::_thesis: ( b <> a implies |.(n .--> a).| . b = 0 )
assume A5: b <> a ; ::_thesis: |.(n .--> a).| . b = 0
defpred S2[ Element of NAT ] means |.($1 .--> a).| . b = 0 ;
A6: for n being Element of NAT st S2[n] holds
S2[n + 1]
proof
let n be Element of NAT ; ::_thesis: ( S2[n] implies S2[n + 1] )
assume A7: |.(n .--> a).| . b = 0 ; ::_thesis: S2[n + 1]
thus |.((n + 1) .--> a).| . b = |.((n .--> a) ^ <*a*>).| . b by FINSEQ_2:60
.= (|.(n .--> a).| [*] (chi a)) . b by Th39
.= 0 + ((chi a) . b) by A7, Th29
.= 0 by A5, Th31 ; ::_thesis: verum
end;
 (A --> 0) . b = 0 by FUNCOP_1:7;
then A8: S2[ 0 ] by A1, Th37;
 for n being Element of NAT holds S2[n] from NAT_1:sch_1(A8, A6);
hence  |.(n .--> a).| . b = 0 ; ::_thesis: verum
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
let A be non empty set ; ::_thesis: for p being FinSequence of A holds |.p.| is Element of (finite-MultiSet_over A)
let p be FinSequence of A; ::_thesis: |.p.| is Element of (finite-MultiSet_over A)
defpred S1[ FinSequence of A] means |.$1.| is Element of (finite-MultiSet_over A);
defpred S2[ Element of NAT ] means  for p being FinSequence of A st len p = $1 holds
S1[p];
A1: len p = len p ;
A2: for n being Element of NAT st S2[n] holds
S2[n + 1]
proof
set M = finite-MultiSet_over A;
let n be Element of NAT ; ::_thesis: ( S2[n] implies S2[n + 1] )
assume A3: for p being FinSequence of A st len p = n holds
S1[p] ; ::_thesis: S2[n + 1]
let p be FinSequence of A; ::_thesis: ( len p = n + 1 implies S1[p] )
assume A4: len p = n + 1 ; ::_thesis: S1[p]
then  p <> {} ;
then consider r being FinSequence, x being set  such that
A5: p = r ^ <*x*> by FINSEQ_1:46;
 rng <*x*> = {x} by FINSEQ_1:39;
then  {x} c= rng p by A5, FINSEQ_1:30;
then A6: {x} c= A by XBOOLE_1:1;
reconsider r = r as FinSequence of A by A5, FINSEQ_1:36;
A7: len <*x*> = 1 by FINSEQ_1:40;
reconsider x = x as Element of A by A6, ZFMISC_1:31;
 n + 1 = (len r) + 1 by A4, A5, A7, FINSEQ_1:22;
then reconsider r9 = |.r.|, a = chi x as Element of (finite-MultiSet_over A) by A3, Th33;
 finite-MultiSet_over A is SubStr of MultiSet_over A by MONOID_0:21;
then r9 [*] a = |.r.| [*] (chi x) by MONOID_0:25
.= |.p.| by A5, Th39 ;
hence  S1[p] ; ::_thesis: verum
end;
A8: S2[ 0 ]
proof
let p be FinSequence of A; ::_thesis: ( len p = 0 implies S1[p] )
assume  len p = 0 ; ::_thesis: S1[p]
then  p = <*> A ;
then |.p.| = A --> 0 by Th37
.= H2( MultiSet_over A) by Th26
.= H2( finite-MultiSet_over A) by MONOID_0:def_24 ;
hence  S1[p] ; ::_thesis: verum
end;
 for n being Element of NAT holds S2[n] from NAT_1:sch_1(A8, A2);
hence  |.p.| is Element of (finite-MultiSet_over A) by A1; ::_thesis: verum
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
let x be set ; ::_thesis: 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.|
let A be non empty set ; ::_thesis: ( x is Element of (finite-MultiSet_over A) implies ex p being FinSequence of A st x = |.p.| )
defpred S1[ Element of NAT ] means  for fm being Element of (finite-MultiSet_over A) st ( for V being finite set st V = fm " (NAT \ {0}) holds
card V = $1 ) holds
ex p being FinSequence of A st fm = |.p.|;
assume  x is Element of (finite-MultiSet_over A) ; ::_thesis: ex p being FinSequence of A st x = |.p.|
then reconsider m = x as Element of (finite-MultiSet_over A) ;
 H3( finite-MultiSet_over A) c= H3( MultiSet_over A) by MONOID_0:23;
then  m is Multiset of A by TARSKI:def_3;
then reconsider V = m " (NAT \ {0}) as finite set by Def6;
A1: for V9 being finite set st V9 = m " (NAT \ {0}) holds
card V9 = card V ;
A2: for n being Element of NAT st S1[n] holds
S1[n + 1]
proof
deffunc H4( set ) ->  Element of NAT = 0 ;
let n be Element of NAT ; ::_thesis: ( S1[n] implies S1[n + 1] )
assume A3: for fm being Element of (finite-MultiSet_over A) st ( for V being finite set st V = fm " (NAT \ {0}) holds
card V = n ) holds
ex p being FinSequence of A st fm = |.p.| ; ::_thesis: S1[n + 1]
let fm be Element of (finite-MultiSet_over A); ::_thesis: ( ( for V being finite set st V = fm " (NAT \ {0}) holds
card V = n + 1 ) implies ex p being FinSequence of A st fm = |.p.| )
assume A4: for V being finite set st V = fm " (NAT \ {0}) holds
card V = n + 1 ; ::_thesis: ex p being FinSequence of A st fm = |.p.|
deffunc H5( set ) ->  set = fm . $1;
set x = the Element of fm " (NAT \ {0});
 H3( finite-MultiSet_over A) c= H3( MultiSet_over A) by MONOID_0:23;
then reconsider m = fm as Multiset of A by TARSKI:def_3;
reconsider V = m " (NAT \ {0}) as finite set by Def6;
A5: card V = n + 1 by A4;
A6: dom m = A by Th28;
then reconsider x = the Element of fm " (NAT \ {0}) as Element of A by A5, CARD_1:27, FUNCT_1:def_7;
defpred S2[ set ] means x = $1;
consider f being Function such that
A7: ( dom f = A & ( for a being set st a in A holds
( ( S2[a] implies f . a = H4(a) ) & ( not S2[a] implies f . a = H5(a) ) ) ) ) from PARTFUN1:sch_1();
 rng f c= NAT
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in rng f or y in NAT )
assume  y in rng f ; ::_thesis: y in NAT
then consider z being set  such that
A8: z in dom f and
A9: y = f . z by FUNCT_1:def_3;
reconsider z = z as Element of A by A7, A8;
 ( y = 0 or y = m . z ) by A7, A9;
hence  y in NAT ; ::_thesis: verum
end;
then reconsider f = f as Function of A,NAT by A7, FUNCT_2:def_1, RELSET_1:4;
reconsider f = f as Multiset of A by Th27;
A10: f " (NAT \ {0}) = (fm " (NAT \ {0})) \ {x}
proof
thus  f " (NAT \ {0}) c= (fm " (NAT \ {0})) \ {x} :: according to XBOOLE_0:def_10 ::_thesis: (fm " (NAT \ {0})) \ {x} c= f " (NAT \ {0})
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in f " (NAT \ {0}) or y in (fm " (NAT \ {0})) \ {x} )
assume A11: y in f " (NAT \ {0}) ; ::_thesis: y in (fm " (NAT \ {0})) \ {x}
then reconsider a = y as Element of A by A7, FUNCT_1:def_7;
A12: f . y in NAT \ {0} by A11, FUNCT_1:def_7;
then  not f . a in {0} by XBOOLE_0:def_5;
then A13: f . a <> 0 by TARSKI:def_1;
then  a <> x by A7;
then A14: not a in {x} by TARSKI:def_1;
 f . a = fm . a by A7, A13;
then  a in fm " (NAT \ {0}) by A6, A12, FUNCT_1:def_7;
hence  y in (fm " (NAT \ {0})) \ {x} by A14, XBOOLE_0:def_5; ::_thesis: verum
end;
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in (fm " (NAT \ {0})) \ {x} or y in f " (NAT \ {0}) )
assume A15: y in (fm " (NAT \ {0})) \ {x} ; ::_thesis: y in f " (NAT \ {0})
then A16: y in dom fm by FUNCT_1:def_7;
A17: fm . y in NAT \ {0} by A15, FUNCT_1:def_7;
 not y in {x} by A15, XBOOLE_0:def_5;
then  y <> x by TARSKI:def_1;
then  fm . y = f . y by A6, A7, A16;
hence  y in f " (NAT \ {0}) by A6, A7, A16, A17, FUNCT_1:def_7; ::_thesis: verum
end;
then reconsider f9 = f as Element of (finite-MultiSet_over A) by A5, Def6;
set g = |.((m . x) .--> x).|;
A18: card {x} = 1 by CARD_1:30;
reconsider V9 = f9 " (NAT \ {0}) as finite set by Def6;
 {x} c= fm " (NAT \ {0}) by A5, CARD_1:27, ZFMISC_1:31;
then  card V9 = (n + 1) - 1 by A5, A10, A18, CARD_2:44
.= n ;
then  for V being finite set st V = f9 " (NAT \ {0}) holds
card V = n ;
then consider p being FinSequence of A such that
A19: f = |.p.| by A3;
take q = p ^ ((m . x) .--> x); ::_thesis: fm = |.q.|
now__::_thesis:_for_a_being_Element_of_A_holds_(f_[*]_|.((m_._x)_.-->_x).|)_._a_=_m_._a
let a be Element of A; ::_thesis: (f [*] |.((m . x) .--> x).|) . a = m . a
A20: 0 + (m . a) = m . a ;
A21: ( a <> x implies ( f . a = m . a & |.((m . x) .--> x).| . a = 0 ) ) by A7, Th41;
 ( f . x = 0 & |.((m . x) .--> x).| . x = m . x ) by A7, Th41;
hence  (f [*] |.((m . x) .--> x).|) . a = m . a by A20, A21, Th29; ::_thesis: verum
end;
hence fm = f [*] |.((m . x) .--> x).| by Th32
.= |.q.| by A19, Th40 ;
::_thesis: verum
end;
A22: S1[ 0 ]
proof
set a = the Element of A;
let fm be Element of (finite-MultiSet_over A); ::_thesis: ( ( for V being finite set st V = fm " (NAT \ {0}) holds
card V = 0 ) implies ex p being FinSequence of A st fm = |.p.| )
assume A23: for V being finite set st V = fm " (NAT \ {0}) holds
card V = 0 ; ::_thesis: ex p being FinSequence of A st fm = |.p.|
 H3( finite-MultiSet_over A) c= H3( MultiSet_over A) by MONOID_0:23;
then reconsider m = fm as Multiset of A by TARSKI:def_3;
reconsider V = m " (NAT \ {0}) as finite set by Def6;
 card V = 0 by A23;
then  fm " (NAT \ {0}) = {} ;
then  rng fm misses NAT \ {0} by RELAT_1:138;
then A24: {} = (rng fm) /\ (NAT \ {0}) by XBOOLE_0:def_7
.= ((rng fm) /\ NAT) \ {0} by XBOOLE_1:49 ;
take p = <*> A; ::_thesis: fm = |.p.|
 rng m c= NAT ;
then  (rng fm) /\ NAT = rng fm by XBOOLE_1:28;
then A25: rng fm c= {0} by A24, XBOOLE_1:37;
A26: dom m = A by Th28;
then A27: fm . the Element of A in rng fm by FUNCT_1:def_3;
then  fm . the Element of A = 0 by A25, TARSKI:def_1;
then  {0} c= rng fm by A27, ZFMISC_1:31;
then  rng fm = {0} by A25, XBOOLE_0:def_10;
hence fm = A --> 0 by A26, FUNCOP_1:9
.= |.p.| by Th37 ;
::_thesis: verum
end;
 for n being Element of NAT holds S1[n] from NAT_1:sch_1(A22, A2);
hence  ex p being FinSequence of A st x = |.p.| by A1; ::_thesis: verum
end;

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):]
proof
deffunc H4( Element of [:(bool D1),(bool D2):]) ->  Element of bool D = f .: [:($1 `1),($1 `2):];
 ex f being Function of [:(bool D1),(bool D2):],(bool D) st
for x being Element of [:(bool D1),(bool D2):] holds f . x = H4(x) from FUNCT_2:sch_4();
hence  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):] ; ::_thesis: verum
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
let F1, F2 be Function of [:(bool D1),(bool D2):],(bool D); ::_thesis: ( ( for x being Element of [:(bool D1),(bool D2):] holds F1 . x = f .: [:(x `1),(x `2):] ) & ( for x being Element of [:(bool D1),(bool D2):] holds F2 . x = f .: [:(x `1),(x `2):] ) implies F1 = F2 )
assume that
A1: for x being Element of [:(bool D1),(bool D2):] holds F1 . x = f .: [:(x `1),(x `2):] and
A2: for x being Element of [:(bool D1),(bool D2):] holds F2 . x = f .: [:(x `1),(x `2):] ; ::_thesis: F1 = F2
now__::_thesis:_for_x_being_Element_of_[:(bool_D1),(bool_D2):]_holds_F1_._x_=_F2_._x
let x be Element of [:(bool D1),(bool D2):]; ::_thesis: F1 . x = F2 . x
thus F1 . x = f .: [:(x `1),(x `2):] by A1
.= F2 . x by A2 ; ::_thesis: verum
end;
hence  F1 = F2 by FUNCT_2:63; ::_thesis: verum
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
let D1, D2, D be non empty set ; ::_thesis: 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:]
let f be Function of [:D1,D2:],D; ::_thesis: for X1 being Subset of D1
for X2 being Subset of D2 holds (f .:^2) . (X1,X2) = f .: [:X1,X2:]
let X1 be Subset of D1; ::_thesis: for X2 being Subset of D2 holds (f .:^2) . (X1,X2) = f .: [:X1,X2:]
let X2 be Subset of D2; ::_thesis: (f .:^2) . (X1,X2) = f .: [:X1,X2:]
 ( [X1,X2] `1 = X1 & [X1,X2] `2 = X2 ) by MCART_1:7;
hence  (f .:^2) . (X1,X2) = f .: [:X1,X2:] by Def8; ::_thesis: verum
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
let D1, D2, D be non empty set ; ::_thesis: 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)
let f be Function of [:D1,D2:],D; ::_thesis: 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)
let X1 be Subset of D1; ::_thesis: 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)
let X2 be Subset of D2; ::_thesis: for x1, x2 being set st x1 in X1 & x2 in X2 holds
f . (x1,x2) in (f .:^2) . (X1,X2)
let x1, x2 be set ; ::_thesis: ( x1 in X1 & x2 in X2 implies f . (x1,x2) in (f .:^2) . (X1,X2) )
assume that
A1: x1 in X1 and
A2: x2 in X2 ; ::_thesis: f . (x1,x2) in (f .:^2) . (X1,X2)
reconsider b = x2 as Element of D2 by A2;
reconsider a = x1 as Element of D1 by A1;
A3: ( (f .:^2) . (X1,X2) = f .: [:X1,X2:] & dom f = [:D1,D2:] ) by Th44, FUNCT_2:def_1;
 [a,b] in [:X1,X2:] by A1, A2, ZFMISC_1:87;
hence  f . (x1,x2) in (f .:^2) . (X1,X2) by A3, FUNCT_1:def_6; ::_thesis: verum
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
let D1, D2, D be non empty set ; ::_thesis: 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 )  }
let f be Function of [:D1,D2:],D; ::_thesis: 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 )  }
let X1 be Subset of D1; ::_thesis: 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 )  }
let X2 be Subset of D2; ::_thesis: (f .:^2) . (X1,X2) =  {  (f . (a,b)) where a is Element of D1, b is Element of D2 : ( a in X1 & b in X2 )  }
set A =  {  (f . (a,b)) where a is Element of D1, b is Element of D2 : ( a in X1 & b in X2 )  }  ;
A1: (f .:^2) . (X1,X2) = f .: [:X1,X2:] by Th44;
thus  (f .:^2) . (X1,X2) c=  {  (f . (a,b)) where a is Element of D1, b is Element of D2 : ( a in X1 & b in X2 )  }  :: according to XBOOLE_0:def_10 ::_thesis:  {  (f . (a,b)) where a is Element of D1, b is Element of D2 : ( a in X1 & b in X2 )  }  c= (f .:^2) . (X1,X2)
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in (f .:^2) . (X1,X2) or x in  {  (f . (a,b)) where a is Element of D1, b is Element of D2 : ( a in X1 & b in X2 )  }  )
assume  x in (f .:^2) . (X1,X2) ; ::_thesis: x in  {  (f . (a,b)) where a is Element of D1, b is Element of D2 : ( a in X1 & b in X2 )  }
then consider y being set  such that
 y in dom f and
A2: y in [:X1,X2:] and
A3: x = f . y by A1, FUNCT_1:def_6;
consider y1, y2 being set  such that
A4: y1 in X1 and
A5: y2 in X2 and
A6: y = [y1,y2] by A2, ZFMISC_1:84;
reconsider y2 = y2 as Element of D2 by A5;
reconsider y1 = y1 as Element of D1 by A4;
 x = f . (y1,y2) by A3, A6;
hence  x in  {  (f . (a,b)) where a is Element of D1, b is Element of D2 : ( a in X1 & b in X2 )  }  by A4, A5; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in  {  (f . (a,b)) where a is Element of D1, b is Element of D2 : ( a in X1 & b in X2 )  }  or x in (f .:^2) . (X1,X2) )
assume  x in  {  (f . (a,b)) where a is Element of D1, b is Element of D2 : ( a in X1 & b in X2 )  }  ; ::_thesis: x in (f .:^2) . (X1,X2)
then  ex a being Element of D1 ex b being Element of D2 st
( x = f . (a,b) & a in X1 & b in X2 ) ;
hence  x in (f .:^2) . (X1,X2) by Th45; ::_thesis: verum
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
let X, Y be set ; ::_thesis: for D being non empty set
for o being BinOp of D st o is commutative holds
o .: [:X,Y:] = o .: [:Y,X:]
let D be non empty set ; ::_thesis: for o being BinOp of D st o is commutative holds
o .: [:X,Y:] = o .: [:Y,X:]
let o be BinOp of D; ::_thesis: ( o is commutative implies o .: [:X,Y:] = o .: [:Y,X:] )
assume A1: for a, b being Element of D holds o . (a,b) = o . (b,a) ; :: according to BINOP_1:def_2 ::_thesis: o .: [:X,Y:] = o .: [:Y,X:]
now__::_thesis:_for_X,_Y_being_set_holds_o_.:_[:X,Y:]_c=_o_.:_[:Y,X:]
let X, Y be set ; ::_thesis: o .: [:X,Y:] c= o .: [:Y,X:]
thus  o .: [:X,Y:] c= o .: [:Y,X:] ::_thesis: verum
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in o .: [:X,Y:] or x in o .: [:Y,X:] )
assume  x in o .: [:X,Y:] ; ::_thesis: x in o .: [:Y,X:]
then consider y being set  such that
A2: y in dom o and
A3: y in [:X,Y:] and
A4: x = o . y by FUNCT_1:def_6;
reconsider y = y as Element of [:D,D:] by A2;
 y = [(y `1),(y `2)] by MCART_1:21;
then  ( y `1 in X & y `2 in Y ) by A3, ZFMISC_1:87;
then A5: [(y `2),(y `1)] in [:Y,X:] by ZFMISC_1:87;
A6: ( dom o = [:D,D:] & o . ((y `1),(y `2)) = o . ((y `2),(y `1)) ) by A1, FUNCT_2:def_1;
 x = o . ((y `1),(y `2)) by A4, MCART_1:21;
hence  x in o .: [:Y,X:] by A6, A5, FUNCT_1:def_6; ::_thesis: verum
end;
end;
hence  ( o .: [:X,Y:] c= o .: [:Y,X:] & o .: [:Y,X:] c= o .: [:X,Y:] ) ; :: according to XBOOLE_0:def_10 ::_thesis: verum
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
let X, Y, Z be set ; ::_thesis: 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:]):]
let D be non empty set ; ::_thesis: for o being BinOp of D st o is associative holds
o .: [:(o .: [:X,Y:]),Z:] = o .: [:X,(o .: [:Y,Z:]):]
let o be BinOp of D; ::_thesis: ( o is associative implies o .: [:(o .: [:X,Y:]),Z:] = o .: [:X,(o .: [:Y,Z:]):] )
A1: dom o = [:D,D:] by FUNCT_2:def_1;
assume A2: for a, b, c being Element of D holds o . ((o . (a,b)),c) = o . (a,(o . (b,c))) ; :: according to BINOP_1:def_3 ::_thesis: o .: [:(o .: [:X,Y:]),Z:] = o .: [:X,(o .: [:Y,Z:]):]
thus  o .: [:(o .: [:X,Y:]),Z:] c= o .: [:X,(o .: [:Y,Z:]):] :: according to XBOOLE_0:def_10 ::_thesis: o .: [:X,(o .: [:Y,Z:]):] c= o .: [:(o .: [:X,Y:]),Z:]
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in o .: [:(o .: [:X,Y:]),Z:] or x in o .: [:X,(o .: [:Y,Z:]):] )
assume  x in o .: [:(o .: [:X,Y:]),Z:] ; ::_thesis: x in o .: [:X,(o .: [:Y,Z:]):]
then consider y being set  such that
A3: y in dom o and
A4: y in [:(o .: [:X,Y:]),Z:] and
A5: x = o . y by FUNCT_1:def_6;
reconsider y = y as Element of [:D,D:] by A3;
A6: y = [(y `1),(y `2)] by MCART_1:21;
then A7: y `2 in Z by A4, ZFMISC_1:87;
 y `1 in o .: [:X,Y:] by A4, A6, ZFMISC_1:87;
then consider z being set  such that
A8: z in dom o and
A9: z in [:X,Y:] and
A10: y `1 = o . z by FUNCT_1:def_6;
reconsider z = z as Element of [:D,D:] by A8;
A11: y `1 = o . ((z `1),(z `2)) by A10, MCART_1:21;
A12: z = [(z `1),(z `2)] by MCART_1:21;
then  z `2 in Y by A9, ZFMISC_1:87;
then  [(z `2),(y `2)] in [:Y,Z:] by A7, ZFMISC_1:87;
then A13: o . ((z `2),(y `2)) in o .: [:Y,Z:] by A1, FUNCT_1:def_6;
 z `1 in X by A9, A12, ZFMISC_1:87;
then A14: [(z `1),(o . ((z `2),(y `2)))] in [:X,(o .: [:Y,Z:]):] by A13, ZFMISC_1:87;
 x = o . ((y `1),(y `2)) by A5, MCART_1:21;
then  x = o . ((z `1),(o . ((z `2),(y `2)))) by A2, A11;
hence  x in o .: [:X,(o .: [:Y,Z:]):] by A1, A14, FUNCT_1:def_6; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in o .: [:X,(o .: [:Y,Z:]):] or x in o .: [:(o .: [:X,Y:]),Z:] )
assume  x in o .: [:X,(o .: [:Y,Z:]):] ; ::_thesis: x in o .: [:(o .: [:X,Y:]),Z:]
then consider y being set  such that
A15: y in dom o and
A16: y in [:X,(o .: [:Y,Z:]):] and
A17: x = o . y by FUNCT_1:def_6;
reconsider y = y as Element of [:D,D:] by A15;
A18: y = [(y `1),(y `2)] by MCART_1:21;
then A19: y `1 in X by A16, ZFMISC_1:87;
 y `2 in o .: [:Y,Z:] by A16, A18, ZFMISC_1:87;
then consider z being set  such that
A20: z in dom o and
A21: z in [:Y,Z:] and
A22: y `2 = o . z by FUNCT_1:def_6;
reconsider z = z as Element of [:D,D:] by A20;
A23: y `2 = o . ((z `1),(z `2)) by A22, MCART_1:21;
A24: z = [(z `1),(z `2)] by MCART_1:21;
then  z `1 in Y by A21, ZFMISC_1:87;
then  [(y `1),(z `1)] in [:X,Y:] by A19, ZFMISC_1:87;
then A25: o . ((y `1),(z `1)) in o .: [:X,Y:] by A1, FUNCT_1:def_6;
 z `2 in Z by A21, A24, ZFMISC_1:87;
then A26: [(o . ((y `1),(z `1))),(z `2)] in [:(o .: [:X,Y:]),Z:] by A25, ZFMISC_1:87;
 x = o . ((y `1),(y `2)) by A17, MCART_1:21;
then  x = o . ((o . ((y `1),(z `1))),(z `2)) by A2, A23;
hence  x in o .: [:(o .: [:X,Y:]),Z:] by A1, A26, FUNCT_1:def_6; ::_thesis: verum
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
let D be non empty set ; ::_thesis: for o being BinOp of D st o is commutative holds
o .:^2 is commutative
let o be BinOp of D; ::_thesis: ( o is commutative implies o .:^2 is commutative )
assume A1: o is commutative ; ::_thesis: o .:^2 is commutative
let x, y be Subset of D; :: according to BINOP_1:def_2 ::_thesis: (o .:^2) . (x,y) = (o .:^2) . (y,x)
thus (o .:^2) . (x,y) = o .: [:x,y:] by Th44
.= o .: [:y,x:] by A1, Th47
.= (o .:^2) . (y,x) by Th44 ; ::_thesis: verum
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
let D be non empty set ; ::_thesis: for o being BinOp of D st o is associative holds
o .:^2 is associative
let o be BinOp of D; ::_thesis: ( o is associative implies o .:^2 is associative )
assume A1: o is associative ; ::_thesis: o .:^2 is associative
let x, y, z be Subset of D; :: according to BINOP_1:def_3 ::_thesis: (o .:^2) . (x,((o .:^2) . (y,z))) = (o .:^2) . (((o .:^2) . (x,y)),z)
thus (o .:^2) . (((o .:^2) . (x,y)),z) = (o .:^2) . ((o .: [:x,y:]),z) by Th44
.= o .: [:(o .: [:x,y:]),z:] by Th44
.= o .: [:x,(o .: [:y,z:]):] by A1, Th48
.= (o .:^2) . (x,(o .: [:y,z:])) by Th44
.= (o .:^2) . (x,((o .:^2) . (y,z))) by Th44 ; ::_thesis: verum
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
let X be set ; ::_thesis: 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 )
let D be non empty set ; ::_thesis: 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 )
let o be BinOp of D; ::_thesis: for a being Element of D st a is_a_unity_wrt o holds
( o .: [:{a},X:] = D /\ X & o .: [:X,{a}:] = D /\ X )
let a be Element of D; ::_thesis: ( a is_a_unity_wrt o implies ( o .: [:{a},X:] = D /\ X & o .: [:X,{a}:] = D /\ X ) )
assume A1: a is_a_unity_wrt o ; ::_thesis: ( o .: [:{a},X:] = D /\ X & o .: [:X,{a}:] = D /\ X )
thus  o .: [:{a},X:] c= D /\ X :: according to XBOOLE_0:def_10 ::_thesis: ( D /\ X c= o .: [:{a},X:] & o .: [:X,{a}:] = D /\ X )
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in o .: [:{a},X:] or x in D /\ X )
assume  x in o .: [:{a},X:] ; ::_thesis: x in D /\ X
then consider y being set  such that
A2: y in dom o and
A3: y in [:{a},X:] and
A4: x = o . y by FUNCT_1:def_6;
reconsider y = y as Element of [:D,D:] by A2;
A5: x = o . ((y `1),(y `2)) by A4, MCART_1:21;
A6: y = [(y `1),(y `2)] by MCART_1:21;
then  y `1 in {a} by A3, ZFMISC_1:87;
then A7: y `1 = a by TARSKI:def_1;
A8: o . (a,(y `2)) = y `2 by A1, BINOP_1:3;
 y `2 in X by A3, A6, ZFMISC_1:87;
hence  x in D /\ X by A5, A8, A7, XBOOLE_0:def_4; ::_thesis: verum
end;
A9: dom o = [:D,D:] by FUNCT_2:def_1;
thus  D /\ X c= o .: [:{a},X:] ::_thesis: o .: [:X,{a}:] = D /\ X
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in D /\ X or x in o .: [:{a},X:] )
A10: a in {a} by TARSKI:def_1;
assume A11: x in D /\ X ; ::_thesis: x in o .: [:{a},X:]
then reconsider d = x as Element of D by XBOOLE_0:def_4;
A12: x = o . (a,d) by A1, BINOP_1:3
.= o . [a,x] ;
 x in X by A11, XBOOLE_0:def_4;
then  [a,d] in [:{a},X:] by A10, ZFMISC_1:87;
hence  x in o .: [:{a},X:] by A9, A12, FUNCT_1:def_6; ::_thesis: verum
end;
thus  o .: [:X,{a}:] c= D /\ X :: according to XBOOLE_0:def_10 ::_thesis: D /\ X c= o .: [:X,{a}:]
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in o .: [:X,{a}:] or x in D /\ X )
assume  x in o .: [:X,{a}:] ; ::_thesis: x in D /\ X
then consider y being set  such that
A13: y in dom o and
A14: y in [:X,{a}:] and
A15: x = o . y by FUNCT_1:def_6;
reconsider y = y as Element of [:D,D:] by A13;
A16: x = o . ((y `1),(y `2)) by A15, MCART_1:21;
A17: y = [(y `1),(y `2)] by MCART_1:21;
then  y `2 in {a} by A14, ZFMISC_1:87;
then A18: y `2 = a by TARSKI:def_1;
A19: o . ((y `1),a) = y `1 by A1, BINOP_1:3;
 y `1 in X by A14, A17, ZFMISC_1:87;
hence  x in D /\ X by A16, A19, A18, XBOOLE_0:def_4; ::_thesis: verum
end;
thus  D /\ X c= o .: [:X,{a}:] ::_thesis: verum
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in D /\ X or x in o .: [:X,{a}:] )
A20: a in {a} by TARSKI:def_1;
assume A21: x in D /\ X ; ::_thesis: x in o .: [:X,{a}:]
then reconsider d = x as Element of D by XBOOLE_0:def_4;
A22: x = o . (d,a) by A1, BINOP_1:3
.= o . [x,a] ;
 x in X by A21, XBOOLE_0:def_4;
then  [d,a] in [:X,{a}:] by A20, ZFMISC_1:87;
hence  x in o .: [:X,{a}:] by A9, A22, FUNCT_1:def_6; ::_thesis: verum
end;
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
let D be non empty set ; ::_thesis: 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} )
let o be BinOp of D; ::_thesis: 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} )
let a be Element of D; ::_thesis: ( a is_a_unity_wrt o implies ( {a} is_a_unity_wrt o .:^2 & o .:^2 is having_a_unity & the_unity_wrt (o .:^2) = {a} ) )
assume A1: a is_a_unity_wrt o ; ::_thesis: ( {a} is_a_unity_wrt o .:^2 & o .:^2 is having_a_unity & the_unity_wrt (o .:^2) = {a} )
now__::_thesis:_for_x_being_Subset_of_D_holds_
(_(o_.:^2)_._({a},x)_=_x_&_(o_.:^2)_._(x,{a})_=_x_)
let x be Subset of D; ::_thesis: ( (o .:^2) . ({a},x) = x & (o .:^2) . (x,{a}) = x )
thus (o .:^2) . ({a},x) = o .: [:{a},x:] by Th44
.= D /\ x by A1, Th51
.= x by XBOOLE_1:28 ; ::_thesis: (o .:^2) . (x,{a}) = x
thus (o .:^2) . (x,{a}) = o .: [:x,{a}:] by Th44
.= D /\ x by A1, Th51
.= x by XBOOLE_1:28 ; ::_thesis: verum
end;
hence A2: {a} is_a_unity_wrt o .:^2 by BINOP_1:3; ::_thesis: ( o .:^2 is having_a_unity & the_unity_wrt (o .:^2) = {a} )
hence  ex A being Subset of D st A is_a_unity_wrt o .:^2 ; :: according to SETWISEO:def_2 ::_thesis: the_unity_wrt (o .:^2) = {a}
thus  the_unity_wrt (o .:^2) = {a} by A2, BINOP_1:def_8; ::_thesis: verum
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
let D be non empty set ; ::_thesis: 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)} )
let o be BinOp of D; ::_thesis: ( o is having_a_unity implies ( 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)} ) )
given a being Element of D such that A1: a is_a_unity_wrt o ; :: according to SETWISEO:def_2 ::_thesis: ( 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)} )
 a = the_unity_wrt o by A1, BINOP_1:def_8;
hence  ( 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)} ) by A1, Th52; ::_thesis: verum
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
let D be non empty set ; ::_thesis: for o being BinOp of D st o is uniquely-decomposable holds
o .:^2 is uniquely-decomposable
let o be BinOp of D; ::_thesis: ( o is uniquely-decomposable implies o .:^2 is uniquely-decomposable )
assume that
A1: o is having_a_unity and
A2: for a, b being Element of D st o . (a,b) = the_unity_wrt o holds
( a = b & b = the_unity_wrt o ) ; :: according to MONOID_0:def_9 ::_thesis: o .:^2 is uniquely-decomposable
thus  o .:^2 is having_a_unity by A1, Th53; :: according to MONOID_0:def_9 ::_thesis: for b1, b2 being Element of bool D holds
( not (o .:^2) . (b1,b2) = the_unity_wrt (o .:^2) or ( b1 = b2 & b2 = the_unity_wrt (o .:^2) ) )
let A, B be Subset of D; ::_thesis: ( not (o .:^2) . (A,B) = the_unity_wrt (o .:^2) or ( A = B & B = the_unity_wrt (o .:^2) ) )
assume A3: (o .:^2) . (A,B) = the_unity_wrt (o .:^2) ; ::_thesis: ( A = B & B = the_unity_wrt (o .:^2) )
set a = the_unity_wrt o;
A4: the_unity_wrt (o .:^2) = {(the_unity_wrt o)} by A1, Th53;
set a1 = the Element of A;
set a2 = the Element of B;
 o .: [:A,B:] = (o .:^2) . (A,B) by Th44;
then  dom o meets [:A,B:] by A3, A4, RELAT_1:118;
then  (dom o) /\ [:A,B:] <> {} by XBOOLE_0:def_7;
then A5: [:A,B:] <> {} ;
then A6: A <> {} by ZFMISC_1:90;
A7: B <> {} by A5, ZFMISC_1:90;
then reconsider a1 = the Element of A, a2 = the Element of B as Element of D by A6, TARSKI:def_3;
A8: {a1} c= A by A6, ZFMISC_1:31;
 o . (a1,a2) in {(the_unity_wrt o)} by A3, A4, A6, A7, Th45;
then A9: o . (a1,a2) = the_unity_wrt o by TARSKI:def_1;
then A10: a2 = the_unity_wrt o by A2;
A11: A c= {(the_unity_wrt o)}
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in A or x in {(the_unity_wrt o)} )
assume A12: x in A ; ::_thesis: x in {(the_unity_wrt o)}
then reconsider c = x as Element of D ;
 o . (c,a2) in {(the_unity_wrt o)} by A3, A4, A7, A12, Th45;
then  o . (c,a2) = the_unity_wrt o by TARSKI:def_1;
then  c = a2 by A2;
hence  x in {(the_unity_wrt o)} by A10, TARSKI:def_1; ::_thesis: verum
end;
A13: B c= {(the_unity_wrt o)}
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in B or x in {(the_unity_wrt o)} )
assume A14: x in B ; ::_thesis: x in {(the_unity_wrt o)}
then reconsider c = x as Element of D ;
 o . (a1,c) in {(the_unity_wrt o)} by A3, A4, A6, A14, Th45;
then  o . (a1,c) = the_unity_wrt o by TARSKI:def_1;
then  c = the_unity_wrt o by A2;
hence  x in {(the_unity_wrt o)} by TARSKI:def_1; ::_thesis: verum
end;
A15: a1 = a2 by A2, A9;
 {a2} c= B by A7, ZFMISC_1:31;
then  B = {(the_unity_wrt o)} by A10, A13, XBOOLE_0:def_10;
hence  ( A = B & B = the_unity_wrt (o .:^2) ) by A1, A15, A10, A8, A11, Th53, XBOOLE_0:def_10; ::_thesis: verum
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
percases ( G is unital or not G is unital ) ;
suppose G is unital ; ::_thesis: not bool G is empty
then  bool G = multLoopStr(# (bool the carrier of G),( the multF of G .:^2),{(the_unity_wrt the multF of G)} #) by Def9;
hence  not the carrier of (bool G) is empty ; :: according to STRUCT_0:def_1 ::_thesis: verum
end;
suppose not G is unital ; ::_thesis: not bool G is empty
then  bool G = multMagma(# (bool the carrier of G),( the multF of G .:^2) #) by Def9;
hence  not the carrier of (bool G) is empty ; :: according to STRUCT_0:def_1 ::_thesis: verum
end;
end;
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
set M = multLoopStr(# (bool H3(G)),(H1(G) .:^2),{(the_unity_wrt H1(G))} #);
 H1(G) is having_a_unity by MONOID_0:def_10;
then A1: {(the_unity_wrt H1(G))} is_a_unity_wrt H1(G) .:^2 by Th53;
 ( 1. multLoopStr(# (bool H3(G)),(H1(G) .:^2),{(the_unity_wrt H1(G))} #) = {(the_unity_wrt H1(G))} & bool G = multLoopStr(# (bool H3(G)),(H1(G) .:^2),{(the_unity_wrt H1(G))} #) ) by Def9;
hence  bool G is non empty strict well-unital multLoopStr by A1, MONOID_0:def_21; ::_thesis: verum
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
let G be non empty multMagma ; ::_thesis: ( the carrier of (bool G) = bool the carrier of G & the multF of (bool G) = the multF of G .:^2 )
 ( bool G = multLoopStr(# (bool H3(G)),(H1(G) .:^2),{(the_unity_wrt H1(G))} #) or bool G = multMagma(# (bool the carrier of G),(H1(G) .:^2) #) ) by Def9;
hence  ( the carrier of (bool G) = bool the carrier of G & the multF of (bool G) = the multF of G .:^2 ) ; ::_thesis: verum
end;

theorem :: MONOID_1:56
for G being non empty unital multMagma holds 1. (bool G) = {(the_unity_wrt the multF of G)}
proof
let G be non empty unital multMagma ; ::_thesis: 1. (bool G) = {(the_unity_wrt the multF of G)}
 bool G = multLoopStr(# (bool H3(G)),(H1(G) .:^2),{(the_unity_wrt H1(G))} #) by Def9;
hence  1. (bool G) = {(the_unity_wrt the multF of G)} ; ::_thesis: verum
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
let G be non empty multMagma ; ::_thesis: ( ( 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 ) )
A1: ( H1( bool G) = H1(G) .:^2 & H3( bool G) = bool H3(G) ) by Th55;
thus  ( G is commutative implies bool G is commutative ) ::_thesis: ( ( G is associative implies bool G is associative ) & ( G is uniquely-decomposable implies bool G is uniquely-decomposable ) )
proof
assume  H1(G) is commutative ; :: according to MONOID_0:def_11 ::_thesis: bool G is commutative
hence  H1( bool G) is commutative by A1, Th49; :: according to MONOID_0:def_11 ::_thesis: verum
end;
thus  ( G is associative implies bool G is associative ) ::_thesis: ( G is uniquely-decomposable implies bool G is uniquely-decomposable )
proof
assume  H1(G) is associative ; :: according to MONOID_0:def_12 ::_thesis: bool G is associative
hence  H1( bool G) is associative by A1, Th50; :: according to MONOID_0:def_12 ::_thesis: verum
end;
assume  H1(G) is uniquely-decomposable ; :: according to MONOID_0:def_20 ::_thesis: bool G is uniquely-decomposable
hence  H1( bool G) is uniquely-decomposable by A1, Th54; :: according to MONOID_0:def_20 ::_thesis: verum
end;