theorem :: FINSEQ_3:71

for p being FinSequence holds p - {} = p