theorem Th55: :: MATRIX_8:55
for n being Nat
for K being Field holds Trace (0. (K,n)) = 0. K