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_0:24;
then [i,i] in Indices (0. (K,n,n)) by A1, A2, ZFMISC_1:87;
then A3: (0. (K,n)) * (i,i) = 0. K by MATRIX_3:1;
(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 6; :: thesis: verum
end;
hence Trace (0. (K,n)) = 0. K by MATRLIN:11; :: thesis: verum