theorem Th46: :: MATGRP_0:35

for R being Ring
for I, K, L being Nat st I <> 0 & K <> 0 holds
for i, k1, k2, l being Nat st k1 <> k2 holds
(canMat (i,k1,I,K,R)) * (canMat (k2,l,K,L,R)) = 0. (R,I,L)