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

proof

let i be Element of NAT ; :: thesis: ( i in dom M implies for j being Element of NAT st j in dom (M . i) holds
(M . i) . j <= 1 )
assume A3: i in dom M ; :: thesis: for j being Element of 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 Element of NAT ; :: thesis: ( j in dom (M . i) implies (M . i) . j <= 1 )
assume A5: j in dom (M . i) ; :: thesis: (M . i) . j <= 1
(M . i) . j <= Sum (M . i) by A4, A5, Th5;
hence (M . i) . j <= 1 by A3, Def9; :: thesis: verum

end;

let i, j be Element of NAT ; :: thesis: ( [i,j] in Indices M implies M * i,j <= 1 )
assume A6: [i,j] in Indices M ; :: thesis: M * i,j <= 1
A7: ( i in Seg (len M) & j in Seg (width M) ) by A6, Th12;
then A8: i in dom M by FINSEQ_1:def 3;
then j in Seg (len (M . i)) by A7, GOBRD13:4;
then A9: j in dom (M . i) by FINSEQ_1:def 3;
consider p1 being FinSequence of REAL such that
A10: ( p1 = M . i & M * i,j = p1 . j ) by A6, MATRIX_1:def 6;
thus M * i,j <= 1 by A2, A8, A9, A10; :: thesis: verum