theorem Th37: :: ENTROPY1:37

for M being Matrix of REAL
for p being FinSequence of REAL * st ( for k being Nat st k >= 1 & k < len M holds
p . (k + 1) = (p . k) ^ (M . (k + 1)) ) holds
for k being Nat st k >= 1 & k < len M holds
Sum (p . (k + 1)) = (Sum (p . k)) + (Sum (M . (k + 1)))