let X, Y be set ; :: thesis:
let f be Function; :: thesis:
assume that
A1: rng f c= Funcs (X,Y) and
A2: X <> {} ; :: thesis:
A3: dom (uncurry f) = [:(dom f),X:] by A1, Th19;

A4: now :: thesis:

A5: now :: thesis:

let x be object ; :: thesis:
assume A6: x in dom f ; :: thesis:
then consider h being Function such that
A7: ( (curry (uncurry f)) . x = h & dom h = X & rng h c= rng (uncurry f) ) and
A8: for y being object st y in X holds
h . y = (uncurry f) . (x,y) by A2, A3, Th22;
f . x in rng f by A6, FUNCT_1:def 3;
then consider g being Function such that
A9: ( f . x = g & dom g = X ) and
rng g c= Y by A1, FUNCT_2:def 2;

now :: thesis:

let y be object ; :: thesis:
assume A10: y in X ; :: thesis:
then (uncurry f) . (x,y) = g . y by A6, A9, Th31;
hence g . y = h . y by A8, A10; :: thesis:

end;

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

end;

assume dom f <> {} ; :: thesis:
then dom (curry (uncurry f)) = dom f by A2, A3, Th17;
hence curry (uncurry f) = f by A5; :: thesis:

end;

A11: now :: thesis:

assume dom f = {} ; :: thesis:
then ( dom (uncurry f) = {} & f = {} ) by A3;
hence curry (uncurry f) = f by Th35, RELAT_1:41; :: thesis:

end;

hence curry (uncurry f) = f by A4; :: thesis:
thus curry' (uncurry' f) = f by A3, A11, A4, FUNCT_4:52; :: thesis: