theorem Th55: :: FINSEQ_6:157

for f being FinSequence holds f ^' {} = f