let P1, P2 be empty-yielding Conditional_Probability Matrix of REAL; :: thesis: ( width P1 = len P2 implies ( P1 * P2 is empty-yielding Conditional_Probability Matrix of REAL & len (P1 * P2) = len P1 & width (P1 * P2) = width P2 ) )
assume A1: width P1 = len P2 ; :: thesis: ( P1 * P2 is empty-yielding Conditional_Probability Matrix of REAL & len (P1 * P2) = len P1 & width (P1 * P2) = width P2 )
set n2 = width P2;
set m = len P2;
set n1 = len P1;
A2: len (P1 * P2) = len P1 by A1, Th42;
A3: width (P1 * P2) = width P2 by A1, Th42;
then reconsider P = P1 * P2 as Matrix of len P1, width P2,REAL by A2, MATRIX_0:51;
A4: for i being Nat st i in dom P holds
Line (P,i) is non empty ProbFinS FinSequence of REAL

proof

let i be Nat; :: thesis: ( i in dom P implies Line (P,i) is non empty ProbFinS FinSequence of REAL )
assume i in dom P ; :: thesis: Line (P,i) is non empty ProbFinS FinSequence of REAL
then A5: i in Seg (len P) by FINSEQ_1:def 3;
then i in dom P1 by A2, FINSEQ_1:def 3;
then reconsider p = Line (P1,i) as non empty ProbFinS FinSequence of REAL by Th60;
len p = len P2 by A1, MATRIX_0:def 7;
then p * P2 is non empty ProbFinS FinSequence of REAL by Th62;
hence Line (P,i) is non empty ProbFinS FinSequence of REAL by A1, A5, Th42; :: thesis: verum

end;

( len P1 > 0 & width P2 > 0 ) by Th54;
then P is empty-yielding Matrix of REAL by A2, A3, MATRIX_0:def 10;
hence ( P1 * P2 is empty-yielding Conditional_Probability Matrix of REAL & len (P1 * P2) = len P1 & width (P1 * P2) = width P2 ) by A1, A4, Th42, Th60; :: thesis: verum