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