theorem Th2: :: NDIFF11:2

for m being non zero Nat
for s, t being FinSequence of REAL m st 1 <= len s & s = t | (len s) holds
for i being Nat st 1 <= i & i <= len s holds
(accum t) . i = (accum s) . i