let K be Field; :: thesis: for A being Matrix of K

for P, Q, Q9 being finite without_zero Subset of NAT st [:P,Q9:] 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= Q9 & (Line (A,i)) * (Sgm Q9) = (card Q9) |-> (0. K) holds

the_rank_of A > the_rank_of (Segm (A,P,Q))

let A be Matrix of K; :: thesis: for P, Q, Q9 being finite without_zero Subset of NAT st [:P,Q9:] 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= Q9 & (Line (A,i)) * (Sgm Q9) = (card Q9) |-> (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 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: the_rank_of A > the_rank_of (Segm (A,P,Q))

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}));

for P, Q, Q9 being finite without_zero Subset of NAT st [:P,Q9:] 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= Q9 & (Line (A,i)) * (Sgm Q9) = (card Q9) |-> (0. K) holds

the_rank_of A > the_rank_of (Segm (A,P,Q))

let A be Matrix of K; :: thesis: for P, Q, Q9 being finite without_zero Subset of NAT st [:P,Q9:] 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= Q9 & (Line (A,i)) * (Sgm Q9) = (card Q9) |-> (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 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: the_rank_of A > the_rank_of (Segm (A,P,Q))

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
( [:P,Q:] = {} or [:P,Q:] <> {} )
;

end;

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: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: verum

end;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: verum

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

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;

then 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;

then A28: Sgm (Q2 \/ {j0}) is one-to-one by A26, FINSEQ_3:92, 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:31;

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:96;

A34: dom (Sgm (P2 \/ {i0})) = Seg (card (P2 \/ {i0})) by A7, A23, A31, FINSEQ_3:40, 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: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 A7, A32, FINSEQ_1:def 13;

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, A26, A27, A37, A40, A42, FINSEQ_3:40, XBOOLE_1:8;

A49: dom (Sgm (Q2 \/ {j0})) = Seg (card (Q2 \/ {j0})) by A26, A27, FINSEQ_3:40, 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: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 A24, FINSEQ_1:def 13;

.= 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: verum

end;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;

then 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;

then A28: Sgm (Q2 \/ {j0}) is one-to-one by A26, FINSEQ_3:92, 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:31;

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:96;

A34: dom (Sgm (P2 \/ {i0})) = Seg (card (P2 \/ {i0})) by A7, A23, A31, FINSEQ_3:40, 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: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 A7, A32, FINSEQ_1:def 13;

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, A26, A27, A37, A40, A42, FINSEQ_3:40, XBOOLE_1:8;

A49: dom (Sgm (Q2 \/ {j0})) = Seg (card (Q2 \/ {j0})) by A26, A27, FINSEQ_3:40, 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: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 A24, FINSEQ_1:def 13;

now :: thesis: for k being Nat st k in dom (LaplaceExpL ((EqSegm (A,(P2 \/ {i0}),(Q2 \/ {j0}))),x)) & k <> y holds

(LaplaceExpL ((EqSegm (A,(P2 \/ {i0}),(Q2 \/ {j0}))),x)) . k = 0. K

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
(LaplaceExpL ((EqSegm (A,(P2 \/ {i0}),(Q2 \/ {j0}))),x)) . k = 0. K

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 that

A54: k in dom (LaplaceExpL ((EqSegm (A,(P2 \/ {i0}),(Q2 \/ {j0}))),x)) and

A55: k <> y ; :: thesis: (LaplaceExpL ((EqSegm (A,(P2 \/ {i0}),(Q2 \/ {j0}))),x)) . k = 0. K

(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: verum

end;assume that

A54: k in dom (LaplaceExpL ((EqSegm (A,(P2 \/ {i0}),(Q2 \/ {j0}))),x)) and

A55: k <> y ; :: thesis: (LaplaceExpL ((EqSegm (A,(P2 \/ {i0}),(Q2 \/ {j0}))),x)) . k = 0. K

(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: verum

.= 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: verum