let P1, P2 be non empty-yielding Conditional_Probability Matrix of REAL ; :: thesis: ( width P1 = len P2 implies ( P1 * P2 is non 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 non empty-yielding Conditional_Probability Matrix of REAL & len (P1 * P2) = len P1 & width (P1 * P2) = width P2 )
set n1 = len P1;
set m = len P2;
set n2 = width P2;
A2: ( len P1 > 0 & len P2 > 0 & width P2 > 0 ) by Th54;
then A3: ( len (P1 * P2) = len P1 & width (P1 * P2) = width P2 & ( for i being Element of NAT st i in Seg (len (P1 * P2)) holds
Line (P1 * P2),i = (Line P1,i) * P2 ) ) by A1, Th42;
then reconsider P = P1 * P2 as Matrix of len P1, width P2, REAL by MATRIX_2:7;
A4: P is non empty-yielding Matrix of REAL by A2, A3, GOBOARD1:def 5;
for i being Element of NAT st i in dom P holds
Line P,i is non empty ProbFinS FinSequence of REAL

proof

let i be Element of NAT ; :: thesis: ( i in dom P implies Line P,i is non empty ProbFinS FinSequence of REAL )
assume A5: i in dom P ; :: thesis: Line P,i is non empty ProbFinS FinSequence of REAL
A6: i in Seg (len P) by A5, FINSEQ_1:def 3;
then i in dom P1 by A3, 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_1:def 8;
then ( p * P2 is non empty ProbFinS FinSequence of REAL & len (p * P2) = width P2 ) by Th62;
hence Line P,i is non empty ProbFinS FinSequence of REAL by A1, A2, A6, Th42; :: thesis: verum

end;

hence ( P1 * P2 is non empty-yielding Conditional_Probability Matrix of REAL & len (P1 * P2) = len P1 & width (P1 * P2) = width P2 ) by A1, A2, A4, Th42, Th60; :: thesis: verum