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