begin
theorem
for
x,
y,
z,
t being
set holds
(
proj1 {[x,y],[z,t]} = {x,z} &
proj2 {[x,y],[z,t]} = {y,t} )
definition
let f be
Function;
existence
ex b1 being Function st
( dom b1 = proj1 (dom f) & ( for x being set st x in proj1 (dom f) holds
ex g being Function st
( b1 . x = g & dom g = proj2 ((dom f) /\ [:{x},(proj2 (dom f)):]) & ( for y being set st y in dom g holds
g . y = f . (x,y) ) ) ) )
uniqueness
for b1, b2 being Function st dom b1 = proj1 (dom f) & ( for x being set st x in proj1 (dom f) holds
ex g being Function st
( b1 . x = g & dom g = proj2 ((dom f) /\ [:{x},(proj2 (dom f)):]) & ( for y being set st y in dom g holds
g . y = f . (x,y) ) ) ) & dom b2 = proj1 (dom f) & ( for x being set st x in proj1 (dom f) holds
ex g being Function st
( b2 . x = g & dom g = proj2 ((dom f) /\ [:{x},(proj2 (dom f)):]) & ( for y being set st y in dom g holds
g . y = f . (x,y) ) ) ) holds
b1 = b2
existence
ex b1 being Function st
( ( for t being set holds
( t in dom b1 iff ex x being set ex g being Function ex y being set st
( t = [x,y] & x in dom f & g = f . x & y in dom g ) ) ) & ( for x being set
for g being Function st x in dom b1 & g = f . (x `1) holds
b1 . x = g . (x `2) ) )
uniqueness
for b1, b2 being Function st ( for t being set holds
( t in dom b1 iff ex x being set ex g being Function ex y being set st
( t = [x,y] & x in dom f & g = f . x & y in dom g ) ) ) & ( for x being set
for g being Function st x in dom b1 & g = f . (x `1) holds
b1 . x = g . (x `2) ) & ( for t being set holds
( t in dom b2 iff ex x being set ex g being Function ex y being set st
( t = [x,y] & x in dom f & g = f . x & y in dom g ) ) ) & ( for x being set
for g being Function st x in dom b2 & g = f . (x `1) holds
b2 . x = g . (x `2) ) holds
b1 = b2
end;
theorem Th60:
for
X1,
Y1,
X2,
Y2 being
set st
X1,
Y1 are_equipotent &
X2,
Y2 are_equipotent holds
(
Funcs (
X1,
X2),
Funcs (
Y1,
Y2)
are_equipotent &
card (Funcs (X1,X2)) = card (Funcs (Y1,Y2)) )
theorem
for
X1,
X2,
X being
set st
X1 misses X2 holds
(
Funcs (
(X1 \/ X2),
X),
[:(Funcs (X1,X)),(Funcs (X2,X)):] are_equipotent &
card (Funcs ((X1 \/ X2),X)) = card [:(Funcs (X1,X)),(Funcs (X2,X)):] )
theorem
for
X,
Y,
Z being
set holds
(
Funcs (
[:X,Y:],
Z),
Funcs (
X,
(Funcs (Y,Z)))
are_equipotent &
card (Funcs ([:X,Y:],Z)) = card (Funcs (X,(Funcs (Y,Z)))) )
theorem
for
Z,
X,
Y being
set holds
(
Funcs (
Z,
[:X,Y:]),
[:(Funcs (Z,X)),(Funcs (Z,Y)):] are_equipotent &
card (Funcs (Z,[:X,Y:])) = card [:(Funcs (Z,X)),(Funcs (Z,Y)):] )
begin
definition
let C,
D,
E be non
empty set ;
let f be
Function of
[:C,D:],
E;
curryredefine func curry f -> Function of
C,
(Funcs (D,E));
coherence
curry f is Function of C,(Funcs (D,E))
by Th1;
curry'redefine func curry' f -> Function of
D,
(Funcs (C,E));
coherence
curry' f is Function of D,(Funcs (C,E))
by Th2;
end;