theorem Th54: :: MATGRP_0:42

for R being Ring
for n, i, j being Nat st [i,j] in Indices (canMat (i,j,n,R)) holds
for A being Matrix of n,R
for i2, j2 being Nat st [i2,j2] in Indices A holds
( ( i = i2 implies ((canMat (i,j,n,R)) * A) * (i2,j2) = A * (j,j2) ) & ( i <> i2 implies ((canMat (i,j,n,R)) * A) * (i2,j2) = 0. R ) )