theorem :: FINSEQ_4:29

for p being FinSequence
for x being object st p is one-to-one & x in rng p holds
{(x .. p)} = p " {x}