let R be Ring; :: thesis: for I, K, i, k being Nat st not [i,k] in Indices (canMat (i,k,I,K,R)) holds
canMat (i,k,I,K,R) = 0. (R,I,K)
let I, K, i, k be Nat; :: thesis: ( not [i,k] in Indices (canMat (i,k,I,K,R)) implies canMat (i,k,I,K,R) = 0. (R,I,K) )
assume A1: not [i,k] in Indices (canMat (i,k,I,K,R)) ; :: thesis: canMat (i,k,I,K,R) = 0. (R,I,K)
for i2, k2 being Nat st [i2,k2] in Indices (canMat (i,k,I,K,R)) holds
(canMat (i,k,I,K,R)) * (i2,k2) = (0. (R,I,K)) * (i2,k2)

proof

let i2, k2 be Nat; :: thesis: ( [i2,k2] in Indices (canMat (i,k,I,K,R)) implies (canMat (i,k,I,K,R)) * (i2,k2) = (0. (R,I,K)) * (i2,k2) )
assume A2: [i2,k2] in Indices (canMat (i,k,I,K,R)) ; :: thesis: (canMat (i,k,I,K,R)) * (i2,k2) = (0. (R,I,K)) * (i2,k2)
then A3: [i2,k2] in Indices (0. (R,I,K)) by MATRIX_0:26;

per cases ( i <> i2 or k <> k2 ) by A1, A2;

suppose i <> i2 ; :: thesis: (canMat (i,k,I,K,R)) * (i2,k2) = (0. (R,I,K)) * (i2,k2)

hence (canMat (i,k,I,K,R)) * (i2,k2) = 0. R by A2, Th40
.= (0. (R,I,K)) * (i2,k2) by A3, MATRIX_3:1 ;
:: thesis: verum

end;

suppose k <> k2 ; :: thesis: (canMat (i,k,I,K,R)) * (i2,k2) = (0. (R,I,K)) * (i2,k2)

hence (canMat (i,k,I,K,R)) * (i2,k2) = 0. R by A2, Th40
.= (0. (R,I,K)) * (i2,k2) by A3, MATRIX_3:1 ;
:: thesis: verum

end;

end;

end;

hence canMat (i,k,I,K,R) = 0. (R,I,K) by MATRIX_0:27; :: thesis: verum