let i, j, n 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_0:24;
A2: len M = n by MATRIX_0:24;
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:57;
Del (M,i) = M by A3, A4, FINSEQ_3:104;
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:104;

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_0:def 13;
then A10: Deleting (M,i,j) = {} ;
A11: (Seg n) \ {1} = {} by A2, A7, A9, FINSEQ_1:2, XBOOLE_1:37;
i = 1 by A2, A6, A7, A9, FINSEQ_1:2, TARSKI:def 1;
then len (Segm (M,((Seg n) \ {i}),((Seg n) \ {j}))) = 0 by A11, MATRIX_0:def 2;
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:8;
then A12: n = width (DelLine (M,i)) by A2, A1, LAPLACE:4;
A13: (Seg n) \ {j} c= Seg n by XBOOLE_1:36;
A14: rng (Sgm ((Seg n) \ {i})) = (Seg n) \ {i} by FINSEQ_1:def 14;
dom (Sgm ((Seg n) \ {i})) = Seg (card ((Seg n) \ {i})) by FINSEQ_3:40;
then A15: (Sgm ((Seg n) \ {i})) " ((Seg n) \ {i}) = Seg (card ((Seg n) \ {i})) by A14, RELAT_1:134
.= Seg (len (Segm (M,((Seg n) \ {i}),(Seg n)))) by MATRIX_0:def 2 ;
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:48;
then (Sgm (Seg n)) " ((Seg n) \ {j}) = (Seg (width (Segm (M,((Seg n) \ {i}),(Seg n))))) \ {j} by A13, A12, A16, FUNCT_2:94;
hence Segm (M,((Seg n) \ {i}),((Seg n) \ {j})) = Deleting (M,i,j) by A13, A15, A17, Th56; :: thesis: verum

end;

end;

end;

end;