theorem Th48: :: MATGRP_0:37

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