let n be Nat; :: thesis: for K being Field
for M1 being Matrix of n,K holds Trace (- M1) = - (Trace M1)
let K be Field; :: thesis: for M1 being Matrix of n,K holds Trace (- M1) = - (Trace M1)
let M1 be Matrix of n,K; :: thesis: Trace (- M1) = - (Trace M1)
A1: ( len M1 = n & width M1 = n ) by MATRIX_0:24;
(Trace M1) + (Trace (- M1)) = Trace (M1 + (- M1)) by Th53
.= Trace (0. (K,n,n)) by A1, MATRIX_4:2
.= Trace (0. (K,n))
.= 0. K by Th55 ;
hence Trace (- M1) = - (Trace M1) by RLVECT_1:6; :: thesis: verum