theorem Th21: :: MATGRP_0:14

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