for p being XFinSequence
for B being set holds
( len (SubXFinS (p,B)) = card (B /\ (Segm (len p))) & ( for i being Nat st i < len (SubXFinS (p,B)) holds
(SubXFinS (p,B)) . i = p . ((Sgm0 (B /\ (Segm (len p)))) . i) ) )