dom (NDdataSeq (g,X,d)) = dom X by Def4;
hence NDdataSeq (g,X,d) is finite by FINSET_1:10; :: thesis: verum