reconsider I0 = 0 as Element of INT by INT_1:def 2;
set M = n |-> (m |-> I0);
reconsider M = n |-> (m |-> I0) as Matrix of n,m,INT by MATRIX_0:10;
M = n |-> (m |-> 0) ;
hence n |-> (m |-> (0. INT.Ring)) is Matrix of n,m,INT.Ring ; :: thesis: verum