let K be Field; 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; 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; 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; ( 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
; ( 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; verum