theorem Th30: :: MATRIX13:30

for i, j, m being Nat
for K being Field
for mt, mt1 being Element of m -tuples_on NAT
for M being Matrix of K st i in Seg m & j in Seg m & mt . i = mt . j & i <> j holds
Det (Segm (M,mt1,mt)) = 0. K