theorem Th19: :: MATGRP_0:12

for R being Ring
for i, k, m, n being Nat
for A being Matrix of m,n,R st i in dom (0. (R,m)) holds
(Line ((0. (R,m)),i)) "*" (Col (A,k)) = 0. R