let X, Y be set ; :: thesis: 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; :: thesis: ( 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 ; :: thesis: ( 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; :: according to XBOOLE_0:def 10 :: thesis: dom f c= dom (curry (uncurry f))
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in dom f or x in dom (curry (uncurry f)) )
assume A4: x in dom f ; :: thesis: 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; :: thesis: verum

end;

now :: thesis: for x being object st x in dom f holds
f . x = (curry (uncurry f)) . x

let x be object ; :: thesis: ( x in dom f implies f . x = (curry (uncurry f)) . x )
assume A7: x in dom f ; :: thesis: f . x = (curry (uncurry f)) . x
then 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 :: according to XBOOLE_0:def 10 :: thesis: dom g c= dom h

proof

let z be object ; :: according to TARSKI:def 3 :: thesis: ( not z in dom h or z in dom g )
assume z in dom h ; :: thesis: 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; :: thesis: verum

end;

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in dom g or y in dom h )
assume y in dom g ; :: thesis: y in dom h
then [x,y] in dom (uncurry f) by A7, A8, Th31;
hence y in dom h by Th13; :: thesis: verum

end;

now :: thesis: for y being object st y in dom h holds
h . y = g . y

let y be object ; :: thesis: ( y in dom h implies h . y = g . y )
assume A15: y in dom h ; :: thesis: h . y = g . y
hence h . y = (uncurry f) . (x,y) by A3, A7, Th24
.= g . y by A7, A8, A10, A15, Th31 ;
:: thesis: verum

end;

hence f . x = (curry (uncurry f)) . x by A8, A10, FUNCT_1:2; :: thesis: verum

end;

hence A16: curry (uncurry f) = f by A3; :: thesis: curry' (uncurry' f) = f
dom (uncurry f) c= [:(dom f),X:] by A1, Th30;
hence curry' (uncurry' f) = f by A16, FUNCT_4:52; :: thesis: verum