:: deftheorem Def1 defines /^ RFINSEQ:def 1 :
for n being Nat
for f, b₃ being FinSequence holds
( ( n <= len f implies ( b₃ = f /^ n iff ( len b₃ = (len f) - n & ( for m being Nat st m in dom b₃ holds
b₃ . m = f . (m + n) ) ) ) ) & ( not n <= len f implies ( b₃ = f /^ n iff b₃ = {} ) ) );