begin
begin
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)))
begin
Lm1:
for X being set st ( for x being set st x in X holds
x is Function ) holds
SubFuncs X = X
begin
Lm2:
for f being Function holds rng (Frege f) c= product (rngs f)
Lm3:
for f being Function holds product (rngs f) c= rng (Frege f)
begin
begin
Lm4:
for x, y, z being set
for f, g being Function st [x,y] in dom f & g = (curry f) . x & z in dom g holds
[x,z] in dom f
Lm5:
for X being set
for f being Function st f <> {} & X <> {} holds
product (Funcs (X,f)), Funcs (X,(product f)) are_equipotent
begin