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:118;
then A10: [:P,Q:] c= Indices A by A1, XBOOLE_1:1;
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:47, ZFMISC_1:113;
then A21: the_rank_of (Segm A,P,Q) = 0 by MATRIX13:77;
[i,j] in Indices A by A7, A8, A11, ZFMISC_1:106;
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:138;
then A23: P2 c= dom A by A16, XBOOLE_1:1;
[:P,R:] <> {} by A9, A22, XBOOLE_1:3;
then A24: R c= Seg (width A) by A1, ZFMISC_1:138;
then A25: dom (Sgm R) = Seg (card R) by FINSEQ_3:45;
Q c= Seg (width A) by A10, A22, ZFMISC_1:138;
then A26: Q2 c= Seg (width A) by A17, XBOOLE_1:1;
A27: {j0} c= Seg (width A) by A11, ZFMISC_1:37;
then A28: Sgm (Q2 \/ {j0}) is one-to-one by A26, FINSEQ_3:99, XBOOLE_1:8;
A29: Q2 \/ {j0} c= Seg (width A) by A26, A27, XBOOLE_1:8;
then A30: rng (Sgm (Q2 \/ {j0})) = Q2 \/ {j0} by FINSEQ_1:def 13;
A31: {i0} c= dom A by A7, A8, ZFMISC_1:37;
then A32: P2 \/ {i0} c= dom A by A23, XBOOLE_1:8;
then A33: [:(P2 \/ {i0}),(Q2 \/ {j0}):] c= Indices A by A29, ZFMISC_1:119;
A34: dom (Sgm (P2 \/ {i0})) = Seg (card (P2 \/ {i0})) by A7, A23, A31, FINSEQ_3:45, XBOOLE_1:8;
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:54;
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:54;
then A41: EqSegm A,(P2 \/ {i0}),(Q2 \/ {j0}) = Segm A,(P2 \/ {i0}),(Q2 \/ {j0}) by A13, A18, A19, A36, CARD_2:54, MATRIX13:def 3;
j in {j} by TARSKI:def 1;
then j in Q2 \/ {j0} by XBOOLE_0:def 3;
then consider y being set such that
A42: y in dom (Sgm (Q2 \/ {j0})) and
A43: (Sgm (Q2 \/ {j0})) . y = j by A30, FUNCT_1:def 5;
rng (Sgm (P2 \/ {i0})) = P2 \/ {i0} by A7, A32, FINSEQ_1:def 13;
then consider x being set such that
A44: x in dom (Sgm (P2 \/ {i0})) and
A45: (Sgm (P2 \/ {i0})) . x = i by A35, FUNCT_1:def 5;
reconsider x = x, y = y as Element of NAT by A44, A42;
- (1_ K) <> 0. K by VECTSP_1:86;
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, A26, A27, A37, A40, A42, FINSEQ_3:45, XBOOLE_1:8;
A49: dom (Sgm (Q2 \/ {j0})) = Seg (card (Q2 \/ {j0})) by A26, A27, FINSEQ_3:45, XBOOLE_1:8;
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:141
.= EqSegm A,P2,Q2 by A39, ZFMISC_1:141
.= 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:44;
A51: Indices (EqSegm A,(P2 \/ {i0}),(Q2 \/ {j0})) = [:(Seg (card (P2 \/ {i0}))),(Seg (card (P2 \/ {i0}))):] by MATRIX_1:25;
then A52: [x,y] in Indices (EqSegm A,(P2 \/ {i0}),(Q2 \/ {j0})) by A13, A18, A19, A37, A40, A34, A49, A44, A42, ZFMISC_1:106;
A53: rng (Sgm R) = R by A24, FINSEQ_1:def 13;

now

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 8;
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 5;
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 set such that
A59: z in dom (Sgm R) and
A60: (Sgm R) . z = (Sgm (Q2 \/ {j0})) . k by A5, A53, A57, FUNCT_1:def 5;
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:106;
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_1:def 8
.= ((card R) |-> (0. K)) . z by A6, A59, FUNCT_1:23
.= 0. K by A25, A59, FINSEQ_2:71 ;
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 by VECTSP_1:39 ;
:: 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:14
.= 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:44;
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;