let i be Nat; :: thesis: Del ({},i) = {}
dom (Del ({},i)) c= dom {} by WSIERP_1:39;
hence Del ({},i) = {} ; :: thesis: verum