for M being V3() Joint_Probability Matrix of REAL holds M @ is V3() Joint_Probability Matrix of REAL