let K be Field; for M being Matrix of K
for P, P1, Q1 being finite without_zero Subset of NAT st card P1 = card Q1 & P c= P1 & Det (EqSegm (M,P1,Q1)) <> 0. K holds
ex Q being finite without_zero Subset of NAT st
( Q c= Q1 & card P = card Q & Det (EqSegm (M,P,Q)) <> 0. K )
let M be Matrix of K; for P, P1, Q1 being finite without_zero Subset of NAT st card P1 = card Q1 & P c= P1 & Det (EqSegm (M,P1,Q1)) <> 0. K holds
ex Q being finite without_zero Subset of NAT st
( Q c= Q1 & card P = card Q & Det (EqSegm (M,P,Q)) <> 0. K )
let P, P1, Q1 be finite without_zero Subset of NAT; ( card P1 = card Q1 & P c= P1 & Det (EqSegm (M,P1,Q1)) <> 0. K implies ex Q being finite without_zero Subset of NAT st
( Q c= Q1 & card P = card Q & Det (EqSegm (M,P,Q)) <> 0. K ) )
assume that
A1:
card P1 = card Q1
and
A2:
P c= P1
and
A3:
Det (EqSegm (M,P1,Q1)) <> 0. K
; ex Q being finite without_zero Subset of NAT st
( Q c= Q1 & card P = card Q & Det (EqSegm (M,P,Q)) <> 0. K )
defpred S1[ Nat] means for P being finite without_zero Subset of NAT st P c= P1 & card P = $1 holds
ex Q being finite without_zero Subset of NAT st
( Q c= Q1 & card P = card Q & Det (EqSegm (M,P,Q)) <> 0. K );
A4:
for k being Element of NAT st k < card P1 & S1[k + 1] holds
S1[k]
proof
let k be
Element of
NAT ;
( k < card P1 & S1[k + 1] implies S1[k] )
assume that A5:
k < card P1
and A6:
S1[
k + 1]
;
S1[k]
let P be
finite without_zero Subset of
NAT;
( P c= P1 & card P = k implies ex Q being finite without_zero Subset of NAT st
( Q c= Q1 & card P = card Q & Det (EqSegm (M,P,Q)) <> 0. K ) )
assume that A7:
P c= P1
and A8:
card P = k
;
ex Q being finite without_zero Subset of NAT st
( Q c= Q1 & card P = card Q & Det (EqSegm (M,P,Q)) <> 0. K )
P c< P1
by A5, A7, A8, XBOOLE_0:def 8;
then
P1 \ P <> {}
by XBOOLE_1:105;
then consider x being
object such that A9:
x in P1 \ P
by XBOOLE_0:def 1;
reconsider x =
x as non
zero Element of
NAT by A9;
reconsider Px =
P \/ {x} as
finite without_zero Subset of
NAT ;
A10:
not
x in P
by A9, XBOOLE_0:def 5;
then A11:
card Px = k + 1
by A8, CARD_2:41;
x in P1
by A9, XBOOLE_0:def 5;
then
{x} c= P1
by ZFMISC_1:31;
then
Px c= P1
by A7, XBOOLE_1:8;
then consider Q2 being
finite without_zero Subset of
NAT such that A12:
Q2 c= Q1
and A13:
card Px = card Q2
and A14:
Det (EqSegm (M,Px,Q2)) <> 0. K
by A6, A8, A10, CARD_2:41;
set E =
EqSegm (
M,
Px,
Q2);
A15:
Px \ {x} = P
by A10, ZFMISC_1:117;
x in {x}
by TARSKI:def 1;
then A16:
x in Px
by XBOOLE_0:def 3;
A18:
dom (Sgm Px) = Seg (card Px)
by FINSEQ_3:40;
rng (Sgm Px) = Px
by FINSEQ_1:def 14;
then consider i being
object such that A19:
i in Seg (card Px)
and A20:
(Sgm Px) . i = x
by A18, A16, FUNCT_1:def 3;
A21:
(k + 1) -' 1
= (k + 1) - 1
by XREAL_0:def 2;
reconsider i =
i as
Element of
NAT by A19;
consider j being
Nat such that A22:
j in Seg (card Px)
and A23:
Det (Delete ((EqSegm (M,Px,Q2)),i,j)) <> 0. K
by A14, A19, Lm3;
take Q =
Q2 \ {((Sgm Q2) . j)};
( Q c= Q1 & card P = card Q & Det (EqSegm (M,P,Q)) <> 0. K )
Q c= Q2
by XBOOLE_1:36;
hence
(
Q c= Q1 &
card P = card Q &
Det (EqSegm (M,P,Q)) <> 0. K )
by A8, A11, A12, A13, A19, A20, A22, A23, A15, A21, Th64;
verum
end;
A24:
S1[ card P1]
for k being Element of NAT st k <= card P1 holds
S1[k]
from PRE_POLY:sch 1(A24, A4);
hence
ex Q being finite without_zero Subset of NAT st
( Q c= Q1 & card P = card Q & Det (EqSegm (M,P,Q)) <> 0. K )
by A2, NAT_1:43; verum