theorem Th62: :: ENTROPY1:62

for M being empty-yielding Conditional_Probability Matrix of REAL
for p being FinSequence of REAL holds
( p = Entropy_of_Cond_Prob M iff ( len p = len M & ( for k being Nat st k in dom p holds
p . k = - (Sum ((Infor_FinSeq_of M) . k)) ) ) )