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