theorem :: FUNCT_5:49

for X, Y being set
for f being Function st dom f = [:X,Y:] holds
( uncurry (curry f) = f & uncurry' (curry' f) = f )