theorem :: MATRPROB:63

for P1, P2 being V3() Conditional_Probability Matrix of REAL st width P1 = len P2 holds
( P1 * P2 is V3() Conditional_Probability Matrix of REAL & len (P1 * P2) = len P1 & width (P1 * P2) = width P2 )