theorem Th17: :: MATGRP_0:10

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