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

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;

now

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

end;

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