theorem Th3: :: FINSEQ_5:85

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