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

A4: now :: thesis: ( dom f <> {} implies curry (uncurry f) = f )

A5: 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 A6: x in dom f ; :: thesis: f . x = (curry (uncurry f)) . x
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: for y being object st y in X holds
g . y = h . y

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

end;

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

end;

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

end;

A11: now :: thesis: ( dom f = {} implies curry (uncurry f) = f )

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

end;

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