theorem :: MATRIXR1:66

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