let K be Field; :: thesis:
let M be Matrix of K; :: thesis:
let P1, Q, Q1 be finite without_zero Subset of NAT; :: thesis:
assume that
A1: card P1 = card Q1 and
A2: Q c= Q1 and
A3: Det (EqSegm (M,P1,Q1)) <> 0. K ; :: thesis:
defpred S₁[ Nat] means for Q being finite without_zero Subset of NAT st Q c= Q1 & card Q = $1 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 );
A4: for k being Element of NAT st k < card Q1 & S₁[k + 1] holds
S₁[k]

proof

let k be Element of NAT ; :: thesis:
assume that
A5: k < card Q1 and
A6: S₁[k + 1] ; :: thesis:
let Q be finite without_zero Subset of NAT; :: thesis:
assume that
A7: Q c= Q1 and
A8: card Q = k ; :: thesis:
Q c< Q1 by A5, A7, A8, XBOOLE_0:def 8;
then Q1 \ Q <> {} by XBOOLE_1:105;
then consider x being object such that
A9: x in Q1 \ Q by XBOOLE_0:def 1;
reconsider x = x as non zero Element of NAT by A9;
reconsider Qx = Q \/ {x} as finite without_zero Subset of NAT ;
A10: not x in Q by A9, XBOOLE_0:def 5;
then A11: card Qx = k + 1 by A8, CARD_2:41;
x in Q1 by A9, XBOOLE_0:def 5;
then {x} c= Q1 by ZFMISC_1:31;
then Qx c= Q1 by A7, XBOOLE_1:8;
then consider P2 being finite without_zero Subset of NAT such that
A12: P2 c= P1 and
A13: card Qx = card P2 and
A14: Det (EqSegm (M,P2,Qx)) <> 0. K by A6, A8, A10, CARD_2:41;
A15: (k + 1) -' 1 = (k + 1) - 1 by XREAL_0:def 2;
x in {x} by TARSKI:def 1;
then A16: x in Qx by XBOOLE_0:def 3;
A18: dom (Sgm Qx) = Seg (card Qx) by FINSEQ_3:40;
rng (Sgm Qx) = Qx by FINSEQ_1:def 14;
then consider j being object such that
A19: j in Seg (card Qx) and
A20: (Sgm Qx) . j = x by A18, A16, FUNCT_1:def 3;
set E = EqSegm (M,P2,Qx);
reconsider j = j as Element of NAT by A19;
consider i being Nat such that
A21: i in Seg (card Qx) and
A22: Det (Delete ((EqSegm (M,P2,Qx)),i,j)) <> 0. K by A13, A14, A19, Lm4;
take P = P2 \ {((Sgm P2) . i)}; :: thesis:
A23: P c= P2 by XBOOLE_1:36;
A24: Qx \ {x} = Q by A10, ZFMISC_1:117;
then card P = card Q by A13, A19, A20, A21, Th64;
hence ( P c= P1 & card P = card Q & Det (EqSegm (M,P,Q)) <> 0. K ) by A8, A11, A12, A13, A19, A20, A21, A22, A24, A23, A15, Th64; :: thesis:

end;

A25: S₁[ card Q1]

proof

let Q be finite without_zero Subset of NAT; :: thesis:
assume that
A26: Q c= Q1 and
A27: card Q = card Q1 ; :: thesis:
Q = Q1 by A26, A27, CARD_2:102;
hence ex P being finite without_zero Subset of NAT st
( P c= P1 & card P = card Q & Det (EqSegm (M,P,Q)) <> 0. K ) by A1, A3; :: thesis:

end;

for k being Element of NAT st k <= card Q1 holds
S₁[k] from PRE_POLY:sch 1(A25, A4);
hence ex P being finite without_zero Subset of NAT st
( P c= P1 & card P = card Q & Det (EqSegm (M,P,Q)) <> 0. K ) by A2, NAT_1:43; :: thesis: