:: deftheorem defines diagonal_of_Matrix MATRIX_3:def 10 :
for n being Nat
for K being Ring
for M being Matrix of n,K
for b₄ being FinSequence of K holds
( b₄ = diagonal_of_Matrix M iff ( len b₄ = n & ( for i being Nat st i in Seg n holds
b₄ . i = M * (i,i) ) ) );