take len X ; :: according to FINSEQ_1:def 2 :: thesis: dom (NDdataSeq (g,X,d)) = Seg (len X)
thus dom (NDdataSeq (g,X,d)) = dom X by Def4
.= Seg (len X) by FINSEQ_1:def 3 ; :: thesis: verum