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) & j in Seg (card P1) ) and
A2: 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 SP1 = Sgm P1;
set SQ1 = Sgm Q1;
set E = EqSegm M,P1,Q1;
set P = P1 \ {((Sgm P1) . i)};
set Q = Q1 \ {((Sgm Q1) . j)};
set P2 = (Seg (card P1)) \ {i};
set Q2 = (Seg (card Q1)) \ {j};
A3: ( P1 \ {((Sgm P1) . i)} c= P1 & Q1 \ {((Sgm Q1) . j)} c= Q1 ) by XBOOLE_1:36;
consider n being Nat such that
A4: P1 c= Seg n by Th43;
consider m being Nat such that
A5: Q1 c= Seg m by Th43;
card P1 <> 0 by A1;
then card P1 > 0 ;
then reconsider C = (card P1) - 1 as Element of NAT by NAT_1:20;
A6: ( dom (Sgm P1) = Seg (card P1) & rng (Sgm P1) = P1 & dom (Sgm Q1) = Seg (card Q1) & rng (Sgm Q1) = Q1 & Sgm P1 is without_repeated_line & Sgm Q1 is without_repeated_line ) by A4, A5, FINSEQ_1:def 13, FINSEQ_3:45, FINSEQ_3:99;
then ( (Sgm P1) " {((Sgm P1) . i)} = {i} & (Sgm Q1) " {((Sgm Q1) . j)} = {j} & (Sgm P1) " P1 = Seg (card P1) & (Sgm Q1) " Q1 = Seg (card P1) ) by A1, A2, FINSEQ_5:4, RELAT_1:169;
then A7: ( (Seg (card P1)) \ {i} = (Sgm P1) " (P1 \ {((Sgm P1) . i)}) & (Seg (card Q1)) \ {j} = (Sgm Q1) " (Q1 \ {((Sgm Q1) . j)}) ) by A2, FUNCT_1:138;
( (Sgm P1) . i in P1 & (Sgm Q1) . j in Q1 & card P1 = C + 1 ) by A1, A2, A6, FUNCT_1:def 5;
then A8: ( card (P1 \ {((Sgm P1) . i)}) = C & card (Q1 \ {((Sgm Q1) . j)}) = C ) by A2, STIRL2_1:65;
Delete (EqSegm M,P1,Q1),i,j = Deleting (EqSegm M,P1,Q1),i,j by A1, LAPLACE:def 1
.= Segm (EqSegm M,P1,Q1),((Seg (card P1)) \ {i}),((Seg (card Q1)) \ {j}) by A2, Th58
.= Segm (Segm M,P1,Q1),((Seg (card P1)) \ {i}),((Seg (card Q1)) \ {j}) by A2, Def3
.= Segm M,(P1 \ {((Sgm P1) . i)}),(Q1 \ {((Sgm Q1) . j)}) by A3, A7, Th56
.= EqSegm M,(P1 \ {((Sgm P1) . i)}),(Q1 \ {((Sgm Q1) . j)}) by A8, Def3 ;
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 A8; :: thesis: verum