theorem Th44: :: MATGRP_0:33

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