let M be empty-yielding Joint_Probability Matrix of REAL; :: thesis: M @ is empty-yielding 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; :: thesis: ( [i,j] in Indices M1 implies M1 * (i,j) >= 0 )
assume [i,j] in Indices M1 ; :: thesis: 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; :: thesis: 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 empty-yielding Joint_Probability Matrix of REAL by A1, A2, A3, A5, MATRIX_0:def 10; :: thesis: verum