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