:: deftheorem Def9A defines XFS2FS AFINSQ_1:def 9 :
for q being XFinSequence
for b₂ being FinSequence holds
( b₂ = XFS2FS q iff ( len b₂ = len q & ( for i being Nat st 1 <= i & i <= len q holds
q . (i - 1) = b₂ . i ) ) );