let n be Nat; :: thesis: for K being Field holds Trace (0. K,n) = 0. K
let K be Field; :: thesis: Trace (0. K,n) = 0. K
len (diagonal_of_Matrix (0. K,n)) = n by MATRIX_3:def 10;
then A1: dom (diagonal_of_Matrix (0. K,n)) = Seg n by FINSEQ_1:def 3;
for i being Nat st i in dom (diagonal_of_Matrix (0. K,n)) holds
(diagonal_of_Matrix (0. K,n)) /. i = 0. K

proof

let i be Nat; :: thesis: ( i in dom (diagonal_of_Matrix (0. K,n)) implies (diagonal_of_Matrix (0. K,n)) /. i = 0. K )
assume A2: i in dom (diagonal_of_Matrix (0. K,n)) ; :: thesis: (diagonal_of_Matrix (0. K,n)) /. i = 0. K
Indices (0. K,n) = [:(Seg n),(Seg n):] by MATRIX_1:25;
then [i,i] in Indices (0. K,n,n) by A1, A2, ZFMISC_1:106;
then A3: (0. K,n) * i,i = 0. K by MATRIX_3:3;
(diagonal_of_Matrix (0. K,n)) . i = (0. K,n) * i,i by A1, A2, MATRIX_3:def 10;
hence (diagonal_of_Matrix (0. K,n)) /. i = 0. K by A2, A3, PARTFUN1:def 8; :: thesis: verum

end;

hence Trace (0. K,n) = 0. K by MATRLIN:15; :: thesis: verum