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 A1: ( rng f c= PFuncs X,Y & not {} in rng f ) ; :: thesis: ( curry (uncurry f) = f & curry' (uncurry' f) = f )
A2: dom (curry (uncurry f)) = dom f

proof

dom (uncurry f) c= [:(dom f),X:] by A1, Th44;
hence dom (curry (uncurry f)) c= dom f by Th32; :: according to XBOOLE_0:def 10 :: thesis: dom f c= dom (curry (uncurry f))
let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in dom f or x in dom (curry (uncurry f)) )
assume A3: x in dom f ; :: thesis: x in dom (curry (uncurry f))
then f . x in rng f by FUNCT_1:def 5;
then consider g being Function such that
A4: ( f . x = g & dom g c= X & rng g c= Y ) by A1, PARTFUN1:def 5;
g <> {} by A1, A3, A4, FUNCT_1:def 5;
then A5: dom g <> {} ;
consider y being Element of dom g;
( [x,y] in dom (uncurry f) & dom (curry (uncurry f)) = proj1 (dom (uncurry f)) ) by A3, A4, A5, Def3, Th45;
hence x in dom (curry (uncurry f)) by RELAT_1:def 4; :: thesis: verum

end;

now

let x be set ; :: thesis: ( x in dom f implies f . x = (curry (uncurry f)) . x )
assume A6: x in dom f ; :: thesis: f . x = (curry (uncurry f)) . x
then f . x in rng f by FUNCT_1:def 5;
then consider g being Function such that
A7: ( f . x = g & dom g c= X & rng g c= Y ) by A1, PARTFUN1:def 5;
reconsider h = (curry (uncurry f)) . x as Function by A2, A6, Th37;
A8: ( dom h = proj2 ((dom (uncurry f)) /\ [:{x},(proj2 (dom (uncurry f))):]) & dom h c= proj2 (dom (uncurry f)) & rng h c= rng (uncurry f) & ( for y being set st y in dom h holds
( h . y = (uncurry f) . x,y & [x,y] in dom (uncurry f) ) ) ) by A2, A6, Th38;
A9: 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 set ; :: 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 set such that
A10: [t,z] in (dom (uncurry f)) /\ [:{x},(proj2 (dom (uncurry f))):] by A8, RELAT_1:def 5;
A11: ( [t,z] in dom (uncurry f) & [t,z] in [:{x},(proj2 (dom (uncurry f))):] ) by A10, XBOOLE_0:def 4;
then consider x1 being set , g1 being Function, x2 being set such that
A12: ( [t,z] = [x1,x2] & x1 in dom f & g1 = f . x1 & x2 in dom g1 ) by Def4;
( t = x & t = x1 & z = x2 ) by A11, A12, ZFMISC_1:33, ZFMISC_1:128;
hence z in dom g by A7, A12; :: thesis: verum

end;

let y be set ; :: 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 A6, A7, Th45;
hence y in dom h by Th27; :: thesis: verum

end;

now

let y be set ; :: thesis: ( y in dom h implies h . y = g . y )
assume A13: y in dom h ; :: thesis: h . y = g . y
hence h . y = (uncurry f) . x,y by A2, A6, Th38
.= g . y by A6, A7, A9, A13, Th45 ;
:: thesis: verum

end;

hence f . x = (curry (uncurry f)) . x by A7, A9, FUNCT_1:9; :: thesis: verum

end;

hence A14: curry (uncurry f) = f by A2, FUNCT_1:9; :: thesis: curry' (uncurry' f) = f
dom (uncurry f) c= [:(dom f),X:] by A1, Th44;
hence curry' (uncurry' f) = f by A14, FUNCT_4:53; :: thesis: verum