theorem Th18: :: MATGRP_0:11

for n being Nat
for R being Ring
for A being Matrix of R st n = width (0. (R,(width A),n)) holds
A * (0. (R,(width A),n)) = 0. (R,(len A),n)