B2: len M = n by MATRIX_0:25;
per cases ( not 0 < n or 0 < n ) ;
suppose X11: not 0 < n ; :: thesis: inttorealM M is Matrix of n,m,REAL
then X1: n = 0 ;
M = {} by B2, X11;
hence inttorealM M is Matrix of n,m,REAL by X1, MATRIX_0:13; :: thesis: verum
end;
suppose X2: 0 < n ; :: thesis: inttorealM M is Matrix of n,m,REAL
then width M = m by B2, MATRIX_0:20;
hence inttorealM M is Matrix of n,m,REAL by X2, B2, MATRIX_0:20; :: thesis: verum
end;
end;