theorem Th28: :: FINSEQ_5:28

for f being FinSequence holds f /^ 0 = f