theorem Th43: :: MATGRP_0:32

for R being Ring
for i, k, I, K being Nat holds
( len (canMat (i,k,I,K,R)) = I & ( I = 0 implies width (canMat (i,k,I,K,R)) = 0 ) & ( I <> 0 implies width (canMat (i,k,I,K,R)) = K ) ) by MATRIX_0:22, MATRIX_0:23, MATRIX_0:25;