environ
vocabularies HIDDEN, FUNCT_1, SUBSET_1, FUNCT_2, XBOOLE_0, CARD_3, RELAT_1, FUNCOP_1, TARSKI, ZFMISC_1, FUNCT_5, PARTFUN1, SETFAM_1, FINSEQ_4, MCART_1, FUNCT_6, NAT_1;
notations HIDDEN, TARSKI, XBOOLE_0, ENUMSET1, ZFMISC_1, SUBSET_1, RELAT_1, FUNCT_1, XTUPLE_0, MCART_1, SETFAM_1, FUNCT_2, BINOP_1, PARTFUN1, FUNCT_3, WELLORD2, FUNCOP_1, FUNCT_4, FUNCT_5, ORDINAL1, CARD_3;
definitions TARSKI, FUNCT_1, WELLORD2, XBOOLE_0, FUNCOP_1;
theorems TARSKI, ZFMISC_1, FUNCT_1, SETFAM_1, FUNCT_2, FUNCOP_1, CARD_1, CARD_3, FUNCT_4, FUNCT_5, PARTFUN1, WELLORD2, RELAT_1, XBOOLE_0, XTUPLE_0;
schemes FUNCT_1, PARTFUN1, CARD_3, CLASSES1;
registrations XBOOLE_0, RELAT_1, FUNCT_1, FUNCT_2, FUNCOP_1, RELSET_1, XTUPLE_0, FUNCT_5, CARD_3;
constructors HIDDEN, ENUMSET1, SETFAM_1, PARTFUN1, WELLORD2, BINOP_1, FUNCT_3, FUNCOP_1, FUNCT_4, FUNCT_5, CARD_3, RELSET_1, FINSET_1, DOMAIN_1, XTUPLE_0;
requirements HIDDEN, NUMERALS, BOOLE, SUBSET;
equalities BINOP_1, FUNCOP_1;
expansions TARSKI, FUNCT_1, WELLORD2, XBOOLE_0;
theorem
for
X,
Y,
Z,
V1,
V2 being
set for
f being
Function st (
curry f in Funcs (
X,
(Funcs (Y,Z))) or
curry' f in Funcs (
Y,
(Funcs (X,Z))) ) &
dom f c= [:V1,V2:] holds
f in Funcs (
[:X,Y:],
Z)
theorem
for
X,
Y,
Z,
V1,
V2 being
set for
f being
Function st (
uncurry f in Funcs (
[:X,Y:],
Z) or
uncurry' f in Funcs (
[:Y,X:],
Z) ) &
rng f c= PFuncs (
V1,
V2) &
dom f = X holds
f in Funcs (
X,
(Funcs (Y,Z)))
theorem
for
X,
Y,
Z,
V1,
V2 being
set for
f being
Function st (
curry f in PFuncs (
X,
(PFuncs (Y,Z))) or
curry' f in PFuncs (
Y,
(PFuncs (X,Z))) ) &
dom f c= [:V1,V2:] holds
f in PFuncs (
[:X,Y:],
Z)
theorem
for
X,
Y,
Z,
V1,
V2 being
set for
f being
Function st (
uncurry f in PFuncs (
[:X,Y:],
Z) or
uncurry' f in PFuncs (
[:Y,X:],
Z) ) &
rng f c= PFuncs (
V1,
V2) &
dom f c= X holds
f in PFuncs (
X,
(PFuncs (Y,Z)))
Lm1:
for f being Function-yielding Function holds rng (Frege f) c= product (rngs f)
Lm2:
for f being Function-yielding Function holds product (rngs f) c= rng (Frege f)
Lm3:
for f, g being Function
for x, y, z being object st [x,y] in dom f & g = (curry f) . x & z in dom g holds
[x,z] in dom f
Lm4:
for X being set
for f being Function st f <> {} & X <> {} holds
product (Funcs (X,f)), Funcs (X,(product f)) are_equipotent