let M be non empty-yielding Joint_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 <= Sum (M . i)

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 <= Sum (M . i) )
assume A3: i in dom M ; :: thesis: for j being Element of NAT st j in dom (M . i) holds
(M . i) . j <= Sum (M . i)
for j being Nat st j in dom (M . i) holds
(M . i) . j >= 0 by A1, A3, Lm1;
hence for j being Element of NAT st j in dom (M . i) holds
(M . i) . j <= Sum (M . i) by Th5; :: thesis: verum

end;

A4: for i being Nat st i in dom (Sum M) holds
(Sum M) . i >= 0

proof

let i be Nat; :: thesis: ( i in dom (Sum M) implies (Sum M) . i >= 0 )
assume A5: i in dom (Sum M) ; :: thesis: (Sum M) . i >= 0
i in Seg (len (Sum M)) by A5, FINSEQ_1:def 3;
then i in Seg (len M) by Def1;
then i in dom M by FINSEQ_1:def 3;
then for j being Nat st j in dom (M . i) holds
(M . i) . j >= 0 by A1, Lm1;
then Sum (M . i) >= 0 by RVSUM_1:114;
hence (Sum M) . i >= 0 by A5, Def1; :: thesis: verum

end;

A6: for i being Element of NAT st i in dom (Sum M) holds
(Sum M) . i <= 1

proof

let i be Element of NAT ; :: thesis: ( i in dom (Sum M) implies (Sum M) . i <= 1 )
assume A7: i in dom (Sum M) ; :: thesis: (Sum M) . i <= 1
(Sum M) . i <= SumAll M by A4, A7, Th5;
hence (Sum M) . i <= 1 by Def7; :: thesis: verum

end;

A8: 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 A9: i in dom M ; :: thesis: for j being Element of NAT st j in dom (M . i) holds
(M . i) . j <= 1
let j be Element of NAT ; :: thesis: ( j in dom (M . i) implies (M . i) . j <= 1 )
assume A10: j in dom (M . i) ; :: thesis: (M . i) . j <= 1
i in Seg (len M) by A9, FINSEQ_1:def 3;
then i in Seg (len (Sum M)) by Def1;
then A11: i in dom (Sum M) by FINSEQ_1:def 3;
then (Sum M) . i <= 1 by A6;
then A12: Sum (M . i) <= 1 by A11, Def1;
(M . i) . j <= Sum (M . i) by A2, A9, A10;
hence (M . i) . j <= 1 by A12, XXREAL_0:2; :: thesis: verum

end;

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