A: rng f c= D by ORDINAL1:def 8;
rng (SubXFinS f,B) c= rng f by RELAT_1:45;
then rng (SubXFinS f,B) c= D by A, XBOOLE_1:1;
hence SubXFinS f,B is XFinSequence of D by ORDINAL1:def 8; :: thesis: verum