theorem Th45: :: MATGRP_0:34

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