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

consider E being empty finite without_zero Subset of NAT ;
reconsider E = E as finite without_zero Subset of NAT ;
take C = card E; :: thesis: S₁[C]
take P = E; :: thesis: ex Q being finite without_zero Subset of NAT st
( [:P,Q:] c= Indices M & card P = card Q & card Q = C & Det (EqSegm M,P,Q) <> 0. K )
take Q = E; :: thesis: ( [:P,Q:] c= Indices M & card P = card Q & card Q = C & Det (EqSegm M,P,Q) <> 0. K )
A2: E c= Seg (len M) by XBOOLE_1:2;
A3: E c= Seg (width M) by XBOOLE_1:2;
Det (EqSegm M,E,E) = 1_ K by CARD_1:47, MATRIXR2:41;
hence ( [:P,Q:] c= Indices M & card P = card Q & card Q = C & Det (EqSegm M,P,Q) <> 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:78;
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:44; :: 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