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