let M be non empty-yielding Matrix of REAL; :: thesis: ( M is non empty-yielding Conditional_Probability Matrix of REAL iff for i being Element of NAT st i in dom M holds
Line (M,i) is non empty ProbFinS FinSequence of REAL )

hereby :: thesis: ( ( for i being Element of NAT st i in dom M holds
Line (M,i) is non empty ProbFinS FinSequence of REAL ) implies M is non empty-yielding Conditional_Probability Matrix of REAL )

assume A1: M is non empty-yielding Conditional_Probability Matrix of REAL ; :: thesis: for i being Element of NAT st i in dom M holds
Line (M,i) is non empty ProbFinS FinSequence of REAL

hereby :: thesis: verum

set m = width M;
let i be Element of NAT ; :: thesis: ( i in dom M implies Line (M,i) is non empty ProbFinS FinSequence of REAL )
assume A2: i in dom M ; :: thesis: Line (M,i) is non empty ProbFinS FinSequence of REAL
for i, j being Element of NAT st [i,j] in Indices M holds
M * (i,j) >= 0 by A1, Def6;
then A3: ( len (Line (M,i)) = width M & ( for j being Element of NAT st j in dom (Line (M,i)) holds
(Line (M,i)) . j >= 0 ) ) by A2, Lm2, MATRIX_1:def 8;
Sum (Line (M,i)) = Sum (M . i) by A2, MATRIX_2:18
.= 1 by A1, A2, Def9 ;
hence Line (M,i) is non empty ProbFinS FinSequence of REAL by A3, Def5, Th54; :: thesis: verum

end;

end;

assume A4: for i being Element of NAT st i in dom M holds
Line (M,i) is non empty ProbFinS FinSequence of REAL ; :: thesis: M is non empty-yielding Conditional_Probability Matrix of REAL

now

let k be Element of NAT ; :: thesis: ( k in dom M implies Sum (M . k) = 1 )
assume A5: k in dom M ; :: thesis: Sum (M . k) = 1
Line (M,k) is ProbFinS by A4, A5;
then Sum (Line (M,k)) = 1 by Def5;
hence Sum (M . k) = 1 by A5, MATRIX_2:18; :: thesis: verum

end;

then A6: M is with_line_sum=1 by Def9;
for i, j being Element of NAT st i in dom M & j in dom (Line (M,i)) holds
(Line (M,i)) . j >= 0

proof

let i, j be Element of NAT ; :: thesis: ( i in dom M & j in dom (Line (M,i)) implies (Line (M,i)) . j >= 0 )
assume that
A7: i in dom M and
A8: j in dom (Line (M,i)) ; :: thesis: (Line (M,i)) . j >= 0
Line (M,i) is ProbFinS by A4, A7;
hence (Line (M,i)) . j >= 0 by A8, Def5; :: thesis: verum

end;

then for i, j being Element of NAT st [i,j] in Indices M holds
M * (i,j) >= 0 by Lm2;
then M is m-nonnegative by Def6;
hence M is non empty-yielding Conditional_Probability Matrix of REAL by A6; :: thesis: verum