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 & width M > 0 ) by Th54;
then A2: ( len (M @ ) = width M & width (M @ ) = len M ) by MATRIX_2:12;
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 [j,i] in Indices M by MATRIX_1:def 7;
then ( M1 * i,j = M * j,i & M * j,i >= 0 ) by Def6, MATRIX_1:def 7;
hence M1 * i,j >= 0 ; :: thesis: verum

end;

then A3: 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, GOBOARD1:def 5; :: thesis: verum