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