theorem :: MATGRP_0:38

for R being Ring
for n, i, k, i2, k2 being Nat st [i2,k2] in Indices (canMat (i,k,n,R)) holds
( ( i <> i2 implies (canMat (i,k,n,R)) * (i2,k2) = 0. R ) & ( k <> k2 implies (canMat (i,k,n,R)) * (i2,k2) = 0. R ) & ( i = i2 & k = k2 implies (canMat (i,k,n,R)) * (i2,k2) = 1. R ) ) by Th40;