:: deftheorem Def6 defines |-- FINSEQ_4:def 6 :
for p being FinSequence
for x being object st x in rng p holds
for b₃ being FinSequence holds
( b₃ = p |-- x iff ( len b₃ = (len p) - (x .. p) & ( for k being Nat st k in dom b₃ holds
b₃ . k = p . (k + (x .. p)) ) ) );