let n, m be Element of NAT ; :: thesis: for a being Real st n > 0 holds
a * (0_Rmatrix n,m) = 0_Rmatrix n,m
let a be Real; :: thesis: ( n > 0 implies a * (0_Rmatrix n,m) = 0_Rmatrix n,m )
A1: ( len (a * (0_Rmatrix n,m)) = len (0_Rmatrix n,m) & width (a * (0_Rmatrix n,m)) = width (0_Rmatrix n,m) ) by MATRIXR1:27;
assume A2: n > 0 ; :: thesis: a * (0_Rmatrix n,m) = 0_Rmatrix n,m
then A3: ( width (0_Rmatrix n,m) = m & len (0_Rmatrix n,m) = n ) by MATRIX_1:24;
a * (0_Rmatrix n,m) = a * ((0_Rmatrix n,m) + (0_Rmatrix n,m)) by A2, Th65
.= (a * (0_Rmatrix n,m)) + (a * (0_Rmatrix n,m)) by A3, MATRIXR1:43 ;
hence a * (0_Rmatrix n,m) = 0_Rmatrix n,m by A3, A1, MATRIXR1:37; :: thesis: verum