theorem Th100: :: MATRIX13:100

for K being Field
for M being diagonal Matrix of K
for P being finite without_zero Subset of NAT st [:P,P:] c= Indices M holds
Segm (M,P,P) is V185(b₁)