let K be Field; :: thesis:
let A be Matrix of K; :: thesis:
let P, Q, R be finite without_zero Subset of NAT; :: thesis:
assume A1: [:P,R:] c= Indices A ; :: thesis:
let i, j be Nat; :: thesis:
assume that
A2: i in (dom A) \ P and
A3: j in (Seg (width A)) \ Q and
A4: A * (i,j) <> 0. K and
A5: Q c= R and
A6: (Line (A,i)) * (Sgm R) = (card R) |-> (0. K) ; :: thesis:
A7: dom A = Seg (len A) by FINSEQ_1:def 3;
then A8: i in Seg (len A) by A2, XBOOLE_0:def 5;
A9: [:P,Q:] c= [:P,R:] by A5, ZFMISC_1:95;
then A10: [:P,Q:] c= Indices A by A1;
reconsider i0 = i, j0 = j as non zero Element of NAT by A2, A3, A7;
A11: j in Seg (width A) by A3, XBOOLE_0:def 5;
set S = Segm (A,P,Q);
consider P9, Q9 being finite without_zero Subset of NAT such that
A12: [:P9,Q9:] c= Indices (Segm (A,P,Q)) and
A13: card P9 = card Q9 and
A14: card P9 = the_rank_of (Segm (A,P,Q)) and
A15: Det (EqSegm ((Segm (A,P,Q)),P9,Q9)) <> 0. K by MATRIX13:def 4;
( P9 = {} iff Q9 = {} ) by A13;
then consider P2, Q2 being finite without_zero Subset of NAT such that
A16: P2 c= P and
A17: Q2 c= Q and
P2 = (Sgm P) .: P9 and
Q2 = (Sgm Q) .: Q9 and
A18: card P2 = card P9 and
A19: card Q2 = card Q9 and
A20: Segm ((Segm (A,P,Q)),P9,Q9) = Segm (A,P2,Q2) by A12, MATRIX13:57;
set Q2j = Q2 \/ {j0};
set P2i = P2 \/ {i0};
set ESS = EqSegm (A,(P2 \/ {i0}),(Q2 \/ {j0}));
set SS = Segm (A,(P2 \/ {i0}),(Q2 \/ {j0}));

per cases = {} or [:P,Q:] <> {} ) ;

suppose [:P,Q:] = {} ; :: thesis:

then ( card P = 0 or card Q = 0 ) by CARD_1:27, ZFMISC_1:90;
then A21: the_rank_of (Segm (A,P,Q)) = 0 by MATRIX13:77;
[i,j] in Indices A by A7, A8, A11, ZFMISC_1:87;
hence the_rank_of A > the_rank_of (Segm (A,P,Q)) by A4, A21, MATRIX13:94; :: thesis:

end;

suppose A22: [:P,Q:] <> {} ; :: thesis:

