let R be Ring; :: thesis: for n, i, j being Nat st i > j holds
for r being Element of R holds (1. (R,n)) + (r * (canMat (i,j,n,R))) is lower_triangular
let n be Nat; :: thesis: for i, j being Nat st i > j holds
for r being Element of R holds (1. (R,n)) + (r * (canMat (i,j,n,R))) is lower_triangular
let i, j be Nat; :: thesis: ( i > j implies for r being Element of R holds (1. (R,n)) + (r * (canMat (i,j,n,R))) is lower_triangular )
assume A1: i > j ; :: thesis: for r being Element of R holds (1. (R,n)) + (r * (canMat (i,j,n,R))) is lower_triangular
let r be Element of R; :: thesis: (1. (R,n)) + (r * (canMat (i,j,n,R))) is lower_triangular
set M = (1. (R,n)) + (r * (canMat (i,j,n,R)));
let i9, j9 be Nat; :: according to MATRIX_1:def 13 :: thesis: ( not [i9,j9] in Indices ((1. (R,n)) + (r * (canMat (i,j,n,R)))) or j9 <= i9 or ((1. (R,n)) + (r * (canMat (i,j,n,R)))) * (i9,j9) = 0. R )
assume A2: [i9,j9] in Indices ((1. (R,n)) + (r * (canMat (i,j,n,R)))) ; :: thesis: ( j9 <= i9 or ((1. (R,n)) + (r * (canMat (i,j,n,R)))) * (i9,j9) = 0. R )
assume A3: i9 < j9 ; :: thesis: ((1. (R,n)) + (r * (canMat (i,j,n,R)))) * (i9,j9) = 0. R
A4: [i9,j9] in Indices (1. (R,n)) by A2, MATRIX_0:26;
A5: [i9,j9] in Indices (r * (canMat (i,j,n,R))) by A2, MATRIX_0:26;
A6: r * (canMat (i,j,n,R)) is lower_triangular by A1, Th62;
thus ((1. (R,n)) + (r * (canMat (i,j,n,R)))) * (i9,j9) = ((1. (R,n)) * (i9,j9)) + ((r * (canMat (i,j,n,R))) * (i9,j9)) by A4, MATRIX_1:def 8
.= ((1. (R,n)) * (i9,j9)) + (0. R) by A3, A5, A6
.= 0. R by A3, A4, MATRIX_1:def 3 ; :: thesis: verum