theorem Th7: :: RFINSEQ:7

for f being FinSequence
for n being Nat st n + 1 = len f holds
f = (f | n) ^ <*(f . (n + 1))*>