let n, i, j be Nat; :: thesis: for K being Field
for M being Matrix of n,K holds Segm M,((Seg n) \ {i}),((Seg n) \ {j}) = Deleting M,i,j
let K be Field; :: thesis: for M being Matrix of n,K holds Segm M,((Seg n) \ {i}),((Seg n) \ {j}) = Deleting M,i,j
let M be Matrix of n,K; :: thesis: Segm M,((Seg n) \ {i}),((Seg n) \ {j}) = Deleting M,i,j
A1: width M = n by MATRIX_1:25;
A2: len M = n by MATRIX_1:25;
then A3: dom M = Seg n by FINSEQ_1:def 3;

per cases ( not i in Seg n or i in Seg n ) ;

suppose A4: not i in Seg n ; :: thesis: Segm M,((Seg n) \ {i}),((Seg n) \ {j}) = Deleting M,i,j

then A5: Seg n = (Seg n) \ {i} by ZFMISC_1:65;
Del M,i = M by A3, A4, FINSEQ_3:113;
hence Segm M,((Seg n) \ {i}),((Seg n) \ {j}) = Deleting M,i,j by A2, A1, A5, Th52; :: thesis: verum

end;

suppose A6: i in Seg n ; :: thesis: Segm M,((Seg n) \ {i}),((Seg n) \ {j}) = Deleting M,i,j

set Q1 = Seg n;
set Q = (Seg n) \ {j};
set P = (Seg n) \ {i};
set SS = Segm M,((Seg n) \ {i}),(Seg n);
consider m being Nat such that
A7: len M = m + 1 and
A8: len (Del M,i) = m by A3, A6, FINSEQ_3:113;

per cases ( m = 0 or m > 0 ) ;

suppose A9: m = 0 ; :: thesis: Segm M,((Seg n) \ {i}),((Seg n) \ {j}) = Deleting M,i,j

then len (Deleting M,i,j) = 0 by A8, MATRIX_2:def 6;
then A10: Deleting M,i,j = {} ;
A11: (Seg n) \ {1} = {} by A2, A7, A9, FINSEQ_1:4, XBOOLE_1:37;
i = 1 by A2, A6, A7, A9, FINSEQ_1:4, TARSKI:def 1;
then len (Segm M,((Seg n) \ {i}),((Seg n) \ {j})) = 0 by A11, MATRIX_1:def 3;
hence Segm M,((Seg n) \ {i}),((Seg n) \ {j}) = Deleting M,i,j by A10; :: thesis: verum

end;

suppose m > 0 ; :: thesis: Segm M,((Seg n) \ {i}),((Seg n) \ {j}) = Deleting M,i,j

then n > 1 + 0 by A2, A7, XREAL_1:10;
then A12: n = width (DelLine M,i) by A2, A1, LAPLACE:4;
A13: (Seg n) \ {j} c= Seg n by XBOOLE_1:36;
(Seg n) \ {i} c= Seg n by XBOOLE_1:36;
then A14: rng (Sgm ((Seg n) \ {i})) = (Seg n) \ {i} by FINSEQ_1:def 13;
dom (Sgm ((Seg n) \ {i})) = Seg (card ((Seg n) \ {i})) by FINSEQ_3:45, XBOOLE_1:36;
then A15: (Sgm ((Seg n) \ {i})) " ((Seg n) \ {i}) = Seg (card ((Seg n) \ {i})) by A14, RELAT_1:169
.= Seg (len (Segm M,((Seg n) \ {i}),(Seg n))) by MATRIX_1:def 3 ;
A16: Segm M,((Seg n) \ {i}),(Seg n) = Del M,i by A2, A1, Th51;
then A17: Deleting M,i,j = Segm (Segm M,((Seg n) \ {i}),(Seg n)),(Seg (len (Segm M,((Seg n) \ {i}),(Seg n)))),((Seg (width (Segm M,((Seg n) \ {i}),(Seg n)))) \ {j}) by Th52;
Sgm (Seg n) = idseq n by FINSEQ_3:54;
then (Sgm (Seg n)) " ((Seg n) \ {j}) = (Seg (width (Segm M,((Seg n) \ {i}),(Seg n)))) \ {j} by A13, A12, A16, FUNCT_2:171;
hence Segm M,((Seg n) \ {i}),((Seg n) \ {j}) = Deleting M,i,j by A13, A15, A17, Th56; :: thesis: verum

end;

end;

end;

end;