let K be Field; for M being Matrix of K
for P1, Q, Q1 being finite without_zero Subset of NAT st card P1 = card Q1 & Q c= Q1 & Det (EqSegm (M,P1,Q1)) <> 0. K 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 )
let M be Matrix of K; for P1, Q, Q1 being finite without_zero Subset of NAT st card P1 = card Q1 & Q c= Q1 & Det (EqSegm (M,P1,Q1)) <> 0. K 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 )
let P1, Q, Q1 be finite without_zero Subset of NAT; ( card P1 = card Q1 & Q c= Q1 & Det (EqSegm (M,P1,Q1)) <> 0. K implies ex P being finite without_zero Subset of NAT st
( P c= P1 & card P = card Q & Det (EqSegm (M,P,Q)) <> 0. K ) )
assume that
A1:
card P1 = card Q1
and
A2:
Q c= Q1
and
A3:
Det (EqSegm (M,P1,Q1)) <> 0. K
; ex P being finite without_zero Subset of NAT st
( P c= P1 & card P = card Q & Det (EqSegm (M,P,Q)) <> 0. K )
defpred S1[ 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 & S1[k + 1] holds
S1[k]
proof
let k be
Element of
NAT ;
( k < card Q1 & S1[k + 1] implies S1[k] )
assume that A5:
k < card Q1
and A6:
S1[
k + 1]
;
S1[k]
let Q be
finite without_zero Subset of
NAT;
( Q c= Q1 & card Q = k implies ex P being finite without_zero Subset of NAT st
( P c= P1 & card P = card Q & Det (EqSegm (M,P,Q)) <> 0. K ) )
assume that A7:
Q c= Q1
and A8:
card Q = k
;
ex P being finite without_zero Subset of NAT st
( P c= P1 & card P = card Q & Det (EqSegm (M,P,Q)) <> 0. K )
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;
A17:
ex
n being
Nat st
Qx c= Seg n
by Th43;
then A18:
dom (Sgm Qx) = Seg (card Qx)
by FINSEQ_3:40;
rng (Sgm Qx) = Qx
by A17, FINSEQ_1:def 13;
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)};
( P c= P1 & card P = card Q & Det (EqSegm (M,P,Q)) <> 0. K )
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;
verum
end;
A25:
S1[ card Q1]
for k being Element of NAT st k <= card Q1 holds
S1[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; verum