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 )
assume A1: n > 0 ; :: thesis: a * (0_Rmatrix n,m) = 0_Rmatrix n,m
then A2: width (0_Rmatrix n,m) = m by MATRIX_1:24;
A3: len (0_Rmatrix n,m) = n by A1, MATRIX_1:24;
A4: len (a * (0_Rmatrix n,m)) = len (0_Rmatrix n,m) by MATRIXR1:27;
A5: width (a * (0_Rmatrix n,m)) = width (0_Rmatrix n,m) by MATRIXR1:27;
a * (0_Rmatrix n,m) = a * ((0_Rmatrix n,m) + (0_Rmatrix n,m)) by A1, Th65
.= (a * (0_Rmatrix n,m)) + (a * (0_Rmatrix n,m)) by A1, A2, A3, MATRIXR1:43 ;
hence a * (0_Rmatrix n,m) = 0_Rmatrix n,m by A1, A2, A3, A4, A5, MATRIXR1:37; :: thesis: verum