let p be FinSequence; :: thesis: p - {} = p
{} misses rng p ;
hence p - {} = p by Th67; :: thesis: verum