let n be Nat; :: thesis: for K being Field
for nt1, nt2 being Element of n -tuples_on NAT
for M being Matrix of K st [:(rng nt1),(rng nt2):] c= Indices M & Det (Segm (M,nt1,nt2)) <> 0. K holds
ex P1, P2 being finite without_zero Subset of NAT st
( P1 = rng nt1 & P2 = rng nt2 & card P1 = card P2 & card P1 = n & Det (EqSegm (M,P1,P2)) <> 0. K )
let K be Field; :: thesis: for nt1, nt2 being Element of n -tuples_on NAT
for M being Matrix of K st [:(rng nt1),(rng nt2):] c= Indices M & Det (Segm (M,nt1,nt2)) <> 0. K holds
ex P1, P2 being finite without_zero Subset of NAT st
( P1 = rng nt1 & P2 = rng nt2 & card P1 = card P2 & card P1 = n & Det (EqSegm (M,P1,P2)) <> 0. K )
let nt1, nt2 be Element of n -tuples_on NAT; :: thesis: for M being Matrix of K st [:(rng nt1),(rng nt2):] c= Indices M & Det (Segm (M,nt1,nt2)) <> 0. K holds
ex P1, P2 being finite without_zero Subset of NAT st
( P1 = rng nt1 & P2 = rng nt2 & card P1 = card P2 & card P1 = n & Det (EqSegm (M,P1,P2)) <> 0. K )
let M be Matrix of K; :: thesis: ( [:(rng nt1),(rng nt2):] c= Indices M & Det (Segm (M,nt1,nt2)) <> 0. K implies ex P1, P2 being finite without_zero Subset of NAT st
( P1 = rng nt1 & P2 = rng nt2 & card P1 = card P2 & card P1 = n & Det (EqSegm (M,P1,P2)) <> 0. K ) )
assume that
A1: [:(rng nt1),(rng nt2):] c= Indices M and
A2: Det (Segm (M,nt1,nt2)) <> 0. K ; :: thesis: ex P1, P2 being finite without_zero Subset of NAT st
( P1 = rng nt1 & P2 = rng nt2 & card P1 = card P2 & card P1 = n & Det (EqSegm (M,P1,P2)) <> 0. K )
( n = 0 iff n = 0 ) ;
then consider P1, P2 being finite without_zero Subset of NAT such that
A3: P1 = rng nt1 and
A4: P2 = rng nt2 by A1, Lm5;
nt2 is one-to-one by A2, Th31;
then A5: card P2 = len nt2 by A4, FINSEQ_4:62;
nt1 is one-to-one by A2, Th27;
then A6: card P1 = len nt1 by A3, FINSEQ_4:62;
then reconsider SP1 = Sgm P1, SP2 = Sgm P2 as Element of n -tuples_on NAT by A5, CARD_1:def 7;
ex m being Nat st P2 c= Seg m by Th43;
then A7: rng SP2 = P2 by FINSEQ_1:def 13;
ex k being Nat st P1 c= Seg k by Th43;
then rng SP1 = P1 by FINSEQ_1:def 13;
then A8: ( Det (Segm (M,nt1,nt2)) = Det (Segm (M,SP1,SP2)) or - (Det (Segm (M,nt1,nt2))) = Det (Segm (M,SP1,SP2)) ) by A3, A4, A7, Th36;
A9: len nt1 = n by CARD_1:def 7;
A10: len nt2 = n by CARD_1:def 7;
Segm (M,(Sgm P1),(Sgm P2)) = Segm (M,P1,P2)
.= EqSegm (M,P1,P2) by A6, A5, A9, A10, Def3 ;
hence ex P1, P2 being finite without_zero Subset of NAT st
( P1 = rng nt1 & P2 = rng nt2 & card P1 = card P2 & card P1 = n & Det (EqSegm (M,P1,P2)) <> 0. K ) by A2, A3, A4, A6, A5, A9, A10, A8, VECTSP_1:28; :: thesis: verum