let M be empty-yielding Conditional_Probability Matrix of REAL; :: thesis: for i, j being Nat st [i,j] in Indices M holds
M * (i,j) <= 1
A1: for i, j being Nat st [i,j] in Indices M holds
M * (i,j) >= 0 by Def6;
A2: for i being Nat st i in dom M holds
for j being Nat st j in dom (M . i) holds
(M . i) . j <= 1

proof

let i be Nat; :: thesis: ( i in dom M implies for j being Nat st j in dom (M . i) holds
(M . i) . j <= 1 )
assume A3: i in dom M ; :: thesis: for j being Nat st j in dom (M . i) holds
(M . i) . j <= 1
A4: for j being Nat st j in dom (M . i) holds
(M . i) . j >= 0 by A1, A3, Lm1;
let j be Nat; :: thesis: ( j in dom (M . i) implies (M . i) . j <= 1 )
assume j in dom (M . i) ; :: thesis: (M . i) . j <= 1
then (M . i) . j <= Sum (M . i) by A4, Th5;
hence (M . i) . j <= 1 by A3, Def9; :: thesis: verum

end;

let i, j be Nat; :: thesis: ( [i,j] in Indices M implies M * (i,j) <= 1 )
assume A5: [i,j] in Indices M ; :: thesis: M * (i,j) <= 1
A6: ex p1 being FinSequence of REAL st
( p1 = M . i & M * (i,j) = p1 . j ) by A5, MATRIX_0:def 5;
i in Seg (len M) by A5, Th12;
then A7: i in dom M by FINSEQ_1:def 3;
j in Seg (width M) by A5, Th12;
then j in Seg (len (M . i)) by A7, MATRIX_0:36;
then j in dom (M . i) by FINSEQ_1:def 3;
hence M * (i,j) <= 1 by A2, A7, A6; :: thesis: verum