let n be Nat; :: thesis: for K being Field

for M1 being Matrix of n,K holds Trace (M1 + (- M1)) = 0. K

let K be Field; :: thesis: for M1 being Matrix of n,K holds Trace (M1 + (- M1)) = 0. K

let M1 be Matrix of n,K; :: thesis: Trace (M1 + (- M1)) = 0. K

( len M1 = n & width M1 = n ) by MATRIX_0:24;

then Trace (M1 + (- M1)) = Trace (0. (K,n,n)) by MATRIX_4:2

.= Trace (0. (K,n))

.= 0. K by Th55 ;

hence Trace (M1 + (- M1)) = 0. K ; :: thesis: verum

for M1 being Matrix of n,K holds Trace (M1 + (- M1)) = 0. K

let K be Field; :: thesis: for M1 being Matrix of n,K holds Trace (M1 + (- M1)) = 0. K

let M1 be Matrix of n,K; :: thesis: Trace (M1 + (- M1)) = 0. K

( len M1 = n & width M1 = n ) by MATRIX_0:24;

then Trace (M1 + (- M1)) = Trace (0. (K,n,n)) by MATRIX_4:2

.= Trace (0. (K,n))

.= 0. K by Th55 ;

hence Trace (M1 + (- M1)) = 0. K ; :: thesis: verum