let n, m be 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_0:23;
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