let x, y be set ; :: thesis: for f being Function st [x,y] in dom f holds
( y in dom (curry' f) & (curry' f) . y is Function )
let f be Function; :: thesis: ( [x,y] in dom f implies ( y in dom (curry' f) & (curry' f) . y is Function ) )
assume [x,y] in dom f ; :: thesis: ( y in dom (curry' f) & (curry' f) . y is Function )
then [y,x] in dom (~ f) by FUNCT_4:42;
hence ( y in dom (curry' f) & (curry' f) . y is Function ) by Th26; :: thesis: verum