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 holds
M * i,j = 0. K ) holds
M * R is Upper_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 holds
M * i,j = 0. K ) holds
M * R is Upper_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 holds
M * i,j = 0. K ) holds
M * R is Upper_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 holds
M * i,j = 0. K ) implies M * R is Upper_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 holds
M * i,j = 0. K ; :: thesis: M * R is Upper_Triangular_Matrix of n,K
set MR = M * R;
set I = idseq n;

now

let i, j be Nat; :: thesis: ( [i,j] in Indices (M * R) & i > j implies (M * R) * i,j = 0. K )
assume A4: ( [i,j] in Indices (M * R) & i > j ) ; :: thesis: (M * R) * i,j = 0. K
reconsider i' = i as Element of NAT by ORDINAL1:def 13;
A5: ( Indices (M * R) = [:(Seg n),(Seg n):] & Indices M = [:(Seg n),(Seg n):] ) by MATRIX_1:25;
then A6: ( i in Seg n & j in Seg n & [i,j] in Indices M ) by A4, ZFMISC_1:106;
then i <= n by FINSEQ_1:3;
then reconsider ni = (n - i') + 1 as Element of NAT by FINSEQ_5:1;
(n + 1) - i < (n + 1) - j by A4, XREAL_1:17;
then ni + j < ((n + 1) - j) + j by XREAL_1:10;
then ( ni in Seg n & dom (idseq n) = Seg (len (idseq n)) & len (idseq n) = n & ni + j <= n ) by A6, FINSEQ_1:def 3, FINSEQ_1:def 18, FINSEQ_5:2, NAT_1:13;
then ( R . i = (idseq n) . ni & (idseq n) . ni = ni & M * ni,j = 0. K ) by A1, A2, A6, FINSEQ_5:61, FUNCT_1:34;
hence (M * R) * i,j = 0. K by A4, A5, MATRIX11:def 4; :: thesis: verum

end;

hence M * R is Upper_Triangular_Matrix of n,K by MATRIX_2:def 3; :: thesis: verum