let X, Y be set ; :: thesis: for f being Function st dom f = [:X,Y:] holds
( uncurry (curry f) = f & uncurry' (curry' f) = f )
let f be Function; :: thesis: ( dom f = [:X,Y:] implies ( uncurry (curry f) = f & uncurry' (curry' f) = f ) )
assume A1: dom f = [:X,Y:] ; :: thesis: ( uncurry (curry f) = f & uncurry' (curry' f) = f )

A2: now

A3: rng (curry' f) c= Funcs (X,(rng f)) by A1, Th42;
assume A4: dom f <> {} ; :: thesis: ( uncurry (curry f) = f & uncurry' (curry' f) = f )
then X <> {} by A1, ZFMISC_1:90;
then A5: curry' (uncurry' (curry' f)) = curry' f by A3, Th55;
dom (curry' f) = Y by A1, A4, Th31;
then A6: dom (uncurry' (curry' f)) = [:X,Y:] by A3, Th33;
A7: rng (curry f) c= Funcs (Y,(rng f)) by A1, Th42;
Y <> {} by A1, A4, ZFMISC_1:90;
then A8: curry (uncurry (curry f)) = curry f by A7, Th55;
dom (curry f) = X by A1, A4, Th31;
then dom (uncurry (curry f)) = [:X,Y:] by A7, Th33;
hence ( uncurry (curry f) = f & uncurry' (curry' f) = f ) by A1, A8, A5, A6, Th51, Th52; :: thesis: verum

end;

now

assume dom f = {} ; :: thesis: ( uncurry (curry f) = f & uncurry' (curry' f) = f )
then f = {} ;
hence ( uncurry (curry f) = f & uncurry' (curry' f) = f ) by Th49, Th50; :: thesis: verum

end;

hence ( uncurry (curry f) = f & uncurry' (curry' f) = f ) by A2; :: thesis: verum