let m9, n9 be Nat; :: thesis: for K being Field
for M9 being Matrix of n9,m9,K
for P, Q being finite without_zero Subset of NAT
for i being Nat
for j0 being non zero Nat st j0 in Seg n9 & i in P & not j0 in P & card P = card Q & [:P,Q:] c= Indices M9 holds
( card P = card ((P \ {i}) \/ {j0}) & [:((P \ {i}) \/ {j0}),Q:] c= Indices M9 & ( Det (EqSegm ((RLine (M9,i,(Line (M9,j0)))),P,Q)) = Det (EqSegm (M9,((P \ {i}) \/ {j0}),Q)) or Det (EqSegm ((RLine (M9,i,(Line (M9,j0)))),P,Q)) = - (Det (EqSegm (M9,((P \ {i}) \/ {j0}),Q))) ) )
let K be Field; :: thesis: for M9 being Matrix of n9,m9,K
for P, Q being finite without_zero Subset of NAT
for i being Nat
for j0 being non zero Nat st j0 in Seg n9 & i in P & not j0 in P & card P = card Q & [:P,Q:] c= Indices M9 holds
( card P = card ((P \ {i}) \/ {j0}) & [:((P \ {i}) \/ {j0}),Q:] c= Indices M9 & ( Det (EqSegm ((RLine (M9,i,(Line (M9,j0)))),P,Q)) = Det (EqSegm (M9,((P \ {i}) \/ {j0}),Q)) or Det (EqSegm ((RLine (M9,i,(Line (M9,j0)))),P,Q)) = - (Det (EqSegm (M9,((P \ {i}) \/ {j0}),Q))) ) )
let M9 be Matrix of n9,m9,K; :: thesis: for P, Q being finite without_zero Subset of NAT
for i being Nat
for j0 being non zero Nat st j0 in Seg n9 & i in P & not j0 in P & card P = card Q & [:P,Q:] c= Indices M9 holds
( card P = card ((P \ {i}) \/ {j0}) & [:((P \ {i}) \/ {j0}),Q:] c= Indices M9 & ( Det (EqSegm ((RLine (M9,i,(Line (M9,j0)))),P,Q)) = Det (EqSegm (M9,((P \ {i}) \/ {j0}),Q)) or Det (EqSegm ((RLine (M9,i,(Line (M9,j0)))),P,Q)) = - (Det (EqSegm (M9,((P \ {i}) \/ {j0}),Q))) ) )
let P, Q be finite without_zero Subset of NAT; :: thesis: for i being Nat
for j0 being non zero Nat st j0 in Seg n9 & i in P & not j0 in P & card P = card Q & [:P,Q:] c= Indices M9 holds
( card P = card ((P \ {i}) \/ {j0}) & [:((P \ {i}) \/ {j0}),Q:] c= Indices M9 & ( Det (EqSegm ((RLine (M9,i,(Line (M9,j0)))),P,Q)) = Det (EqSegm (M9,((P \ {i}) \/ {j0}),Q)) or Det (EqSegm ((RLine (M9,i,(Line (M9,j0)))),P,Q)) = - (Det (EqSegm (M9,((P \ {i}) \/ {j0}),Q))) ) )
let i be Nat; :: thesis: for j0 being non zero Nat st j0 in Seg n9 & i in P & not j0 in P & card P = card Q & [:P,Q:] c= Indices M9 holds
( card P = card ((P \ {i}) \/ {j0}) & [:((P \ {i}) \/ {j0}),Q:] c= Indices M9 & ( Det (EqSegm ((RLine (M9,i,(Line (M9,j0)))),P,Q)) = Det (EqSegm (M9,((P \ {i}) \/ {j0}),Q)) or Det (EqSegm ((RLine (M9,i,(Line (M9,j0)))),P,Q)) = - (Det (EqSegm (M9,((P \ {i}) \/ {j0}),Q))) ) )
let j0 be non zero Nat; :: thesis: ( j0 in Seg n9 & i in P & not j0 in P & card P = card Q & [:P,Q:] c= Indices M9 implies ( card P = card ((P \ {i}) \/ {j0}) & [:((P \ {i}) \/ {j0}),Q:] c= Indices M9 & ( Det (EqSegm ((RLine (M9,i,(Line (M9,j0)))),P,Q)) = Det (EqSegm (M9,((P \ {i}) \/ {j0}),Q)) or Det (EqSegm ((RLine (M9,i,(Line (M9,j0)))),P,Q)) = - (Det (EqSegm (M9,((P \ {i}) \/ {j0}),Q))) ) ) )
assume that
A1: j0 in Seg n9 and
A2: i in P and
A3: not j0 in P and
A4: card P = card Q and
A5: [:P,Q:] c= Indices M9 ; :: thesis: ( card P = card ((P \ {i}) \/ {j0}) & [:((P \ {i}) \/ {j0}),Q:] c= Indices M9 & ( Det (EqSegm ((RLine (M9,i,(Line (M9,j0)))),P,Q)) = Det (EqSegm (M9,((P \ {i}) \/ {j0}),Q)) or Det (EqSegm ((RLine (M9,i,(Line (M9,j0)))),P,Q)) = - (Det (EqSegm (M9,((P \ {i}) \/ {j0}),Q))) ) )
set Pi = P \ {i};
A6: P \ {i} c= P by XBOOLE_1:36;
set SQ = Sgm Q;
set Pij = (P \ {i}) \/ {j0};
set SPij = Sgm ((P \ {i}) \/ {j0});
A7: rng (Sgm ((P \ {i}) \/ {j0})) = (P \ {i}) \/ {j0} by FINSEQ_1:def 14;
card P > 0 by A2;
then reconsider C = (card P) - 1 as Element of NAT by NAT_1:20;
card P = C + 1 ;
then A8: card (P \ {i}) = C by A2, STIRL2_1:55;
not j0 in P \ {i} by A3, XBOOLE_0:def 5;
hence A9: card ((P \ {i}) \/ {j0}) = C + 1 by A8, CARD_2:41
.= card P ;
:: thesis: ( [:((P \ {i}) \/ {j0}),Q:] c= Indices M9 & ( Det (EqSegm ((RLine (M9,i,(Line (M9,j0)))),P,Q)) = Det (EqSegm (M9,((P \ {i}) \/ {j0}),Q)) or Det (EqSegm ((RLine (M9,i,(Line (M9,j0)))),P,Q)) = - (Det (EqSegm (M9,((P \ {i}) \/ {j0}),Q))) ) )
then reconsider SPij = Sgm ((P \ {i}) \/ {j0}), SQ9 = Sgm Q as Element of (card P) -tuples_on NAT by A4;
A10: Segm (M9,SPij,SQ9) = Segm (M9,((P \ {i}) \/ {j0}),Q) by A4, A9
.= EqSegm (M9,((P \ {i}) \/ {j0}),Q) by A4, A9, Def3 ;
P c= Seg (len M9) by A4, A5, Th67;
then A11: P \ {i} c= Seg (len M9) by A6;
n9 = len M9 by MATRIX_0:def 2;
then {j0} c= Seg (len M9) by A1, ZFMISC_1:31;
then A12: (P \ {i}) \/ {j0} c= Seg (len M9) by A11, XBOOLE_1:8;
set SP = Sgm P;
A13: rng (Sgm Q) = Q by FINSEQ_1:def 14;
rng (Sgm P) = P by FINSEQ_1:def 14;
then consider PT being Element of (card P) -tuples_on NAT such that
A14: rng PT = (P \ {i}) \/ {j0} and
A15: Segm ((RLine (M9,i,(Line (M9,j0)))),(Sgm P),(Sgm Q)) = Segm (M9,PT,(Sgm Q)) by A2, A5, A13, Th39;
Q c= Seg (width M9) by A4, A5, Th67;
hence [:((P \ {i}) \/ {j0}),Q:] c= Indices M9 by A4, A9, A12, Th67; :: thesis: ( Det (EqSegm ((RLine (M9,i,(Line (M9,j0)))),P,Q)) = Det (EqSegm (M9,((P \ {i}) \/ {j0}),Q)) or Det (EqSegm ((RLine (M9,i,(Line (M9,j0)))),P,Q)) = - (Det (EqSegm (M9,((P \ {i}) \/ {j0}),Q))) )
EqSegm ((RLine (M9,i,(Line (M9,j0)))),P,Q) = Segm ((RLine (M9,i,(Line (M9,j0)))),P,Q) by A4, Def3
.= Segm (M9,PT,SQ9) by A4, A15 ;
hence ( Det (EqSegm ((RLine (M9,i,(Line (M9,j0)))),P,Q)) = Det (EqSegm (M9,((P \ {i}) \/ {j0}),Q)) or Det (EqSegm ((RLine (M9,i,(Line (M9,j0)))),P,Q)) = - (Det (EqSegm (M9,((P \ {i}) \/ {j0}),Q))) ) by A9, A7, A13, A14, A10, Th36; :: thesis: verum