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

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

hence
Trace (0. (K,n)) = 0. K
by MATRLIN:11; :: thesis: verum
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;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