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