let K be Field; :: thesis: for n being Nat
for M1 being Matrix of n,K st M1 is symmetric holds
- M1 is symmetric
let n be Nat; :: thesis: for M1 being Matrix of n,K st M1 is symmetric holds
- M1 is symmetric
let M1 be Matrix of n,K; :: thesis: ( M1 is symmetric implies - M1 is symmetric )
assume A1: M1 is symmetric ; :: thesis: - M1 is symmetric
(- M1) @ = - (M1 @ ) by Th27
.= - M1 by A1, Def5 ;
hence - M1 is symmetric by Def5; :: thesis: verum