let X, Y be set ; for f being Function st rng f c= PFuncs (X,Y) & not {} in rng f holds
( curry (uncurry f) = f & curry' (uncurry' f) = f )
let f be Function; ( rng f c= PFuncs (X,Y) & not {} in rng f implies ( curry (uncurry f) = f & curry' (uncurry' f) = f ) )
assume that
A1:
rng f c= PFuncs (X,Y)
and
A2:
not {} in rng f
; ( curry (uncurry f) = f & curry' (uncurry' f) = f )
A3:
dom (curry (uncurry f)) = dom f
proof
dom (uncurry f) c= [:(dom f),X:]
by A1, Th30;
hence
dom (curry (uncurry f)) c= dom f
by Th18;
XBOOLE_0:def 10 dom f c= dom (curry (uncurry f))
let x be
object ;
TARSKI:def 3 ( not x in dom f or x in dom (curry (uncurry f)) )
assume A4:
x in dom f
;
x in dom (curry (uncurry f))
then
f . x in rng f
by FUNCT_1:def 3;
then consider g being
Function such that A5:
f . x = g
and
dom g c= X
and
rng g c= Y
by A1, PARTFUN1:def 3;
set y = the
Element of
dom g;
g <> {}
by A2, A4, A5, FUNCT_1:def 3;
then A6:
[x, the Element of dom g] in dom (uncurry f)
by A4, A5, Th31;
dom (curry (uncurry f)) = proj1 (dom (uncurry f))
by Def1;
hence
x in dom (curry (uncurry f))
by A6, XTUPLE_0:def 12;
verum
end;
now for x being object st x in dom f holds
f . x = (curry (uncurry f)) . xlet x be
object ;
( x in dom f implies f . x = (curry (uncurry f)) . x )assume A7:
x in dom f
;
f . x = (curry (uncurry f)) . xthen reconsider h =
(curry (uncurry f)) . x as
Function by A3, Th23;
f . x in rng f
by A7, FUNCT_1:def 3;
then consider g being
Function such that A8:
f . x = g
and
dom g c= X
and
rng g c= Y
by A1, PARTFUN1:def 3;
A9:
dom h = proj2 ((dom (uncurry f)) /\ [:{x},(proj2 (dom (uncurry f))):])
by A3, A7, Th24;
A10:
dom h = dom g
proof
thus
dom h c= dom g
XBOOLE_0:def 10 dom g c= dom hproof
let z be
object ;
TARSKI:def 3 ( not z in dom h or z in dom g )
assume
z in dom h
;
z in dom g
then consider t being
object such that A11:
[t,z] in (dom (uncurry f)) /\ [:{x},(proj2 (dom (uncurry f))):]
by A9, XTUPLE_0:def 13;
[t,z] in [:{x},(proj2 (dom (uncurry f))):]
by A11, XBOOLE_0:def 4;
then A12:
t = x
by ZFMISC_1:105;
[t,z] in dom (uncurry f)
by A11, XBOOLE_0:def 4;
then consider x1 being
object ,
g1 being
Function,
x2 being
object such that A13:
[t,z] = [x1,x2]
and
x1 in dom f
and A14:
(
g1 = f . x1 &
x2 in dom g1 )
by Def2;
t = x1
by A13, XTUPLE_0:1;
hence
z in dom g
by A8, A13, A14, A12, XTUPLE_0:1;
verum
end;
let y be
object ;
TARSKI:def 3 ( not y in dom g or y in dom h )
assume
y in dom g
;
y in dom h
then
[x,y] in dom (uncurry f)
by A7, A8, Th31;
hence
y in dom h
by Th13;
verum
end; hence
f . x = (curry (uncurry f)) . x
by A8, A10, FUNCT_1:2;
verum end;
hence A16:
curry (uncurry f) = f
by A3; curry' (uncurry' f) = f
dom (uncurry f) c= [:(dom f),X:]
by A1, Th30;
hence
curry' (uncurry' f) = f
by A16, FUNCT_4:52; verum