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

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

suppose [:P,Q:] = {} ; :: thesis: the_rank_of A > the_rank_of (Segm A,P,Q)

then ( card P = 0 or card Q = 0 ) by CARD_1:47, ZFMISC_1:113;
then A14: the_rank_of (Segm A,P,Q) = 0 by MATRIX13:77;
[i,j] in Indices A by A12, A13, ZFMISC_1:106;
hence the_rank_of A > the_rank_of (Segm A,P,Q) by A14, A2, MATRIX13:94; :: thesis: verum

end;

suppose [:P,Q:] <> {} ; :: thesis: the_rank_of A > the_rank_of (Segm A,P,Q)

then ( P c= dom A & Q c= Seg (width A) & [:P,R:] <> {} ) by A5, A4, XBOOLE_1:3, ZFMISC_1:138;
then A15: ( P2 c= dom A & Q2 c= Seg (width A) & R c= Seg (width A) ) by A9, A1, XBOOLE_1:1, ZFMISC_1:138;
A16: ( {i0} c= dom A & {j0} c= Seg (width A) ) by A12, A13, ZFMISC_1:37;
then A17: ( P2 \/ {i0} c= dom A & Q2 \/ {j0} c= Seg (width A) ) by A15, XBOOLE_1:8;
A18: ( not i in P2 & not j in Q2 ) by A9, A2, XBOOLE_0:def 5;
then A19: ( card (P2 \/ {i0}) = (card P2) + 1 & card (Q2 \/ {j0}) = (card Q2) + 1 ) by CARD_2:54;
A20: ( rng (Sgm (P2 \/ {i0})) = P2 \/ {i0} & dom (Sgm (P2 \/ {i0})) = Seg (card (P2 \/ {i0})) & rng (Sgm (Q2 \/ {j0})) = Q2 \/ {j0} & dom (Sgm (Q2 \/ {j0})) = Seg (card (Q2 \/ {j0})) & Sgm (Q2 \/ {j0}) is one-to-one & rng (Sgm R) = R & dom (Sgm R) = Seg (card R) ) by A12, A15, A17, FINSEQ_1:def 13, FINSEQ_3:45, FINSEQ_3:99;
i in {i} by TARSKI:def 1;
then i in P2 \/ {i0} by XBOOLE_0:def 3;
then consider x being set such that
A21: ( x in dom (Sgm (P2 \/ {i0})) & (Sgm (P2 \/ {i0})) . x = i ) by A20, FUNCT_1:def 5;
j in {j} by TARSKI:def 1;
then j in Q2 \/ {j0} by XBOOLE_0:def 3;
then consider y being set such that
A22: ( y in dom (Sgm (Q2 \/ {j0})) & (Sgm (Q2 \/ {j0})) . y = j ) by A20, FUNCT_1:def 5;
reconsider x = x, y = y as Element of NAT by A21, A22;
set L = LaplaceExpL (EqSegm A,(P2 \/ {i0}),(Q2 \/ {j0})),x;
A23: 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 A24: y in dom (LaplaceExpL (EqSegm A,(P2 \/ {i0}),(Q2 \/ {j0})),x) by A6, A10, A19, A22, A16, A15, FINSEQ_3:45, XBOOLE_1:8;
A25: ( len (EqSegm A,(P2 \/ {i0}),(Q2 \/ {j0})) = card (P2 \/ {i0}) & dom (EqSegm A,(P2 \/ {i0}),(Q2 \/ {j0})) = Seg (len (EqSegm A,(P2 \/ {i0}),(Q2 \/ {j0}))) & Indices (EqSegm A,(P2 \/ {i0}),(Q2 \/ {j0})) = [:(Seg (card (P2 \/ {i0}))),(Seg (card (P2 \/ {i0}))):] ) by FINSEQ_1:def 3, MATRIX_1:25;
A26: EqSegm A,(P2 \/ {i0}),(Q2 \/ {j0}) = Segm A,(P2 \/ {i0}),(Q2 \/ {j0}) by A6, A10, A19, MATRIX13:def 3;

now

