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;

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)

hence
(Delete (M,i,j)) @ = Delete ((M @),j,i)
by MATRIX_0:27; :: thesis: verumDT * (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_{1},b_{2}) = (Delete (MT,j,i)) * (b_{1},b_{2}) )

assume A5: [k,m] in Indices DT ; :: thesis: DT * (b_{1},b_{2}) = (Delete (MT,j,i)) * (b_{1},b_{2})

[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;

end;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

assume A5: [k,m] in Indices DT ; :: thesis: DT * (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 ) )
;

end;

suppose A13:
( m9 < I & k9 < j )
; :: thesis: DT * (b_{1},b_{2}) = (Delete (MT,j,i)) * (b_{1},b_{2})

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;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

suppose A16:
( m9 < I & k9 >= j )
; :: thesis: DT * (b_{1},b_{2}) = (Delete (MT,j,i)) * (b_{1},b_{2})

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;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

suppose A19:
( m9 >= I & k9 < j )
; :: thesis: DT * (b_{1},b_{2}) = (Delete (MT,j,i)) * (b_{1},b_{2})

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;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

suppose A22:
( m9 >= I & k9 >= j )
; :: thesis: DT * (b_{1},b_{2}) = (Delete (MT,j,i)) * (b_{1},b_{2})

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;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