theorem Th8: :: ENTROPY1:8

for q, q1, q2 being FinSequence of REAL st len q1 = len q & len q1 = len q2 & ( for k being Nat st k in dom q1 holds
q . k = (q1 . k) - (q2 . k) ) holds
Sum q = (Sum q1) - (Sum q2)