:: deftheorem defines SubXFinS AFINSQ_2:def 7 :
for f being XFinSequence
for B being set holds SubXFinS (f,B) = f * (Sgm0 (B /\ (Segm (len f))));