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

proof

let i be Nat; :: thesis: ( i in dom (Sum M) implies (Sum M) . i >= 0 )
assume A3: i in dom (Sum M) ; :: thesis: (Sum M) . i >= 0
i in Seg (len (Sum M)) by A3, 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:84;
hence (Sum M) . i >= 0 by A3, Def1; :: thesis: verum

end;

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

proof

let i be Nat; :: thesis: ( i in dom (Sum M) implies (Sum M) . i <= 1 )
assume i in dom (Sum M) ; :: thesis: (Sum M) . i <= 1
then (Sum M) . i <= SumAll M by A2, Th5;
hence (Sum M) . i <= 1 by Def7; :: thesis: verum

end;

A5: for i being Nat st i in dom M holds
for j being Nat st j in dom (M . i) holds
(M . i) . j <= Sum (M . i)

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

end;

A6: 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 A7: i in dom M ; :: thesis: for j being Nat st j in dom (M . i) holds
(M . i) . j <= 1
i in Seg (len M) by A7, FINSEQ_1:def 3;
then i in Seg (len (Sum M)) by Def1;
then A8: i in dom (Sum M) by FINSEQ_1:def 3;
then (Sum M) . i <= 1 by A4;
then A9: Sum (M . i) <= 1 by A8, Def1;
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 A5, A7;
hence (M . i) . j <= 1 by A9, XXREAL_0:2; :: thesis: verum

end;

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