theorem :: MATRIX13:66

for K being Field
for M being Matrix of K
for P1, Q, Q1 being finite without_zero Subset of NAT st card P1 = card Q1 & Q c= Q1 & Det (EqSegm (M,P1,Q1)) <> 0. K holds
ex P being finite without_zero Subset of NAT st
( P c= P1 & card P = card Q & Det (EqSegm (M,P,Q)) <> 0. K )