theorem :: MATGRP_0:41

for R being Ring
for n, i, k, l being Nat st k in Seg n holds
(canMat (i,k,n,R)) * (canMat (k,l,n,R)) = canMat (i,l,n,R) by Th48;