let f be Function; :: thesis: ( ( for x, y being set holds not [x,y] in dom f ) implies ( curry f = {} & curry' f = {} ) )
assume A1: for x, y being set holds not [x,y] in dom f ; :: thesis: ( curry f = {} & curry' f = {} )
then proj1 (dom f) = {} by Th17;
then dom (curry f) = {} by Def3;
hence curry f = {} ; :: thesis: curry' f = {}

now

let x, y be set ; :: thesis: not [x,y] in dom (~ f)
assume [x,y] in dom (~ f) ; :: thesis: contradiction
then [y,x] in dom f by FUNCT_4:43;
hence contradiction by A1; :: thesis: verum

end;

then proj1 (dom (~ f)) = {} by Th17;
then dom (curry (~ f)) = {} by Def3;
hence curry' f = {} ; :: thesis: verum