:: deftheorem Def11 defines XFS2FS* AFINSQ_1:def 11 :
for D being non empty set
for p being XFinSequence of D st p . 0 is Nat & p . 0 in len p holds
for b₃ being FinSequence of D holds
( b₃ = XFS2FS* p iff for m being Nat st m = p . 0 holds
( len b₃ = m & ( for i being Nat st 1 <= i & i <= m holds
b₃ . i = p . i ) ) );