dom (FNDSC (V,A)) = NAT by Def3;
hence (FNDSC (V,A)) | (Seg n) is FinSequence-like by Th2; :: thesis: verum