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;
:: deftheorem defines .. MONOID_1:def 1 :
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;
..redefine func f .. x1,
x2,
x -> Element of
D;
coherence
f .. x1,x2,x is Element of D
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;
.:redefine func f .: g1,
g2 -> Element of
Funcs A,
D;
coherence
f .: g1,g2 is Element of Funcs A,D
end;
theorem
canceled;
theorem
scheme
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]
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:
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
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
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
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)
theorem Th4:
theorem Th5:
theorem Th6:
theorem Th7:
theorem Th8:
theorem Th9:
theorem Th10:
theorem Th11:
theorem Th12:
theorem Th13:
theorem Th14:
theorem Th15:
theorem
theorem Th17:
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
definition
let G be non
empty multMagma ;
let A be
set ;
func .: G,
A -> multMagma equals :
Def3:
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 :
deffunc H3( non empty multMagma ) -> set = the carrier of $1;
theorem Th18:
theorem
Lm1:
for X being set
for G being non empty multMagma holds .: G,X is constituted-Functions
theorem Th20:
theorem Th21:
theorem Th22:
theorem Th23:
theorem Th24:
theorem
theorem
begin
:: deftheorem defines MultiSet_over MONOID_1:def 4 :
theorem Th27:
theorem Th28:
theorem Th29:
theorem Th30:
theorem Th31:
:: deftheorem defines chi MONOID_1:def 5 :
theorem Th32:
theorem Th33:
:: deftheorem Def6 defines finite-MultiSet_over MONOID_1:def 6 :
theorem Th34:
theorem Th35:
theorem Th36:
:: deftheorem Def7 defines |. MONOID_1:def 7 :
theorem
theorem Th38:
theorem
theorem Th40:
theorem Th41:
theorem Th42:
theorem
theorem
begin
definition
let D1,
D2,
D be non
empty set ;
let f be
Function of
D1,
D2,
D;
func f .:^2 -> Function of
(bool D1),
(bool D2),
(bool D) means :
Def8:
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 ):]
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
end;
:: deftheorem Def8 defines .:^2 MONOID_1:def 8 :
theorem Th45:
theorem Th46:
theorem
theorem Th48:
theorem Th49:
theorem Th50:
theorem Th51:
theorem Th52:
theorem Th53:
theorem Th54:
theorem Th55:
:: deftheorem Def9 defines bool MONOID_1:def 9 :
theorem Th56:
theorem
theorem