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: ( diagonal_of_Matrix M1 is FinSequence of K & len (diagonal_of_Matrix M1) = n & diagonal_of_Matrix M2 is FinSequence of K & len (diagonal_of_Matrix M2) = n & diagonal_of_Matrix (M1 + M2) is FinSequence of K & len (diagonal_of_Matrix (M1 + M2)) = n ) by MATRIX_3:def 10;
then A2: ( dom (diagonal_of_Matrix M1) = Seg n & dom (diagonal_of_Matrix M2) = Seg n & dom (diagonal_of_Matrix (M1 + M2)) = Seg n ) by FINSEQ_1:def 3;
then A3: dom ((diagonal_of_Matrix M1) + (diagonal_of_Matrix M2)) = Seg n by POLYNOM1:5;
for i being Nat st i in dom (diagonal_of_Matrix M1) holds
((diagonal_of_Matrix M1) + (diagonal_of_Matrix M2)) . i = (diagonal_of_Matrix (M1 + M2)) . i

proof

let i be Nat; :: thesis: ( i in dom (diagonal_of_Matrix M1) implies ((diagonal_of_Matrix M1) + (diagonal_of_Matrix M2)) . i = (diagonal_of_Matrix (M1 + M2)) . i )
assume i in dom (diagonal_of_Matrix M1) ; :: thesis: ((diagonal_of_Matrix M1) + (diagonal_of_Matrix M2)) . i = (diagonal_of_Matrix (M1 + M2)) . i
then A4: i in Seg n by A1, FINSEQ_1:def 3;
Indices M1 = [:(Seg n),(Seg n):] by MATRIX_1:25;
then A5: [i,i] in Indices M1 by A4, ZFMISC_1:106;
A6: ( (diagonal_of_Matrix M1) . i = M1 * i,i & (diagonal_of_Matrix M2) . i = M2 * i,i & (diagonal_of_Matrix (M1 + M2)) . i = (M1 + M2) * i,i ) by A4, MATRIX_3:def 10;
then ((diagonal_of_Matrix M1) + (diagonal_of_Matrix M2)) . i = (M1 * i,i) + (M2 * i,i) by A3, A4, FUNCOP_1:28
.= (diagonal_of_Matrix (M1 + M2)) . i by A5, A6, MATRIX_3:def 3 ;
hence ((diagonal_of_Matrix M1) + (diagonal_of_Matrix M2)) . i = (diagonal_of_Matrix (M1 + M2)) . i ; :: thesis: verum

end;

then Trace (M1 + M2) = Sum ((diagonal_of_Matrix M1) + (diagonal_of_Matrix M2)) by A2, A3, FINSEQ_1:17
.= (Sum (diagonal_of_Matrix M1)) + (Sum (diagonal_of_Matrix M2)) by A1, MATRIX_4:61 ;
hence Trace (M1 + M2) = (Trace M1) + (Trace M2) ; :: thesis: verum