let f be Function; :: thesis: ( ( for x, y being object holds not [x,y] in dom f ) implies ( curry f = {} & curry' f = {} ) )
assume A1: for x, y being object holds not [x,y] in dom f ; :: thesis: ( curry f = {} & curry' f = {} )
then proj1 (dom f) = {} by Th8;
then dom (curry f) = {} by Def1;
hence curry f = {} ; :: thesis: curry' f = {}
now :: thesis: for x, y being object holds not [x,y] in dom (~ f)
let x, y be object ; :: thesis: not [x,y] in dom (~ f)
assume [x,y] in dom (~ f) ; :: thesis: contradiction
then [y,x] in dom f by FUNCT_4:42;
hence contradiction by A1; :: thesis: verum
end;
then proj1 (dom (~ f)) = {} by Th8;
then dom (curry (~ f)) = {} by Def1;
hence curry' f = {} ; :: thesis: verum