defpred S₁[ Nat] means ex P, Q being finite without_zero Subset of NAT st
( [:P,Q:] c= Indices M & card P = card Q & card Q = $1 & Det (EqSegm (M,P,Q)) <> 0. K );
A1: ex k being Nat st S₁[k]

proof

set E = the empty finite without_zero Subset of NAT;
reconsider E = the empty finite without_zero Subset of NAT as finite without_zero Subset of NAT ;
take card E ; :: thesis: S₁[ card E]
take E ; :: thesis: ex Q being finite without_zero Subset of NAT st
( [:E,Q:] c= Indices M & card E = card Q & card Q = card E & Det (EqSegm (M,E,Q)) <> 0. K )
take E ; :: thesis: ( [:E,E:] c= Indices M & card E = card E & card E = card E & Det (EqSegm (M,E,E)) <> 0. K )
A2: E c= Seg (len M) ;
A3: E c= Seg (width M) ;
Det (EqSegm (M,E,E)) = 1_ K by MATRIXR2:41;
hence ( [:E,E:] c= Indices M & card E = card E & card E = card E & Det (EqSegm (M,E,E)) <> 0. K ) by A2, A3, Th67; :: thesis: verum

end;

A4: for k being Nat st S₁[k] holds
k <= len M

proof

let k be Nat; :: thesis: ( S₁[k] implies k <= len M )
A5: card (Seg (len M)) = len M by FINSEQ_1:57;
assume S₁[k] ; :: thesis: k <= len M
then consider P, Q being finite without_zero Subset of NAT such that
A6: [:P,Q:] c= Indices M and
A7: card P = card Q and
A8: card Q = k and
Det (EqSegm (M,P,Q)) <> 0. K ;
P c= Seg (len M) by A6, A7, Th67;
hence k <= len M by A7, A8, A5, NAT_1:43; :: thesis: verum

end;

consider k being Nat such that
A9: S₁[k] and
A10: for n being Nat st S₁[n] holds
n <= k from NAT_1:sch 6(A4, A1);
take k ; :: thesis: ( k is Element of NAT & ex P, Q being finite without_zero Subset of NAT st
( [:P,Q:] c= Indices M & card P = card Q & card P = k & Det (EqSegm (M,P,Q)) <> 0. K ) & ( for P1, Q1 being finite without_zero Subset of NAT st [:P1,Q1:] c= Indices M & card P1 = card Q1 & Det (EqSegm (M,P1,Q1)) <> 0. K holds
card P1 <= k ) )
thus ( k is Element of NAT & ex P, Q being finite without_zero Subset of NAT st
( [:P,Q:] c= Indices M & card P = card Q & card P = k & Det (EqSegm (M,P,Q)) <> 0. K ) & ( for P1, Q1 being finite without_zero Subset of NAT st [:P1,Q1:] c= Indices M & card P1 = card Q1 & Det (EqSegm (M,P1,Q1)) <> 0. K holds
card P1 <= k ) ) by A9, A10; :: thesis: verum