:: deftheorem Def5 defines -| FINSEQ_4:def 5 :
for p being FinSequence
for x being object st x in rng p holds
for b₃ being FinSequence holds
( b₃ = p -| x iff ex n being Nat st
( n = (x .. p) - 1 & b₃ = p | (Seg n) ) );