let n be Nat; :: thesis: for K being Field
for M being Matrix of n,K holds
( M is lower_triangular Matrix of n,K iff M @ is upper_triangular Matrix of n,K )
let K be Field; :: thesis: for M being Matrix of n,K holds
( M is lower_triangular Matrix of n,K iff M @ is upper_triangular Matrix of n,K )
let M be Matrix of n,K; :: thesis: ( M is lower_triangular Matrix of n,K iff M @ is upper_triangular Matrix of n,K )
thus ( M is lower_triangular Matrix of n,K implies M @ is upper_triangular Matrix of n,K ) :: thesis: ( M @ is upper_triangular Matrix of n,K implies M is lower_triangular Matrix of n,K )

proof

assume A1: M is lower_triangular Matrix of n,K ; :: thesis: M @ is upper_triangular Matrix of n,K

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

let i, j be Nat; :: thesis: ( [i,j] in Indices (M @) & i > j implies (M @) * (i,j) = 0. K )
assume that
A2: [i,j] in Indices (M @) and
A3: i > j ; :: thesis: (M @) * (i,j) = 0. K
A4: [j,i] in Indices M by A2, MATRIX_0:def 6;
then M * (j,i) = 0. K by A1, A3, MATRIX_1:def 9;
hence (M @) * (i,j) = 0. K by A4, MATRIX_0:def 6; :: thesis: verum

end;

hence M @ is upper_triangular Matrix of n,K by MATRIX_1:def 8; :: thesis: verum

end;

assume A5: M @ is upper_triangular Matrix of n,K ; :: thesis: M is lower_triangular Matrix of n,K

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

let i, j be Nat; :: thesis: ( [i,j] in Indices M & i < j implies M * (i,j) = 0. K )
assume that
A6: [i,j] in Indices M and
A7: i < j ; :: thesis: M * (i,j) = 0. K
[j,i] in Indices (M @) by A6, MATRIX_0:def 6;
then (M @) * (j,i) = 0. K by A5, A7, MATRIX_1:def 8;
hence M * (i,j) = 0. K by A6, MATRIX_0:def 6; :: thesis: verum

end;

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