let M be V3() Joint_Probability Matrix of REAL; M @ is V3() Joint_Probability Matrix of REAL
set n = len M;
set m = width M;
A1:
len M > 0
by Th54;
A2:
width M > 0
by Th54;
then A3:
( len (M @) = width M & width (M @) = len M )
by MATRIX_0:54;
then reconsider M1 = M @ as Matrix of width M, len M,REAL by MATRIX_0:51;
for i, j being Nat st [i,j] in Indices M1 holds
M1 * (i,j) >= 0
proof
let i,
j be
Nat;
( [i,j] in Indices M1 implies M1 * (i,j) >= 0 )
assume
[i,j] in Indices M1
;
M1 * (i,j) >= 0
then A4:
[j,i] in Indices M
by MATRIX_0:def 6;
then
M1 * (
i,
j)
= M * (
j,
i)
by MATRIX_0:def 6;
hence
M1 * (
i,
j)
>= 0
by A4, Def6;
verum
end;
then A5:
M1 is m-nonnegative
;
SumAll M1 =
SumAll M
by Th28
.=
1
by Def7
;
then
M1 is with_sum=1
;
hence
M @ is V3() Joint_Probability Matrix of REAL
by A1, A2, A3, A5, MATRIX_0:def 10; verum