let R be Ring; :: thesis: for n, i, j being Nat st not [i,j] in Indices (canMat (i,j,n,R)) holds
canMat (i,j,n,R) = 0. (R,n)
let n be Nat; :: thesis: for i, j being Nat st not [i,j] in Indices (canMat (i,j,n,R)) holds
canMat (i,j,n,R) = 0. (R,n)
0. (R,n,n) = 0. (R,n) ;
hence for i, j being Nat st not [i,j] in Indices (canMat (i,j,n,R)) holds
canMat (i,j,n,R) = 0. (R,n) by Th41; :: thesis: verum