theorem Th28: :: FINSEQ_5:28

for D being set
for f being FinSequence of D holds f /^ 0 = f