then P c= dom A by A10, ZFMISC_1:114;
then A23: P2 c= dom A by A16;
[:P,R:] <> {} by A9, A22, XBOOLE_1:3;
then A24: R c= Seg (width A) by A1, ZFMISC_1:114;
A25: dom (Sgm R) = Seg (card R) by FINSEQ_3:40;
Q c= Seg (width A) by A10, A22, ZFMISC_1:114;
then A26: Q2 c= Seg (width A) by A17;
A27: {j0} c= Seg (width A) by A11, ZFMISC_1:31;
A28: Sgm (Q2 \/ {j0}) is one-to-one by FINSEQ_3:92;
A29: Q2 \/ {j0} c= Seg (width A) by A26, A27, XBOOLE_1:8;
A30: rng (Sgm (Q2 \/ {j0})) = Q2 \/ {j0} by FINSEQ_1:def 14;
{i0} c= dom A by A7, A8, ZFMISC_1:31;
then P2 \/ {i0} c= dom A by A23, XBOOLE_1:8;
then A33: [:(P2 \/ {i0}),(Q2 \/ {j0}):] c= Indices A by A29, ZFMISC_1:96;
A34: dom (Sgm (P2 \/ {i0})) = Seg (card (P2 \/ {i0})) by FINSEQ_3:40;
i in {i} by TARSKI:def 1;
then A35: i in P2 \/ {i0} by XBOOLE_0:def 3;
A36: not i in P2 by A2, A16, XBOOLE_0:def 5;
then A37: card (P2 \/ {i0}) = (card P2) + 1 by CARD_2:41;
then A38: (card (P2 \/ {i0})) -' 1 = card P9 by A18, NAT_D:34;
A39: not j in Q2 by A3, A17, XBOOLE_0:def 5;
then A40: card (Q2 \/ {j0}) = (card Q2) + 1 by CARD_2:41;
then A41: EqSegm (A,(P2 \/ {i0}),(Q2 \/ {j0})) = Segm (A,(P2 \/ {i0}),(Q2 \/ {j0})) by A13, A18, A19, A36, CARD_2:41, MATRIX13:def 3;
j in {j} by TARSKI:def 1;
then j in Q2 \/ {j0} by XBOOLE_0:def 3;
then consider y being object such that
A42: y in dom (Sgm (Q2 \/ {j0})) and
A43: (Sgm (Q2 \/ {j0})) . y = j by A30, FUNCT_1:def 3;
rng (Sgm (P2 \/ {i0})) = P2 \/ {i0} by FINSEQ_1:def 14;
then consider x being object such that
A44: x in dom (Sgm (P2 \/ {i0})) and
A45: (Sgm (P2 \/ {i0})) . x = i by A35, FUNCT_1:def 3;
reconsider x = x, y = y as Element of NAT by A44, A42;
- (1_ K) <> 0. K by VECTSP_1:28;
then A46: (power K) . ((- (1_ K)),(x + y)) <> 0. K by Lm2;
set L = LaplaceExpL ((EqSegm (A,(P2 \/ {i0}),(Q2 \/ {j0}))),x);
A47: dom (LaplaceExpL ((EqSegm (A,(P2 \/ {i0}),(Q2 \/ {j0}))),x)) = Seg (len (LaplaceExpL ((EqSegm (A,(P2 \/ {i0}),(Q2 \/ {j0}))),x))) by FINSEQ_1:def 3
.= Seg (card (P2 \/ {i0})) by LAPLACE:def 7 ;
then A48: y in dom (LaplaceExpL ((EqSegm (A,(P2 \/ {i0}),(Q2 \/ {j0}))),x)) by A13, A18, A19, A37, A40, A42, FINSEQ_3:40;
A49: dom (Sgm (Q2 \/ {j0})) = Seg (card (Q2 \/ {j0})) by FINSEQ_3:40;
then Delete ((EqSegm (A,(P2 \/ {i0}),(Q2 \/ {j0}))),x,y) = EqSegm (A,((P2 \/ {i0}) \ {i}),((Q2 \/ {j0}) \ {j})) by A13, A18, A19, A37, A40, A34, A44, A45, A42, A43, MATRIX13:64
.= EqSegm (A,P2,((Q2 \/ {j0}) \ {j})) by A36, ZFMISC_1:117
.= EqSegm (A,P2,Q2) by A39, ZFMISC_1:117
.= Segm (A,P2,Q2) by A13, A18, A19, MATRIX13:def 3
.= EqSegm ((Segm (A,P,Q)),P9,Q9) by A13, A20, MATRIX13:def 3 ;
then A50: ((power K) . ((- (1_ K)),(x + y))) * (Det (Delete ((EqSegm (A,(P2 \/ {i0}),(Q2 \/ {j0}))),x,y))) <> 0. K by A15, A38, A46, VECTSP_1:12;
A51: Indices (EqSegm (A,(P2 \/ {i0}),(Q2 \/ {j0}))) = [:(Seg (card (P2 \/ {i0}))),(Seg (card (P2 \/ {i0}))):] by MATRIX_0:24;
then A52: [x,y] in Indices (EqSegm (A,(P2 \/ {i0}),(Q2 \/ {j0}))) by A13, A18, A19, A37, A40, A34, A49, A44, A42, ZFMISC_1:87;
A53: rng (Sgm R) = R by FINSEQ_1:def 14;

