theorem Th84: :: MSAFREE4:84

for p being FinSequence
for i being Nat st i + 1 <= len p holds
p /^ i = <*(p . (i + 1))*> ^ (p /^ (i + 1))