let K be Field; :: thesis: 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; :: thesis: 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 ; :: thesis: ( 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 & P c= P1 )
and
A2:
Det (EqSegm M,P1,Q1) <> 0. K
; :: thesis: 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 );
A3:
S1[ card P1]
A4:
for k being Element of NAT st k < card P1 & S1[k + 1] holds
S1[k]
proof
let k be
Element of
NAT ;
:: thesis: ( k < card P1 & S1[k + 1] implies S1[k] )
assume A5:
(
k < card P1 &
S1[
k + 1] )
;
:: thesis: S1[k]
let P be
finite without_zero Subset of
NAT ;
:: thesis: ( 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 A6:
(
P c= P1 &
card P = k )
;
:: thesis: 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, A6, XBOOLE_0:def 8;
then
P1 \ P <> {}
by XBOOLE_1:105;
then consider x being
set such that A7:
x in P1 \ P
by XBOOLE_0:def 1;
reconsider x =
x as non
zero Element of
NAT by A7;
reconsider Px =
P \/ {x} as
finite without_zero Subset of
NAT ;
(
x in P1 & not
0 in P1 )
by A7, XBOOLE_0:def 5;
then A8:
( not
x in P &
{x} c= P1 )
by A7, XBOOLE_0:def 5, ZFMISC_1:37;
then A9:
(
card Px = k + 1 &
Px c= P1 )
by A6, CARD_2:54, XBOOLE_1:8;
then consider Q2 being
finite without_zero Subset of
NAT such that A10:
(
Q2 c= Q1 &
card Px = card Q2 &
Det (EqSegm M,Px,Q2) <> 0. K )
by A5;
set E =
EqSegm M,
Px,
Q2;
consider n being
Nat such that A11:
Px c= Seg n
by Th43;
x in {x}
by TARSKI:def 1;
then
(
rng (Sgm Px) = Px &
dom (Sgm Px) = Seg (card Px) &
x in Px )
by A11, FINSEQ_1:def 13, FINSEQ_3:45, XBOOLE_0:def 3;
then consider i being
set such that A12:
(
i in Seg (card Px) &
(Sgm Px) . i = x )
by FUNCT_1:def 5;
reconsider i =
i as
Element of
NAT by A12;
consider j being
Nat such that A13:
(
j in Seg (card Px) &
Det (Delete (EqSegm M,Px,Q2),i,j) <> 0. K )
by A10, A12, Lm3;
take Q =
Q2 \ {((Sgm Q2) . j)};
:: thesis: ( Q c= Q1 & card P = card Q & Det (EqSegm M,P,Q) <> 0. K )
(
Px \ {x} = P &
Q c= Q2 &
(k + 1) -' 1
= (k + 1) - 1 )
by A8, XBOOLE_1:36, XREAL_0:def 2, ZFMISC_1:141;
hence
(
Q c= Q1 &
card P = card Q &
Det (EqSegm M,P,Q) <> 0. K )
by A6, A9, A10, A12, A13, Th64, XBOOLE_1:1;
:: thesis: verum
end;
A14:
for k being Element of NAT st k <= card P1 holds
S1[k]
from TRIANG_1:sch 1(A3, A4);
card P <= card P1
by A1, NAT_1:44;
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 A1, A14; :: thesis: verum