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)
A1: len () = n by MATRIX_3:def 10;
then A2: dom () = Seg n by FINSEQ_1:def 3;
len (diagonal_of_Matrix (M1 + M2)) = n by MATRIX_3:def 10;
then A3: dom (diagonal_of_Matrix (M1 + M2)) = Seg n by FINSEQ_1:def 3;
A4: len () = n by MATRIX_3:def 10;
then dom () = Seg n by FINSEQ_1:def 3;
then A5: dom (() + ()) = Seg n by ;
for i being Nat st i in dom () holds
(() + ()) . i = (diagonal_of_Matrix (M1 + M2)) . i
proof
let i be Nat; :: thesis: ( i in dom () implies (() + ()) . i = (diagonal_of_Matrix (M1 + M2)) . i )
assume i in dom () ; :: thesis: (() + ()) . i = (diagonal_of_Matrix (M1 + M2)) . i
then A6: i in Seg n by ;
then A7: (diagonal_of_Matrix (M1 + M2)) . i = (M1 + M2) * (i,i) by MATRIX_3:def 10;
Indices M1 = [:(Seg n),(Seg n):] by MATRIX_0:24;
then A8: [i,i] in Indices M1 by ;
( (diagonal_of_Matrix M1) . i = M1 * (i,i) & () . i = M2 * (i,i) ) by ;
then (() + ()) . i = (M1 * (i,i)) + (M2 * (i,i)) by
.= (diagonal_of_Matrix (M1 + M2)) . i by ;
hence ((diagonal_of_Matrix M1) + ()) . i = (diagonal_of_Matrix (M1 + M2)) . i ; :: thesis: verum
end;
then Trace (M1 + M2) = Sum (() + ()) by
.= () + () by ;
hence Trace (M1 + M2) = (Trace M1) + (Trace M2) ; :: thesis: verum