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

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

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

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

Trace ((M1 + M2) - M3) = (Trace (M1 + M2)) - (Trace M3) by Th59

.= ((Trace M1) + (Trace M2)) - (Trace M3) by Th53 ;

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

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

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

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

Trace ((M1 + M2) - M3) = (Trace (M1 + M2)) - (Trace M3) by Th59

.= ((Trace M1) + (Trace M2)) - (Trace M3) by Th53 ;

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