let R be Ring; :: thesis: for n, i, j being Nat st i < j holds
canMat (i,j,n,R) is upper_triangular
let n be Nat; :: thesis: for i, j being Nat st i < j holds
canMat (i,j,n,R) is upper_triangular
let i, j be Nat; :: thesis: ( i < j implies canMat (i,j,n,R) is upper_triangular )
assume A1: i < j ; :: thesis: canMat (i,j,n,R) is upper_triangular
let i9, j9 be Nat; :: according to MATRIX_1:def 12 :: thesis: ( not [i9,j9] in Indices (canMat (i,j,n,R)) or i9 <= j9 or (canMat (i,j,n,R)) * (i9,j9) = 0. R )
assume A2: [i9,j9] in Indices (canMat (i,j,n,R)) ; :: thesis: ( i9 <= j9 or (canMat (i,j,n,R)) * (i9,j9) = 0. R )
assume i9 > j9 ; :: thesis: (canMat (i,j,n,R)) * (i9,j9) = 0. R
then ( i9 = i implies not j9 = j ) by A1;
then [i,j] <> [i9,j9] by XTUPLE_0:1;
hence (canMat (i,j,n,R)) * (i9,j9) = 0. R by A2, Def1; :: thesis: verum