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