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

for M1, M2 being Matrix of n,K holds Trace (M1 - M2) = (Trace M1) - (Trace M2)

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

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

Trace (M1 - M2) = (Trace M1) + (Trace (- M2)) by Th53

.= (Trace M1) + (- (Trace M2)) by Th56 ;

hence Trace (M1 - M2) = (Trace M1) - (Trace M2) ; :: thesis: verum

for M1, M2 being Matrix of n,K holds Trace (M1 - M2) = (Trace M1) - (Trace M2)

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

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

Trace (M1 - M2) = (Trace M1) + (Trace (- M2)) by Th53

.= (Trace M1) + (- (Trace M2)) by Th56 ;

hence Trace (M1 - M2) = (Trace M1) - (Trace M2) ; :: thesis: verum