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

proof

assume i <> i2 ; :: thesis: (canMat (i,k,I,K,R)) * (i2,k2) = 0. R
then [i,k] <> [i2,k2] by XTUPLE_0:1;
hence (canMat (i,k,I,K,R)) * (i2,k2) = 0. R by A1, Def1; :: thesis: verum

end;

thus ( k <> k2 implies (canMat (i,k,I,K,R)) * (i2,k2) = 0. R ) :: thesis: ( i = i2 & k = k2 implies (canMat (i,k,I,K,R)) * (i2,k2) = 1. R )

proof

assume k <> k2 ; :: thesis: (canMat (i,k,I,K,R)) * (i2,k2) = 0. R
then [i,k] <> [i2,k2] by XTUPLE_0:1;
hence (canMat (i,k,I,K,R)) * (i2,k2) = 0. R by A1, Def1; :: thesis: verum

end;

assume ( i = i2 & k = k2 ) ; :: thesis: (canMat (i,k,I,K,R)) * (i2,k2) = 1. R
hence (canMat (i,k,I,K,R)) * (i2,k2) = 1. R by A1, Def1; :: thesis: verum