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 :: thesis: ( dom f <> {} implies ( uncurry (curry f) = f & uncurry' (curry' f) = f ) )

A3: rng (curry' f) c= Funcs (X,(rng f)) by A1, Th28;
assume A4: dom f <> {} ; :: thesis: ( uncurry (curry f) = f & uncurry' (curry' f) = f )
then X <> {} by A1;
then A5: curry' (uncurry' (curry' f)) = curry' f by A3, Th41;
dom (curry' f) = Y by A1, A4, Th17;
then A6: dom (uncurry' (curry' f)) = [:X,Y:] by A3, Th19;
A7: rng (curry f) c= Funcs (Y,(rng f)) by A1, Th28;
Y <> {} by A1, A4;
then A8: curry (uncurry (curry f)) = curry f by A7, Th41;
dom (curry f) = X by A1, A4, Th17;
then dom (uncurry (curry f)) = [:X,Y:] by A7, Th19;
hence ( uncurry (curry f) = f & uncurry' (curry' f) = f ) by A1, A8, A5, A6, Th37, Th38; :: thesis: verum

end;

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

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

end;

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