theorem Th40: :: MATGRP_0:29

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