let n be Nat; for K being Field holds Trace (0. (K,n)) = 0. K
let K be Field; 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;
( 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)))
;
(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;
verum
end;
hence
Trace (0. (K,n)) = 0. K
by MATRLIN:11; verum