let X, Y be set ; for f being Function st dom f = [:X,Y:] holds
( uncurry (curry f) = f & uncurry' (curry' f) = f )
let f be Function; ( dom f = [:X,Y:] implies ( uncurry (curry f) = f & uncurry' (curry' f) = f ) )
assume A1:
dom f = [:X,Y:]
; ( uncurry (curry f) = f & uncurry' (curry' f) = f )
A2:
now ( dom f <> {} implies ( uncurry (curry f) = f & uncurry' (curry' f) = f ) )A3:
rng (curry' f) c= Funcs (
X,
(rng f))
by A1, Th28;
assume A4:
dom f <> {}
;
( uncurry (curry f) = f & uncurry' (curry' f) = f )then
X <> {}
by A1;
then A5:
curry' (uncurry' (curry' f)) = curry' f
by A3, Th41;
dom (curry' f) = Y
by A1, A4, Th17;
then A6:
dom (uncurry' (curry' f)) = [:X,Y:]
by A3, Th19;
A7:
rng (curry f) c= Funcs (
Y,
(rng f))
by A1, Th28;
Y <> {}
by A1, A4;
then A8:
curry (uncurry (curry f)) = curry f
by A7, Th41;
dom (curry f) = X
by A1, A4, Th17;
then
dom (uncurry (curry f)) = [:X,Y:]
by A7, Th19;
hence
(
uncurry (curry f) = f &
uncurry' (curry' f) = f )
by A1, A8, A5, A6, Th37, Th38;
verum end;
hence
( uncurry (curry f) = f & uncurry' (curry' f) = f )
by A2; verum