:: deftheorem Def2 defines /^ AFINSQ_2:def 2 :
for p being XFinSequence
for n being Nat
for b₃ being XFinSequence holds
( b₃ = p /^ n iff ( len b₃ = (len p) -' n & ( for m being Nat st m in dom b₃ holds
b₃ . m = p . (m + n) ) ) );