:: deftheorem Def8 defines FS2XFS AFINSQ_1:def 8 :
for D being set
for q being FinSequence of D
for b₃ being XFinSequence of D holds
( b₃ = FS2XFS q iff ( len b₃ = len q & ( for i being Nat st i < len q holds
q . (i + 1) = b₃ . i ) ) );