let n be Nat; :: thesis: for K being Field
for M being Matrix of n,K
for R being Permutation of (Seg n) st R = Rev (idseq n) & ( for i, j being Nat st i in Seg n & j in Seg n & i + j > n + 1 holds
M * (i,j) = 0. K ) holds
M * R is lower_triangular Matrix of n,K
let K be Field; :: thesis: for M being Matrix of n,K
for R being Permutation of (Seg n) st R = Rev (idseq n) & ( for i, j being Nat st i in Seg n & j in Seg n & i + j > n + 1 holds
M * (i,j) = 0. K ) holds
M * R is lower_triangular Matrix of n,K
let M be Matrix of n,K; :: thesis: for R being Permutation of (Seg n) st R = Rev (idseq n) & ( for i, j being Nat st i in Seg n & j in Seg n & i + j > n + 1 holds
M * (i,j) = 0. K ) holds
M * R is lower_triangular Matrix of n,K
let R be Permutation of (Seg n); :: thesis: ( R = Rev (idseq n) & ( for i, j being Nat st i in Seg n & j in Seg n & i + j > n + 1 holds
M * (i,j) = 0. K ) implies M * R is lower_triangular Matrix of n,K )
assume that
A1: R = Rev (idseq n) and
A2: for i, j being Nat st i in Seg n & j in Seg n & i + j > n + 1 holds
M * (i,j) = 0. K ; :: thesis: M * R is lower_triangular Matrix of n,K
set I = idseq n;
set MR = M * R;

now :: thesis: for i, j being Nat st [i,j] in Indices (M * R) & i < j holds
(M * R) * (i,j) = 0. K

let i, j be Nat; :: thesis: ( [i,j] in Indices (M * R) & i < j implies (M * R) * (i,j) = 0. K )
assume that
A3: [i,j] in Indices (M * R) and
A4: i < j ; :: thesis: (M * R) * (i,j) = 0. K
reconsider i9 = i as Element of NAT by ORDINAL1:def 12;
A5: Indices (M * R) = [:(Seg n),(Seg n):] by MATRIX_0:24;
then A6: i in Seg n by A3, ZFMISC_1:87;
then i <= n by FINSEQ_1:1;
then reconsider ni = (n - i9) + 1 as Element of NAT by FINSEQ_5:1;
(n + 1) - i > (n + 1) - j by A4, XREAL_1:15;
then A7: ni + j > ((n + 1) - j) + j by XREAL_1:8;
A8: len (idseq n) = n by CARD_1:def 7;
A9: Indices M = [:(Seg n),(Seg n):] by MATRIX_0:24;
A10: ni in Seg n by A6, FINSEQ_5:2;
then A11: (idseq n) . ni = ni by FUNCT_1:17;
j in Seg n by A3, A5, ZFMISC_1:87;
then A12: M * (ni,j) = 0. K by A2, A7, A10;
dom (idseq n) = Seg (len (idseq n)) by FINSEQ_1:def 3;
then R . i = (idseq n) . ni by A1, A6, A8, FINSEQ_5:58;
hence (M * R) * (i,j) = 0. K by A3, A5, A9, A11, A12, MATRIX11:def 4; :: thesis: verum

end;

hence M * R is lower_triangular Matrix of n,K by MATRIX_1:def 9; :: thesis: verum