let R be Ring; :: thesis: for I, i, j1, j2, k being Nat st j1 <> j2 holds
(canMat (i,j1,I,R)) * (canMat (j2,k,I,R)) = 0. (R,I)
let I, i, j1, j2, k be Nat; :: thesis: ( j1 <> j2 implies (canMat (i,j1,I,R)) * (canMat (j2,k,I,R)) = 0. (R,I) )
assume A1: j1 <> j2 ; :: thesis: (canMat (i,j1,I,R)) * (canMat (j2,k,I,R)) = 0. (R,I)
set LHS = (canMat (i,j1,I,R)) * (canMat (j2,k,I,R));

per cases ( I = 0 or I <> 0 ) ;

suppose I = 0 ; :: thesis: (canMat (i,j1,I,R)) * (canMat (j2,k,I,R)) = 0. (R,I)

then for i9, j9 being Nat st [i9,j9] in Indices ((canMat (i,j1,I,R)) * (canMat (j2,k,I,R))) holds
((canMat (i,j1,I,R)) * (canMat (j2,k,I,R))) * (i9,j9) = (0. (R,I)) * (i9,j9) by MATRIX_0:22;
hence (canMat (i,j1,I,R)) * (canMat (j2,k,I,R)) = 0. (R,I) by MATRIX_0:27; :: thesis: verum

end;

suppose A3: I <> 0 ; :: thesis: (canMat (i,j1,I,R)) * (canMat (j2,k,I,R)) = 0. (R,I)

0. (R,I) = 0. (R,I,I) ;
hence (canMat (i,j1,I,R)) * (canMat (j2,k,I,R)) = 0. (R,I) by A1, A3, Th46; :: thesis: verum

end;

end;