theorem Th28: :: FINSEQ_5:28
for f being FinSequence holds f /^ 0 = f