B /\ (Segm (len f)) c= dom f by XBOOLE_1:17;
then rng (Sgm0 (B /\ (Segm (len f)))) c= dom f by Def4;
hence f * (Sgm0 (B /\ (Segm (len f)))) is XFinSequence by AFINSQ_1:10; :: thesis: verum