let K be Field; :: thesis: for M being Matrix of K
for P, Q being finite without_zero Subset of NAT
for i, j being Nat st i in Seg (card P) & j in Seg (card P) & card P = card Q holds
( Delete ((EqSegm (M,P,Q)),i,j) = EqSegm (M,(P \ {((Sgm P) . i)}),(Q \ {((Sgm Q) . j)})) & card (P \ {((Sgm P) . i)}) = card (Q \ {((Sgm Q) . j)}) )
let M be Matrix of K; :: thesis: for P, Q being finite without_zero Subset of NAT
for i, j being Nat st i in Seg (card P) & j in Seg (card P) & card P = card Q holds
( Delete ((EqSegm (M,P,Q)),i,j) = EqSegm (M,(P \ {((Sgm P) . i)}),(Q \ {((Sgm Q) . j)})) & card (P \ {((Sgm P) . i)}) = card (Q \ {((Sgm Q) . j)}) )
let P1, Q1 be finite without_zero Subset of NAT; :: thesis: for i, j being Nat st i in Seg (card P1) & j in Seg (card P1) & card P1 = card Q1 holds
( Delete ((EqSegm (M,P1,Q1)),i,j) = EqSegm (M,(P1 \ {((Sgm P1) . i)}),(Q1 \ {((Sgm Q1) . j)})) & card (P1 \ {((Sgm P1) . i)}) = card (Q1 \ {((Sgm Q1) . j)}) )
let i, j be Nat; :: thesis: ( i in Seg (card P1) & j in Seg (card P1) & card P1 = card Q1 implies ( Delete ((EqSegm (M,P1,Q1)),i,j) = EqSegm (M,(P1 \ {((Sgm P1) . i)}),(Q1 \ {((Sgm Q1) . j)})) & card (P1 \ {((Sgm P1) . i)}) = card (Q1 \ {((Sgm Q1) . j)}) ) )
assume that
A1: i in Seg (card P1) and
A2: j in Seg (card P1) and
A3: card P1 = card Q1 ; :: thesis: ( Delete ((EqSegm (M,P1,Q1)),i,j) = EqSegm (M,(P1 \ {((Sgm P1) . i)}),(Q1 \ {((Sgm Q1) . j)})) & card (P1 \ {((Sgm P1) . i)}) = card (Q1 \ {((Sgm Q1) . j)}) )
set SQ1 = Sgm Q1;
A4: ex m being Nat st Q1 c= Seg m by Th43;
then A5: dom (Sgm Q1) = Seg (card Q1) by FINSEQ_3:40;
A6: rng (Sgm Q1) = Q1 by A4, FINSEQ_1:def 13;
then A7: (Sgm Q1) " Q1 = Seg (card P1) by A3, A5, RELAT_1:134;
set Q = Q1 \ {((Sgm Q1) . j)};
set Q2 = (Seg (card Q1)) \ {j};
A8: Q1 \ {((Sgm Q1) . j)} c= Q1 by XBOOLE_1:36;
set SP1 = Sgm P1;
A9: ex n being Nat st P1 c= Seg n by Th43;
then A10: dom (Sgm P1) = Seg (card P1) by FINSEQ_3:40;
A11: rng (Sgm P1) = P1 by A9, FINSEQ_1:def 13;
then A12: (Sgm P1) " P1 = Seg (card P1) by A10, RELAT_1:134;
Sgm Q1 is one-to-one by A4, FINSEQ_3:92;
then (Sgm Q1) " {((Sgm Q1) . j)} = {j} by A2, A3, A5, FINSEQ_5:4;
then A13: (Seg (card Q1)) \ {j} = (Sgm Q1) " (Q1 \ {((Sgm Q1) . j)}) by A3, A7, FUNCT_1:69;
A14: (Sgm P1) . i in P1 by A1, A10, A11, FUNCT_1:def 3;
set P2 = (Seg (card P1)) \ {i};
set P = P1 \ {((Sgm P1) . i)};
Sgm P1 is one-to-one by A9, FINSEQ_3:92;
then (Sgm P1) " {((Sgm P1) . i)} = {i} by A1, A10, FINSEQ_5:4;
then A15: (Seg (card P1)) \ {i} = (Sgm P1) " (P1 \ {((Sgm P1) . i)}) by A12, FUNCT_1:69;
set E = EqSegm (M,P1,Q1);
A16: P1 \ {((Sgm P1) . i)} c= P1 by XBOOLE_1:36;
card P1 <> 0 by A1;
then reconsider C = (card P1) - 1 as Element of NAT by NAT_1:20;
A17: card P1 = C + 1 ;
(Sgm Q1) . j in Q1 by A2, A3, A5, A6, FUNCT_1:def 3;
then A18: card (Q1 \ {((Sgm Q1) . j)}) = C by A3, A17, STIRL2_1:55;
Delete ((EqSegm (M,P1,Q1)),i,j) = Deleting ((EqSegm (M,P1,Q1)),i,j) by A1, A2, LAPLACE:def 1
.= Segm ((EqSegm (M,P1,Q1)),((Seg (card P1)) \ {i}),((Seg (card Q1)) \ {j})) by A3, Th58
.= Segm ((Segm (M,P1,Q1)),((Seg (card P1)) \ {i}),((Seg (card Q1)) \ {j})) by A3, Def3
.= Segm (M,(P1 \ {((Sgm P1) . i)}),(Q1 \ {((Sgm Q1) . j)})) by A16, A8, A15, A13, Th56
.= EqSegm (M,(P1 \ {((Sgm P1) . i)}),(Q1 \ {((Sgm Q1) . j)})) by A14, A17, A18, Def3, STIRL2_1:55 ;
hence ( Delete ((EqSegm (M,P1,Q1)),i,j) = EqSegm (M,(P1 \ {((Sgm P1) . i)}),(Q1 \ {((Sgm Q1) . j)})) & card (P1 \ {((Sgm P1) . i)}) = card (Q1 \ {((Sgm Q1) . j)}) ) by A14, A17, A18, STIRL2_1:55; :: thesis: verum