theorem Th8: :: RFINSEQ:8
for f being FinSequence
for n being Nat holds (f | n) ^ (f /^ n) = f