theorem Th3: :: FINSEQ_5:85

for f being non empty FinSequence holds f /^ 1 = Del (f,1)