rng (XFS2FS f) = rng f by AFINSQ_1:97;
hence XFS2FS f is FinSequence of D ; :: thesis: verum