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

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
set n = len M;
set m = width M;
A3: ( len M > 0 & width M > 0 ) by Th54;
A4: len (Line M,i) = width M by MATRIX_1:def 8;
A5: Sum (Line M,i) = Sum (M . i) by A2, MATRIX_2:18
.= 1 by A1, A2, Def9 ;
( ( for i, j being Element of NAT st [i,j] in Indices M holds
M * i,j >= 0 ) & ( for k being Element of NAT st k in dom M holds
Sum (M . k) = 1 ) ) by A1, Def6, Def9;
then for j being Element of NAT st j in dom (Line M,i) holds
(Line M,i) . j >= 0 by A2, Lm2;
hence Line M,i is non empty ProbFinS FinSequence of REAL by A3, A4, A5, Def5; :: thesis: verum

end;

end;

assume A6: 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
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 A7: ( i in dom M & j in dom (Line M,i) ) ; :: thesis: (Line M,i) . j >= 0
Line M,i is ProbFinS by A6, A7;
hence (Line M,i) . j >= 0 by A7, 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 A8: M is m-nonnegative by Def6;

now

let k be Element of NAT ; :: thesis: ( k in dom M implies Sum (M . k) = 1 )
assume A9: k in dom M ; :: thesis: Sum (M . k) = 1
Line M,k is ProbFinS by A6, A9;
then ( ( for j being Element of NAT st j in dom (Line M,k) holds
(Line M,k) . j >= 0 ) & Sum (Line M,k) = 1 ) by Def5;
hence Sum (M . k) = 1 by A9, MATRIX_2:18; :: thesis: verum

end;

then M is with_line_sum=1 by Def9;
hence M is non empty-yielding Conditional_Probability Matrix of REAL by A8; :: thesis: verum