theorem Th20: :: LIOUVIL1:20

for f being Real_Sequence
for i being Nat holds (FinSeq (f,i)) ^ <*(f . (i + 1))*> = FinSeq (f,(i + 1))