let k be Nat; :: thesis: ( k in dom (LaplaceExpL (EqSegm A,(P2 \/ {i0}),(Q2 \/ {j0})),x) & k <> y implies (LaplaceExpL (EqSegm A,(P2 \/ {i0}),(Q2 \/ {j0})),x) . k = 0. K )
assume A27: ( k in dom (LaplaceExpL (EqSegm A,(P2 \/ {i0}),(Q2 \/ {j0})),x) & k <> y ) ; :: thesis: (LaplaceExpL (EqSegm A,(P2 \/ {i0}),(Q2 \/ {j0})),x) . k = 0. K
A28: [x,k] in Indices (EqSegm A,(P2 \/ {i0}),(Q2 \/ {j0})) by A25, A27, A20, A21, A23, ZFMISC_1:106;
(Sgm (Q2 \/ {j0})) . k <> j by A27, A23, A20, A6, A10, A19, A22, FUNCT_1:def 8;
then ( (Sgm (Q2 \/ {j0})) . k in Q2 \/ {j0} & not (Sgm (Q2 \/ {j0})) . k in {j} ) by A27, A6, A10, A19, A20, A23, FUNCT_1:def 5, TARSKI:def 1;
then (Sgm (Q2 \/ {j0})) . k in Q2 by XBOOLE_0:def 3;
then A29: (Sgm (Q2 \/ {j0})) . k in Q by A9;
then consider z being set such that
A30: ( z in dom (Sgm R) & (Sgm R) . z = (Sgm (Q2 \/ {j0})) . k ) by A3, A20, FUNCT_1:def 5;
A31: (Sgm (Q2 \/ {j0})) . k in R by A3, A29;
reconsider z = z as Element of NAT by A30;
(EqSegm A,(P2 \/ {i0}),(Q2 \/ {j0})) * x,k = A * i,((Sgm (Q2 \/ {j0})) . k) by A21, A28, A26, MATRIX13:def 1
.= (Line A,i) . ((Sgm R) . z) by A15, A31, A30, MATRIX_1:def 8
.= ((card R) |-> (0. K)) . z by A3, A30, FUNCT_1:23
.= 0. K by A20, A30, 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 A27, LAPLACE:def 7
.= 0. K by VECTSP_1:39 ;
:: thesis: verum

end;

then A32: (LaplaceExpL (EqSegm A,(P2 \/ {i0}),(Q2 \/ {j0})),x) . y = Sum (LaplaceExpL (EqSegm A,(P2 \/ {i0}),(Q2 \/ {j0})),x) by A24, MATRIX_3:14
.= Det (EqSegm A,(P2 \/ {i0}),(Q2 \/ {j0})) by A20, A21, LAPLACE:25 ;
A33: [x,y] in Indices (EqSegm A,(P2 \/ {i0}),(Q2 \/ {j0})) by A6, A10, A19, A20, A21, A22, A25, ZFMISC_1:106;
A34: (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 A26, A24, LAPLACE:def 7
.= (A * i,j) * (((power K) . (- (1_ K)),(x + y)) * (Det (Delete (EqSegm A,(P2 \/ {i0}),(Q2 \/ {j0})),x,y))) by A21, A22, A33, A26, MATRIX13:def 1 ;
A35: Delete (EqSegm A,(P2 \/ {i0}),(Q2 \/ {j0})),x,y = EqSegm A,((P2 \/ {i0}) \ {i}),((Q2 \/ {j0}) \ {j}) by A6, A10, A19, A20, A21, A22, MATRIX13:64
.= EqSegm A,P2,((Q2 \/ {j0}) \ {j}) by A18, ZFMISC_1:141
.= EqSegm A,P2,Q2 by A18, ZFMISC_1:141
.= Segm A,P2,Q2 by A6, A10, MATRIX13:def 3
.= EqSegm (Segm A,P,Q),P',Q' by A6, A11, MATRIX13:def 3 ;
A36: (card (P2 \/ {i0})) -' 1 = card P' by A10, A19, NAT_D:34;
- (1_ K) <> 0. K by VECTSP_1:86;
then (power K) . (- (1_ K)),(x + y) <> 0. K by Lm2;
then ((power K) . (- (1_ K)),(x + y)) * (Det (Delete (EqSegm A,(P2 \/ {i0}),(Q2 \/ {j0})),x,y)) <> 0. K by A35, A8, A36, VECTSP_1:44;
then A37: Det (EqSegm A,(P2 \/ {i0}),(Q2 \/ {j0})) <> 0. K by A32, A2, A34, VECTSP_1:44;
[:(P2 \/ {i0}),(Q2 \/ {j0}):] c= Indices A by A17, ZFMISC_1:119;
then the_rank_of A >= card (P2 \/ {i0}) by A6, A10, A19, A37, MATRIX13:def 4;
hence the_rank_of A > the_rank_of (Segm A,P,Q) by A7, A10, A19, NAT_1:13; :: thesis: verum

end;

end;