theorem Th9: :: ENTROPY1:9

for p being FinSequence of REAL st len p >= 1 holds
ex q being FinSequence of REAL st
( len q = len p & q . 1 = p . 1 & ( for k being Nat st 0 <> k & k < len p holds
q . (k + 1) = (q . k) + (p . (k + 1)) ) & Sum p = q . (len p) )