let n, m be Element of NAT ; :: thesis: ( n > 0 implies (0_Rmatrix n,m) + (0_Rmatrix n,m) = 0_Rmatrix n,m )
assume A1: n > 0 ; :: thesis: (0_Rmatrix n,m) + (0_Rmatrix n,m) = 0_Rmatrix n,m
then ( width (0_Rmatrix n,m) = m & len (0_Rmatrix n,m) = n ) by MATRIX_1:24;
then (0 + 0 ) * (0_Rmatrix n,m) = 0_Rmatrix n,m by A1, MATRIXR1:44;
hence (0_Rmatrix n,m) + (0_Rmatrix n,m) = 0_Rmatrix n,m by Th12; :: thesis: verum