theorem :: MATGRP_0:40

for R being Ring
for n, i, j being Nat st not [i,j] in Indices (canMat (i,j,n,R)) holds
canMat (i,j,n,R) = 0. (R,n)