let f be Function; :: thesis: dom (curry' f) = proj2 (dom f)
( dom (curry (~ f)) = proj1 (dom (~ f)) & curry' f = curry (~ f) ) by Def3;
hence dom (curry' f) = proj2 (dom f) by Th20; :: thesis: verum