environ
vocabularies HIDDEN, SUBSET_1, NUMBERS, ALGSTR_0, MESFUNC1, XBOOLE_0, FUNCT_1, ZFMISC_1, FINSEQ_4, FUNCT_2, RELAT_1, PARTFUN1, TARSKI, FUNCOP_1, FINSEQ_2, FINSEQ_1, BINOP_1, SETWISEO, ALGSTR_1, MONOID_0, LATTICE2, MCART_1, STRUCT_0, GROUP_1, VECTSP_1, BINOP_2, CARD_1, ARYTM_3, FUNCT_3, FINSET_1, ORDINAL4, COMPLEX1, ARYTM_1, MONOID_1, NAT_1, FUNCT_7;
notations HIDDEN, TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, CARD_1, ORDINAL1, NUMBERS, XXREAL_0, XCMPLX_0, REAL_1, NAT_1, RELAT_1, STRUCT_0, FUNCT_1, FINSEQ_1, MONOID_0, RELSET_1, PARTFUN1, FUNCT_2, BINOP_1, FUNCOP_1, RECDEF_1, SETWISEO, FINSET_1, FUNCT_3, FINSEQ_2, LATTICE2, FUNCT_6, DOMAIN_1, ALGSTR_0;
definitions TARSKI, BINOP_1, LATTICE2, SETWISEO, MONOID_0, STRUCT_0, XBOOLE_0;
theorems TARSKI, NAT_1, FINSEQ_1, BINOP_1, MCART_1, FUNCOP_1, ZFMISC_1, FUNCT_1, FUNCT_2, FUNCT_3, CARD_1, CARD_2, FINSEQ_2, FINSEQ_3, FUNCT_5, MONOID_0, GRFUNC_1, RELAT_1, RELSET_1, XBOOLE_0, XBOOLE_1, GROUP_1;
schemes NAT_1, FUNCT_2, MONOID_0, PARTFUN1, FUNCT_1, BINOP_1;
registrations XBOOLE_0, SUBSET_1, RELAT_1, FUNCT_1, ORDINAL1, FUNCT_2, FUNCOP_1, FINSET_1, XREAL_0, NAT_1, FINSEQ_1, STRUCT_0, MONOID_0, CARD_1, RELSET_1, XTUPLE_0, VALUED_0;
constructors HIDDEN, BINOP_1, DOMAIN_1, FUNCT_3, SETWISEO, REAL_1, BINOP_2, RECDEF_1, FUNCT_5, FUNCT_6, LATTICE2, MONOID_0, RELSET_1, NUMBERS;
requirements HIDDEN, NUMERALS, BOOLE, SUBSET, ARITHM;
equalities BINOP_1, STRUCT_0, FUNCT_6, ALGSTR_0;
expansions TARSKI, BINOP_1, SETWISEO, MONOID_0, XBOOLE_0, RELAT_1;
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 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;
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 Th16:
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
deffunc H3( non empty multMagma ) -> set = the carrier of $1;
Lm1:
for X being set
for G being non empty multMagma holds .: (G,X) is constituted-Functions
definition
let D1,
D2,
D be non
empty set ;
let f be
Function of
[:D1,D2:],
D;
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;