theorem :: MATRIXR1:65

for n, m being Nat
for x being FinSequence of REAL st len x = m & n > 0 & m > 0 holds
(0_Rmatrix (n,m)) * x = 0* n