theorem Th47: :: MATGRP_0:36

for R being Ring
for I, K, L, i, k, l being Nat st i in Seg I & k in Seg K & l in Seg L holds
(canMat (i,k,I,K,R)) * (canMat (k,l,K,L,R)) = canMat (i,l,I,L,R)