:: deftheorem Def11 defines Entropy_of_Cond_Prob ENTROPY1:def 11 :
for MR being Matrix of REAL
for b₂ being FinSequence of REAL holds
( b₂ = Entropy_of_Cond_Prob MR iff ( len b₂ = len MR & ( for k being Nat st k in dom b₂ holds
b₂ . k = Entropy (Line (MR,k)) ) ) );