let f be Function; :: thesis: dom (curry' f) = proj2 (dom f)
dom (curry (~ f)) = proj1 (dom (~ f)) by Def1;
hence dom (curry' f) = proj2 (dom f) by Th11; :: thesis: verum