theorem Th23: :: MATGRP_0:15

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