let K be Field; :: thesis: for M being Matrix of K
for P, Q being finite without_zero Subset of NAT
for i being Nat st i in Seg (card P) & Det (EqSegm M,P,Q) <> 0. K holds
ex j being Nat st
( j in Seg (card P) & Det (Delete (EqSegm M,P,Q),i,j) <> 0. K )
let M be Matrix of K; :: thesis: for P, Q being finite without_zero Subset of NAT
for i being Nat st i in Seg (card P) & Det (EqSegm M,P,Q) <> 0. K holds
ex j being Nat st
( j in Seg (card P) & Det (Delete (EqSegm M,P,Q),i,j) <> 0. K )
let P, Q be finite without_zero Subset of NAT ; :: thesis: for i being Nat st i in Seg (card P) & Det (EqSegm M,P,Q) <> 0. K holds
ex j being Nat st
( j in Seg (card P) & Det (Delete (EqSegm M,P,Q),i,j) <> 0. K )
let i be Nat; :: thesis: ( i in Seg (card P) & Det (EqSegm M,P,Q) <> 0. K implies ex j being Nat st
( j in Seg (card P) & Det (Delete (EqSegm M,P,Q),i,j) <> 0. K ) )
assume that
A1: i in Seg (card P) and
A2: Det (EqSegm M,P,Q) <> 0. K ; :: thesis: ex j being Nat st
( j in Seg (card P) & Det (Delete (EqSegm M,P,Q),i,j) <> 0. K )
set C = card P;
set E = EqSegm M,P,Q;
set LL = LaplaceExpL (EqSegm M,P,Q),i;
set CC = (card P) |-> (0. K);
Sum ((card P) |-> (0. K)) = 0. K by MATRIX_3:13;
then A3: LaplaceExpL (EqSegm M,P,Q),i <> (card P) |-> (0. K) by A1, A2, LAPLACE:25;
len (LaplaceExpL (EqSegm M,P,Q),i) = card P by LAPLACE:def 7;
then A4: dom (LaplaceExpL (EqSegm M,P,Q),i) = Seg (card P) by FINSEQ_1:def 3;
dom ((card P) |-> (0. K)) = Seg (card P) by FUNCOP_1:19;
then consider j being Nat such that
A5: j in dom (LaplaceExpL (EqSegm M,P,Q),i) and
A6: (LaplaceExpL (EqSegm M,P,Q),i) . j <> ((card P) |-> (0. K)) . j by A3, A4, FINSEQ_1:17;
A7: (LaplaceExpL (EqSegm M,P,Q),i) . j = ((EqSegm M,P,Q) * i,j) * (Cofactor (EqSegm M,P,Q),i,j) by A5, LAPLACE:def 7;
((card P) |-> (0. K)) . j = 0. K by A4, A5, FINSEQ_2:71;
then Cofactor (EqSegm M,P,Q),i,j <> 0. K by A6, A7, VECTSP_1:44;
then Minor (EqSegm M,P,Q),i,j <> 0. K by VECTSP_1:44;
hence ex j being Nat st
( j in Seg (card P) & Det (Delete (EqSegm M,P,Q),i,j) <> 0. K ) by A4, A5; :: thesis: verum