let n be Nat; :: thesis: for K being Field
for M1 being Matrix of n,K st M1 is Upper_Triangular_Matrix of n,K & M1 is Lower_Triangular_Matrix of n,K & n > 0 holds
M1 is symmetric
let K be Field; :: thesis: for M1 being Matrix of n,K st M1 is Upper_Triangular_Matrix of n,K & M1 is Lower_Triangular_Matrix of n,K & n > 0 holds
M1 is symmetric
let M1 be Matrix of n,K; :: thesis: ( M1 is Upper_Triangular_Matrix of n,K & M1 is Lower_Triangular_Matrix of n,K & n > 0 implies M1 is symmetric )
assume A1: ( M1 is Upper_Triangular_Matrix of n,K & M1 is Lower_Triangular_Matrix of n,K & n > 0 ) ; :: thesis: M1 is symmetric
A2: ( M1 is Matrix of n,K & width M1 = n & len M1 = n & Indices M1 = [:(Seg n),(Seg n):] ) by MATRIX_1:25;
for i, j being Nat st [i,j] in Indices M1 holds
(M1 @ ) * i,j = M1 * i,j

proof

let i, j be Nat; :: thesis: ( [i,j] in Indices M1 implies (M1 @ ) * i,j = M1 * i,j )
assume A3: [i,j] in Indices M1 ; :: thesis: (M1 @ ) * i,j = M1 * i,j
then [i,j] in [:(Seg n),(Seg n):] by MATRIX_1:25;
then ( i in Seg n & j in Seg n ) by ZFMISC_1:106;
then A4: [j,i] in Indices M1 by A2, ZFMISC_1:106;

per cases ( i = j or i <> j ) ;

suppose i = j ; :: thesis: (M1 @ ) * i,j = M1 * i,j

hence (M1 @ ) * i,j = M1 * i,j by A4, MATRIX_1:def 7; :: thesis: verum

end;

suppose A5: i <> j ; :: thesis: (M1 @ ) * i,j = M1 * i,j

per cases ( i < j or i > j ) by A5, XXREAL_0:1;

suppose A6: i < j ; :: thesis: (M1 @ ) * i,j = M1 * i,j

then A7: M1 * i,j = 0. K by A1, A3, MATRIX_2:def 4;
M1 * j,i = 0. K by A1, A4, A6, MATRIX_2:def 3;
hence (M1 @ ) * i,j = M1 * i,j by A4, A7, MATRIX_1:def 7; :: thesis: verum

end;

suppose A8: i > j ; :: thesis: (M1 @ ) * i,j = M1 * i,j

then A9: M1 * i,j = 0. K by A1, A3, MATRIX_2:def 3;
M1 * j,i = 0. K by A1, A4, A8, MATRIX_2:def 4;
hence (M1 @ ) * i,j = M1 * i,j by A4, A9, MATRIX_1:def 7; :: thesis: verum

end;

end;

end;

end;

end;

then M1 @ = M1 by MATRIX_1:28;
hence M1 is symmetric by Def5; :: thesis: verum