A1: dom (curry {} ) = proj1 (dom {} ) by Def3;
hence curry {} = {} ; :: thesis: curry' {} = {}
thus curry' {} = {} by A1, Th1; :: thesis: verum