defpred S1[ 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 S1[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: S1[ 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 S1[k] holds
k <= len M
proof
let k be Nat; :: thesis: ( S1[k] implies k <= len M )
A5: card (Seg (len M)) = len M by FINSEQ_1:57;
assume S1[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: S1[k] and
A10: for n being Nat st S1[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