theorem Th63: :: ENTROPY1:63

for M being empty-yielding Conditional_Probability Matrix of REAL holds Entropy_of_Cond_Prob M = - (LineSum (Infor_FinSeq_of M))