theorem Th96: :: FUNCT_7:97

for w being FinSequence
for r being object
for i being natural Number holds len (w +* (i,r)) = len w