theorem :: FINSEQ_1:72

for p being FinSequence holds p | (Seg 0) = {} ;