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