:: deftheorem defines Entropy_of_Joint_Prob ENTROPY1:def 10 :
for MR being Matrix of REAL holds Entropy_of_Joint_Prob MR = Entropy (Mx2FinS MR);