let p be non empty ProbFinS FinSequence of REAL ; :: thesis: for P being empty-yielding Conditional_Probability Matrix of REAL st len p = len P holds
( p * P is non empty ProbFinS FinSequence of REAL & len (p * P) = width P )
set n = len p;
let P be empty-yielding Conditional_Probability Matrix of REAL; :: thesis: ( len p = len P implies ( p * P is non empty ProbFinS FinSequence of REAL & len (p * P) = width P ) )
assume A1: len p = len P ; :: thesis: ( p * P is non empty ProbFinS FinSequence of REAL & len (p * P) = width P )
A2: len (p * P) = width P by A1, MATRIXR1:62;
A3: for i being Nat st i in dom (p * P) holds
(p * P) . i >= 0

proof

let i be Nat; :: thesis: ( i in dom (p * P) implies (p * P) . i >= 0 )
assume A4: i in dom (p * P) ; :: thesis: (p * P) . i >= 0
i in Seg (len (p * P)) by A4, FINSEQ_1:def 3;
then A5: (p * P) . i = p "*" (Col (P,i)) by A1, Th40
.= Sum (mlt (p,(Col (P,i)))) ;
A6: for i, j being Nat st [i,j] in Indices P holds
P * (i,j) >= 0 by Def6;
i in Seg (width P) by A2, A4, FINSEQ_1:def 3;
then A7: for j being Nat st j in dom (Col (P,i)) holds
(Col (P,i)) . j >= 0 by A6, Lm3;
for i being Nat st i in dom p holds
p . i >= 0 by Def5;
then for k being Nat st k in dom (mlt (p,(Col (P,i)))) holds
(mlt (p,(Col (P,i)))) . k >= 0 by A7, Th33;
hence (p * P) . i >= 0 by A5, RVSUM_1:84; :: thesis: verum

end;

set m = width P;
set e = (width P) |-> jj;
A8: len ((width P) |-> jj) = width P by CARD_1:def 7;
A9: width P > 0 by Th54;
then A10: len (P @) = width P by MATRIX_0:54;
width (P @) = len P by A9, MATRIX_0:54;
then A11: len (((width P) |-> jj) * (P @)) = len p by A1, A8, A10, MATRIXR1:62;
for k being Nat st k in dom (((width P) |-> jj) * (P @)) holds
(((width P) |-> jj) * (P @)) . k = 1

proof

let k be Nat; :: thesis: ( k in dom (((width P) |-> jj) * (P @)) implies (((width P) |-> jj) * (P @)) . k = 1 )
assume k in dom (((width P) |-> jj) * (P @)) ; :: thesis: (((width P) |-> jj) * (P @)) . k = 1
then A12: k in Seg (len (((width P) |-> jj) * (P @))) by FINSEQ_1:def 3;
then A13: k in dom P by A1, A11, FINSEQ_1:def 3;
thus (((width P) |-> jj) * (P @)) . k = Sum (Col ((P @),k)) by A8, A10, A12, Th50
.= Sum (Line (P,k)) by A13, MATRIX_0:58
.= Sum (P . k) by A13, MATRIX_0:60
.= 1 by A13, Def9 ; :: thesis: verum

end;

then A14: ((width P) |-> jj) * (P @) = (len p) |-> jj by A11, Th1;
Sum (p * P) = |((p * P),((width P) |-> jj))| by A2, Th32
.= |(p,(((width P) |-> jj) * (P @)))| by A1, A9, A8, Th49
.= Sum p by A14, Th32
.= 1 by Def5 ;
hence ( p * P is non empty ProbFinS FinSequence of REAL & len (p * P) = width P ) by A2, A3, Def5, Th54; :: thesis: verum