let R be Ring; :: thesis: for n, i, j being Nat st i < j holds
for r being Element of R holds (canMat (i,j,n,R)) * r is upper_triangular
let n be Nat; :: thesis: for i, j being Nat st i < j holds
for r being Element of R holds (canMat (i,j,n,R)) * r is upper_triangular
let i, j be Nat; :: thesis: ( i < j implies for r being Element of R holds (canMat (i,j,n,R)) * r is upper_triangular )
assume A1: i < j ; :: thesis: for r being Element of R holds (canMat (i,j,n,R)) * r is upper_triangular
let r be Element of R; :: thesis: (canMat (i,j,n,R)) * 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)) * r) or i9 <= j9 or ((canMat (i,j,n,R)) * r) * (i9,j9) = 0. R )
assume A2: [i9,j9] in Indices ((canMat (i,j,n,R)) * r) ; :: thesis: ( i9 <= j9 or ((canMat (i,j,n,R)) * r) * (i9,j9) = 0. R )
assume A3: i9 > j9 ; :: thesis: ((canMat (i,j,n,R)) * r) * (i9,j9) = 0. R
A4: [i9,j9] in Indices (canMat (i,j,n,R)) by A2, MATRIX_0:26;
thus ((canMat (i,j,n,R)) * r) * (i9,j9) = ((canMat (i,j,n,R)) * (i9,j9)) * r by A4, MATRIX_3:def 6
.= (0. R) * r by A1, A3, A4, Th61, MATRIX_1:def 12
.= 0. R ; :: thesis: verum