:: deftheorem Def9 defines XFS2FS AFINSQ_1:def 9 :
for D being set
for q being XFinSequence of D
for b₃ being FinSequence of D 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 ) ) );