now :: thesis:

let k be Nat; :: thesis:
assume that
A54: k in dom (LaplaceExpL ((EqSegm (A,(P2 \/ {i0}),(Q2 \/ {j0}))),x)) and
A55: k <> y ; :: thesis:
(Sgm (Q2 \/ {j0})) . k <> j by A13, A18, A19, A37, A40, A49, A28, A42, A43, A47, A54, A55, FUNCT_1:def 4;
then A56: not (Sgm (Q2 \/ {j0})) . k in {j} by TARSKI:def 1;
(Sgm (Q2 \/ {j0})) . k in Q2 \/ {j0} by A13, A18, A19, A37, A40, A30, A49, A47, A54, FUNCT_1:def 3;
then (Sgm (Q2 \/ {j0})) . k in Q2 by A56, XBOOLE_0:def 3;
then A57: (Sgm (Q2 \/ {j0})) . k in Q by A17;
then A58: (Sgm (Q2 \/ {j0})) . k in R by A5;
consider z being object such that
A59: z in dom (Sgm R) and
A60: (Sgm R) . z = (Sgm (Q2 \/ {j0})) . k by A5, A53, A57, FUNCT_1:def 3;
reconsider z = z as Element of NAT by A59;
[x,k] in Indices (EqSegm (A,(P2 \/ {i0}),(Q2 \/ {j0}))) by A34, A44, A47, A51, A54, ZFMISC_1:87;
then (EqSegm (A,(P2 \/ {i0}),(Q2 \/ {j0}))) * (x,k) = A * (i,((Sgm (Q2 \/ {j0})) . k)) by A45, A41, MATRIX13:def 1
.= (Line (A,i)) . ((Sgm R) . z) by A24, A60, A58, MATRIX_0:def 7
.= ((card R) |-> (0. K)) . z by A6, A59, FUNCT_1:13
.= 0. K by A25, A59, FINSEQ_2:57 ;
hence (LaplaceExpL ((EqSegm (A,(P2 \/ {i0}),(Q2 \/ {j0}))),x)) . k = (0. K) * (Cofactor ((EqSegm (A,(P2 \/ {i0}),(Q2 \/ {j0}))),x,k)) by A54, LAPLACE:def 7
.= 0. K ;
:: thesis:

end;

then A61: (LaplaceExpL ((EqSegm (A,(P2 \/ {i0}),(Q2 \/ {j0}))),x)) . y = Sum (LaplaceExpL ((EqSegm (A,(P2 \/ {i0}),(Q2 \/ {j0}))),x)) by A48, MATRIX_3:12
.= Det (EqSegm (A,(P2 \/ {i0}),(Q2 \/ {j0}))) by A34, A44, LAPLACE:25 ;
(LaplaceExpL ((EqSegm (A,(P2 \/ {i0}),(Q2 \/ {j0}))),x)) . y = ((Segm (A,(P2 \/ {i0}),(Q2 \/ {j0}))) * (x,y)) * (Cofactor ((EqSegm (A,(P2 \/ {i0}),(Q2 \/ {j0}))),x,y)) by A48, A41, LAPLACE:def 7
.= (A * (i,j)) * (((power K) . ((- (1_ K)),(x + y))) * (Det (Delete ((EqSegm (A,(P2 \/ {i0}),(Q2 \/ {j0}))),x,y)))) by A45, A43, A41, A52, MATRIX13:def 1 ;
then Det (EqSegm (A,(P2 \/ {i0}),(Q2 \/ {j0}))) <> 0. K by A4, A61, A50, VECTSP_1:12;
then the_rank_of A >= card (P2 \/ {i0}) by A13, A18, A19, A37, A40, A33, MATRIX13:def 4;
hence the_rank_of A > the_rank_of (Segm (A,P,Q)) by A14, A18, A37, NAT_1:13; :: thesis:

end;