:: deftheorem defines is_tail_of CALCUL_1:def 16 :
for f being FinSequence
for p being set holds
( p is_tail_of f iff ex i being Nat st
( i in dom f & f . i = p ) );