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,F_Real

then X1: n = 0 ;
M = {} by X11, MATRIX_0:25;
hence inttorealM M is Matrix of n,m,F_Real by X1, MATRIX_0:13; :: thesis: verum

end;

suppose X2: 0 < n ; :: thesis: inttorealM M is Matrix of n,m,F_Real

then width M = m by B2, MATRIX_0:20;
hence inttorealM M is Matrix of n,m,F_Real by X2, B2, MATRIX_0:20; :: thesis: verum

end;

end;