theorem Th4: :: NDIFF11:4

for m being non zero Nat
for s being FinSequence of REAL m
for j being Nat st 1 <= j & j <= m holds
ex t being FinSequence of REAL st
( len t = len s & ( for i being Nat st 1 <= i & i <= len s holds
ex si being Element of REAL m st
( si = s . i & t . i = si . j ) ) & (Sum s) . j = Sum t )