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

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

assume A1: M is empty-yielding Conditional_Probability Matrix of REAL ; :: thesis: for i being 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 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 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 Nat st j in dom (Line (M,i)) holds
(Line (M,i)) . j >= 0 ) ) by A2, Lm2, MATRIX_0:def 7;
Sum (Line (M,i)) = Sum (M . i) by A2, MATRIX_0:60
.= 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 Nat st i in dom M holds
Line (M,i) is non empty ProbFinS FinSequence of REAL ; :: thesis: M is empty-yielding Conditional_Probability Matrix of REAL

now :: thesis: for k being Nat st k in dom M holds
Sum (M . k) = 1

let k be 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 ;
hence Sum (M . k) = 1 by A5, MATRIX_0:60; :: thesis: verum

end;

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

proof

let i, j be 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; :: thesis: verum

end;

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