theorem Th55: :: MATGRP_0:43

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
( ( j = j2 implies (A * (canMat (i,j,n,R))) * (i2,j2) = A * (i2,i) ) & ( j <> j2 implies (A * (canMat (i,j,n,R))) * (i2,j2) = 0. R ) )