for p, q being ProbFinS FinSequence of REAL holds Entropy_of_Joint_Prob ((ColVec2Mx p) * (LineVec2Mx q)) = (Entropy p) + (Entropy q)