theorem Th111: :: MATRIX13:111

for n being Nat
for K being Field
for M being diagonal Matrix of n,K st the_rank_of M = n holds
lines M is Basis of (n -VectSp_over K)