let n be Nat; :: thesis: for K being Field
for M being Matrix of n,K
for i, j being Nat st i in Seg n & j in Seg n holds
(Delete (M,i,j)) @ = Delete ((M @),j,i)
let K be Field; :: thesis: for M being Matrix of n,K
for i, j being Nat st i in Seg n & j in Seg n holds
(Delete (M,i,j)) @ = Delete ((M @),j,i)
let M be Matrix of n,K; :: thesis: for i, j being Nat st i in Seg n & j in Seg n holds
(Delete (M,i,j)) @ = Delete ((M @),j,i)
let i, j be Nat; :: thesis: ( i in Seg n & j in Seg n implies (Delete (M,i,j)) @ = Delete ((M @),j,i) )
assume that
A1: i in Seg n and
A2: j in Seg n ; :: thesis: (Delete (M,i,j)) @ = Delete ((M @),j,i)
n > 0 by A1;
then reconsider n1 = n - 1 as Element of NAT by NAT_1:20;
set X1 = Seg n;
reconsider MT = M @ as Matrix of n,K ;
set D = Delete (M,i,j);
set n9 = n -' 1;
reconsider I = i as Element of NAT by ORDINAL1:def 12;
reconsider DT = (Delete (M,i,j)) @ as Matrix of n -' 1,K ;
set D9 = Delete (MT,j,i);
set X = Seg (n -' 1);
A3: (n1 + 1) -' 1 = n1 by NAT_D:34;

now :: thesis: for k, m being Nat st [k,m] in Indices DT holds
DT * (k,m) = (Delete (MT,j,i)) * (k,m)

n -' 1 <= n by NAT_D:35;
then A4: Seg (n -' 1) c= Seg n by FINSEQ_1:5;
let k, m be Nat; :: thesis: ( [k,m] in Indices DT implies DT * (b₁,b₂) = (Delete (MT,j,i)) * (b₁,b₂) )
assume A5: [k,m] in Indices DT ; :: thesis: DT * (b₁,b₂) = (Delete (MT,j,i)) * (b₁,b₂)
[m,k] in Indices (Delete (M,i,j)) by A5, MATRIX_0:def 6;
then A6: DT * (k,m) = (Delete (M,i,j)) * (m,k) by MATRIX_0:def 6;
reconsider k9 = k, m9 = m as Element of NAT by ORDINAL1:def 12;
A7: Indices DT = [:(Seg (n -' 1)),(Seg (n -' 1)):] by MATRIX_0:24;
then A8: k in Seg (n -' 1) by A5, ZFMISC_1:87;
then A9: k + 1 in Seg n by A3, FINSEQ_1:60;
A10: Indices M = [:(Seg n),(Seg n):] by MATRIX_0:24;
A11: m in Seg (n -' 1) by A5, A7, ZFMISC_1:87;
then A12: m + 1 in Seg n by A3, FINSEQ_1:60;

per cases ( ( m9 < I & k9 < j ) or ( m9 < I & k9 >= j ) or ( m9 >= I & k9 < j ) or ( m9 >= I & k9 >= j ) ) ;

suppose A13: ( m9 < I & k9 < j ) ; :: thesis: DT * (b₁,b₂) = (Delete (MT,j,i)) * (b₁,b₂)

then A14: (Delete (MT,j,i)) * (k,m) = MT * (k,m) by A1, A2, A8, A11, Th13;
A15: [m,k] in Indices M by A8, A11, A4, A10, ZFMISC_1:87;
(Delete (M,i,j)) * (m,k) = M * (m,k) by A1, A2, A8, A11, A13, Th13;
hence DT * (k,m) = (Delete (MT,j,i)) * (k,m) by A6, A15, A14, MATRIX_0:def 6; :: thesis: verum

end;

suppose A16: ( m9 < I & k9 >= j ) ; :: thesis: DT * (b₁,b₂) = (Delete (MT,j,i)) * (b₁,b₂)

then A17: (Delete (MT,j,i)) * (k,m) = MT * ((k + 1),m) by A1, A2, A8, A11, Th13;
A18: [m,(k + 1)] in Indices M by A11, A4, A9, A10, ZFMISC_1:87;
(Delete (M,i,j)) * (m,k) = M * (m,(k + 1)) by A1, A2, A8, A11, A16, Th13;
hence DT * (k,m) = (Delete (MT,j,i)) * (k,m) by A6, A18, A17, MATRIX_0:def 6; :: thesis: verum

end;

suppose A19: ( m9 >= I & k9 < j ) ; :: thesis: DT * (b₁,b₂) = (Delete (MT,j,i)) * (b₁,b₂)

then A20: (Delete (MT,j,i)) * (k,m) = MT * (k,(m + 1)) by A1, A2, A8, A11, Th13;
A21: [(m + 1),k] in Indices M by A8, A4, A12, A10, ZFMISC_1:87;
(Delete (M,i,j)) * (m,k) = M * ((m + 1),k) by A1, A2, A8, A11, A19, Th13;
hence DT * (k,m) = (Delete (MT,j,i)) * (k,m) by A6, A21, A20, MATRIX_0:def 6; :: thesis: verum

end;

suppose A22: ( m9 >= I & k9 >= j ) ; :: thesis: DT * (b₁,b₂) = (Delete (MT,j,i)) * (b₁,b₂)

then A23: (Delete (MT,j,i)) * (k,m) = MT * ((k + 1),(m + 1)) by A1, A2, A8, A11, Th13;
A24: [(m + 1),(k + 1)] in Indices M by A9, A12, A10, ZFMISC_1:87;
(Delete (M,i,j)) * (m,k) = M * ((m + 1),(k + 1)) by A1, A2, A8, A11, A22, Th13;
hence DT * (k,m) = (Delete (MT,j,i)) * (k,m) by A6, A24, A23, MATRIX_0:def 6; :: thesis: verum

end;

end;

end;

hence (Delete (M,i,j)) @ = Delete ((M @),j,i) by MATRIX_0:27; :: thesis: verum