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, FINSEQ_1:4;
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 13;
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

n -' 1 <= n by NAT_D:35;
then A4: Seg (n -' 1) c= Seg n by FINSEQ_1:7;
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_1:def 7;
then A6: DT * k,m = (Delete M,i,j) * m,k by MATRIX_1:def 7;
reconsider k9 = k, m9 = m as Element of NAT by ORDINAL1:def 13;
A7: Indices DT = [:(Seg (n -' 1)),(Seg (n -' 1)):] by MATRIX_1:25;
then A8: k in Seg (n -' 1) by A5, ZFMISC_1:106;
then A9: k + 1 in Seg n by A3, FINSEQ_1:81;
A10: Indices M = [:(Seg n),(Seg n):] by MATRIX_1:25;
A11: m in Seg (n -' 1) by A5, A7, ZFMISC_1:106;
then A12: m + 1 in Seg n by A3, FINSEQ_1:81;

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:106;
(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_1:def 7; :: 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:106;
(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_1:def 7; :: 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:106;
(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_1:def 7; :: 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:106;
(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_1:def 7; :: thesis: verum

end;

end;

end;

hence (Delete M,i,j) @ = Delete (M @ ),j,i by MATRIX_1:28; :: thesis: verum