let M be non empty-yielding Joint_Probability Matrix of REAL; :: thesis: M @ is non 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_2:10;
then reconsider M1 = M @ as Matrix of width M, len M, REAL by MATRIX_2:7;
for i, j being Element of NAT st [i,j] in Indices M1 holds
M1 * (i,j) >= 0

proof

let i, j be Element of 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_1:def 6;
then M1 * (i,j) = M * (j,i) by MATRIX_1:def 6;
hence M1 * (i,j) >= 0 by A4, Def6; :: thesis: verum

end;

then A5: M1 is m-nonnegative by Def6;
SumAll M1 = SumAll M by Th28
.= 1 by Def7 ;
then M1 is with_sum=1 by Def7;
hence M @ is non empty-yielding Joint_Probability Matrix of REAL by A1, A2, A3, A5, GOBOARD1:def 3; :: thesis: verum