theorem Th8: :: RFINSEQ:8

for f being FinSequence
for n being Nat holds (f | n) ^ (f /^ n) = f