let f be Function; :: thesis: for x, y being object st [x,y] in dom f holds
x in dom (curry f)
let x, y be object ; :: thesis: ( [x,y] in dom f implies x in dom (curry f) )
assume [x,y] in dom f ; :: thesis: x in dom (curry f)
then x in proj1 (dom f) by XTUPLE_0:def 12;
hence x in dom (curry f) by Def1; :: thesis: verum