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

for k, m being Nat st k in Seg (n -' 1) & m in Seg (n -' 1) holds

( ( k < i & m < j implies (Delete (M,i,j)) * (k,m) = M * (k,m) ) & ( k < i & m >= j implies (Delete (M,i,j)) * (k,m) = M * (k,(m + 1)) ) & ( k >= i & m < j implies (Delete (M,i,j)) * (k,m) = M * ((k + 1),m) ) & ( k >= i & m >= j implies (Delete (M,i,j)) * (k,m) = M * ((k + 1),(m + 1)) ) )

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

for k, m being Nat st k in Seg (n -' 1) & m in Seg (n -' 1) holds

( ( k < i & m < j implies (Delete (M,i,j)) * (k,m) = M * (k,m) ) & ( k < i & m >= j implies (Delete (M,i,j)) * (k,m) = M * (k,(m + 1)) ) & ( k >= i & m < j implies (Delete (M,i,j)) * (k,m) = M * ((k + 1),m) ) & ( k >= i & m >= j implies (Delete (M,i,j)) * (k,m) = M * ((k + 1),(m + 1)) ) )

let M be Matrix of n,K; :: thesis: for i, j being Nat st i in Seg n & j in Seg n holds

for k, m being Nat st k in Seg (n -' 1) & m in Seg (n -' 1) holds

( ( k < i & m < j implies (Delete (M,i,j)) * (k,m) = M * (k,m) ) & ( k < i & m >= j implies (Delete (M,i,j)) * (k,m) = M * (k,(m + 1)) ) & ( k >= i & m < j implies (Delete (M,i,j)) * (k,m) = M * ((k + 1),m) ) & ( k >= i & m >= j implies (Delete (M,i,j)) * (k,m) = M * ((k + 1),(m + 1)) ) )

let i, j be Nat; :: thesis: ( i in Seg n & j in Seg n implies for k, m being Nat st k in Seg (n -' 1) & m in Seg (n -' 1) holds

( ( k < i & m < j implies (Delete (M,i,j)) * (k,m) = M * (k,m) ) & ( k < i & m >= j implies (Delete (M,i,j)) * (k,m) = M * (k,(m + 1)) ) & ( k >= i & m < j implies (Delete (M,i,j)) * (k,m) = M * ((k + 1),m) ) & ( k >= i & m >= j implies (Delete (M,i,j)) * (k,m) = M * ((k + 1),(m + 1)) ) ) )

assume that

A1: i in Seg n and

A2: j in Seg n ; :: thesis: for k, m being Nat st k in Seg (n -' 1) & m in Seg (n -' 1) holds

( ( k < i & m < j implies (Delete (M,i,j)) * (k,m) = M * (k,m) ) & ( k < i & m >= j implies (Delete (M,i,j)) * (k,m) = M * (k,(m + 1)) ) & ( k >= i & m < j implies (Delete (M,i,j)) * (k,m) = M * ((k + 1),m) ) & ( k >= i & m >= j implies (Delete (M,i,j)) * (k,m) = M * ((k + 1),(m + 1)) ) )

set DM = Delete (M,i,j);

A3: Deleting (M,i,j) = Delete (M,i,j) by A1, A2, Def1;

n > 0 by A1;

then reconsider n9 = n - 1 as Element of NAT by NAT_1:20;

set DL = DelLine (M,i);

let k, m be Nat; :: thesis: ( k in Seg (n -' 1) & m in Seg (n -' 1) implies ( ( k < i & m < j implies (Delete (M,i,j)) * (k,m) = M * (k,m) ) & ( k < i & m >= j implies (Delete (M,i,j)) * (k,m) = M * (k,(m + 1)) ) & ( k >= i & m < j implies (Delete (M,i,j)) * (k,m) = M * ((k + 1),m) ) & ( k >= i & m >= j implies (Delete (M,i,j)) * (k,m) = M * ((k + 1),(m + 1)) ) ) )

assume that

A4: k in Seg (n -' 1) and

A5: m in Seg (n -' 1) ; :: thesis: ( ( k < i & m < j implies (Delete (M,i,j)) * (k,m) = M * (k,m) ) & ( k < i & m >= j implies (Delete (M,i,j)) * (k,m) = M * (k,(m + 1)) ) & ( k >= i & m < j implies (Delete (M,i,j)) * (k,m) = M * ((k + 1),m) ) & ( k >= i & m >= j implies (Delete (M,i,j)) * (k,m) = M * ((k + 1),(m + 1)) ) )

A6: n -' 1 = n9 by XREAL_0:def 2;

then A7: k + 1 in Seg (n9 + 1) by A4, FINSEQ_1:60;

reconsider I = i, J = j, K = k, U = m as Element of NAT by ORDINAL1:def 12;

n9 <= n9 + 1 by NAT_1:11;

then A8: Seg n9 c= Seg n by FINSEQ_1:5;

A9: len M = n by MATRIX_0:24;

then A10: dom M = Seg n by FINSEQ_1:def 3;

then len (DelLine (M,i)) = n9 by A1, A6, A9, Th1;

then A11: dom (DelLine (M,i)) = Seg n9 by FINSEQ_1:def 3;

then A12: (Deleting (M,i,j)) . k = Del ((Line ((DelLine (M,i)),k)),j) by A4, A6, MATRIX_0:def 13;

len (Delete (M,i,j)) = n9 by A6, MATRIX_0:24;

then dom (Delete (M,i,j)) = Seg n9 by FINSEQ_1:def 3;

then A13: (Delete (M,i,j)) . k = Line ((Delete (M,i,j)),k) by A4, A6, MATRIX_0:60;

width (Delete (M,i,j)) = n9 by A6, MATRIX_0:24;

then A14: (Line ((Delete (M,i,j)),k)) . m = (Delete (M,i,j)) * (k,m) by A5, A6, MATRIX_0:def 7;

A15: Line ((DelLine (M,i)),k) = (DelLine (M,i)) . k by A4, A6, A11, MATRIX_0:60;

A16: m + 1 in Seg (n9 + 1) by A5, A6, FINSEQ_1:60;

A17: ( K >= I implies ( ( U < J implies (Delete (M,i,j)) * (K,U) = M * ((K + 1),U) ) & ( U >= J implies (Delete (M,i,j)) * (K,U) = M * ((K + 1),(U + 1)) ) ) )

for M being Matrix of n,K

for i, j being Nat st i in Seg n & j in Seg n holds

for k, m being Nat st k in Seg (n -' 1) & m in Seg (n -' 1) holds

( ( k < i & m < j implies (Delete (M,i,j)) * (k,m) = M * (k,m) ) & ( k < i & m >= j implies (Delete (M,i,j)) * (k,m) = M * (k,(m + 1)) ) & ( k >= i & m < j implies (Delete (M,i,j)) * (k,m) = M * ((k + 1),m) ) & ( k >= i & m >= j implies (Delete (M,i,j)) * (k,m) = M * ((k + 1),(m + 1)) ) )

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

for k, m being Nat st k in Seg (n -' 1) & m in Seg (n -' 1) holds

( ( k < i & m < j implies (Delete (M,i,j)) * (k,m) = M * (k,m) ) & ( k < i & m >= j implies (Delete (M,i,j)) * (k,m) = M * (k,(m + 1)) ) & ( k >= i & m < j implies (Delete (M,i,j)) * (k,m) = M * ((k + 1),m) ) & ( k >= i & m >= j implies (Delete (M,i,j)) * (k,m) = M * ((k + 1),(m + 1)) ) )

let M be Matrix of n,K; :: thesis: for i, j being Nat st i in Seg n & j in Seg n holds

for k, m being Nat st k in Seg (n -' 1) & m in Seg (n -' 1) holds

( ( k < i & m < j implies (Delete (M,i,j)) * (k,m) = M * (k,m) ) & ( k < i & m >= j implies (Delete (M,i,j)) * (k,m) = M * (k,(m + 1)) ) & ( k >= i & m < j implies (Delete (M,i,j)) * (k,m) = M * ((k + 1),m) ) & ( k >= i & m >= j implies (Delete (M,i,j)) * (k,m) = M * ((k + 1),(m + 1)) ) )

let i, j be Nat; :: thesis: ( i in Seg n & j in Seg n implies for k, m being Nat st k in Seg (n -' 1) & m in Seg (n -' 1) holds

( ( k < i & m < j implies (Delete (M,i,j)) * (k,m) = M * (k,m) ) & ( k < i & m >= j implies (Delete (M,i,j)) * (k,m) = M * (k,(m + 1)) ) & ( k >= i & m < j implies (Delete (M,i,j)) * (k,m) = M * ((k + 1),m) ) & ( k >= i & m >= j implies (Delete (M,i,j)) * (k,m) = M * ((k + 1),(m + 1)) ) ) )

assume that

A1: i in Seg n and

A2: j in Seg n ; :: thesis: for k, m being Nat st k in Seg (n -' 1) & m in Seg (n -' 1) holds

( ( k < i & m < j implies (Delete (M,i,j)) * (k,m) = M * (k,m) ) & ( k < i & m >= j implies (Delete (M,i,j)) * (k,m) = M * (k,(m + 1)) ) & ( k >= i & m < j implies (Delete (M,i,j)) * (k,m) = M * ((k + 1),m) ) & ( k >= i & m >= j implies (Delete (M,i,j)) * (k,m) = M * ((k + 1),(m + 1)) ) )

set DM = Delete (M,i,j);

A3: Deleting (M,i,j) = Delete (M,i,j) by A1, A2, Def1;

n > 0 by A1;

then reconsider n9 = n - 1 as Element of NAT by NAT_1:20;

set DL = DelLine (M,i);

let k, m be Nat; :: thesis: ( k in Seg (n -' 1) & m in Seg (n -' 1) implies ( ( k < i & m < j implies (Delete (M,i,j)) * (k,m) = M * (k,m) ) & ( k < i & m >= j implies (Delete (M,i,j)) * (k,m) = M * (k,(m + 1)) ) & ( k >= i & m < j implies (Delete (M,i,j)) * (k,m) = M * ((k + 1),m) ) & ( k >= i & m >= j implies (Delete (M,i,j)) * (k,m) = M * ((k + 1),(m + 1)) ) ) )

assume that

A4: k in Seg (n -' 1) and

A5: m in Seg (n -' 1) ; :: thesis: ( ( k < i & m < j implies (Delete (M,i,j)) * (k,m) = M * (k,m) ) & ( k < i & m >= j implies (Delete (M,i,j)) * (k,m) = M * (k,(m + 1)) ) & ( k >= i & m < j implies (Delete (M,i,j)) * (k,m) = M * ((k + 1),m) ) & ( k >= i & m >= j implies (Delete (M,i,j)) * (k,m) = M * ((k + 1),(m + 1)) ) )

A6: n -' 1 = n9 by XREAL_0:def 2;

then A7: k + 1 in Seg (n9 + 1) by A4, FINSEQ_1:60;

reconsider I = i, J = j, K = k, U = m as Element of NAT by ORDINAL1:def 12;

n9 <= n9 + 1 by NAT_1:11;

then A8: Seg n9 c= Seg n by FINSEQ_1:5;

A9: len M = n by MATRIX_0:24;

then A10: dom M = Seg n by FINSEQ_1:def 3;

then len (DelLine (M,i)) = n9 by A1, A6, A9, Th1;

then A11: dom (DelLine (M,i)) = Seg n9 by FINSEQ_1:def 3;

then A12: (Deleting (M,i,j)) . k = Del ((Line ((DelLine (M,i)),k)),j) by A4, A6, MATRIX_0:def 13;

len (Delete (M,i,j)) = n9 by A6, MATRIX_0:24;

then dom (Delete (M,i,j)) = Seg n9 by FINSEQ_1:def 3;

then A13: (Delete (M,i,j)) . k = Line ((Delete (M,i,j)),k) by A4, A6, MATRIX_0:60;

width (Delete (M,i,j)) = n9 by A6, MATRIX_0:24;

then A14: (Line ((Delete (M,i,j)),k)) . m = (Delete (M,i,j)) * (k,m) by A5, A6, MATRIX_0:def 7;

A15: Line ((DelLine (M,i)),k) = (DelLine (M,i)) . k by A4, A6, A11, MATRIX_0:60;

A16: m + 1 in Seg (n9 + 1) by A5, A6, FINSEQ_1:60;

A17: ( K >= I implies ( ( U < J implies (Delete (M,i,j)) * (K,U) = M * ((K + 1),U) ) & ( U >= J implies (Delete (M,i,j)) * (K,U) = M * ((K + 1),(U + 1)) ) ) )

proof

( K < I implies ( ( U < J implies (Delete (M,i,j)) * (K,U) = M * (K,U) ) & ( U >= J implies (Delete (M,i,j)) * (K,U) = M * (K,(U + 1)) ) ) )
assume A18:
K >= I
; :: thesis: ( ( U < J implies (Delete (M,i,j)) * (K,U) = M * ((K + 1),U) ) & ( U >= J implies (Delete (M,i,j)) * (K,U) = M * ((K + 1),(U + 1)) ) )

K <= n9 by A4, A6, FINSEQ_1:1;

then A19: (DelLine (M,i)) . K = M . (K + 1) by A1, A9, A10, A7, A18, FINSEQ_3:111;

A20: M . (K + 1) = Line (M,(K + 1)) by A10, A7, MATRIX_0:60;

thus ( U < J implies (Delete (M,i,j)) * (K,U) = M * ((K + 1),U) ) :: thesis: ( U >= J implies (Delete (M,i,j)) * (K,U) = M * ((K + 1),(U + 1)) )

A23: U <= n9 by A5, A6, FINSEQ_1:1;

A24: width M = n by MATRIX_0:24;

A25: len (Line ((DelLine (M,i)),K)) = width M by A15, A19, A20, MATRIX_0:def 7;

then J in dom (Line ((DelLine (M,i)),K)) by A2, A24, FINSEQ_1:def 3;

then (Delete (M,i,j)) * (K,U) = (Line (M,(K + 1))) . (U + 1) by A12, A3, A13, A14, A15, A7, A19, A20, A22, A25, A23, FINSEQ_3:111, MATRIX_0:24;

hence (Delete (M,i,j)) * (K,U) = M * ((K + 1),(U + 1)) by A16, A24, MATRIX_0:def 7; :: thesis: verum

end;K <= n9 by A4, A6, FINSEQ_1:1;

then A19: (DelLine (M,i)) . K = M . (K + 1) by A1, A9, A10, A7, A18, FINSEQ_3:111;

A20: M . (K + 1) = Line (M,(K + 1)) by A10, A7, MATRIX_0:60;

thus ( U < J implies (Delete (M,i,j)) * (K,U) = M * ((K + 1),U) ) :: thesis: ( U >= J implies (Delete (M,i,j)) * (K,U) = M * ((K + 1),(U + 1)) )

proof

assume A22:
U >= J
; :: thesis: (Delete (M,i,j)) * (K,U) = M * ((K + 1),(U + 1))
A21:
width M = n
by MATRIX_0:24;

assume U < J ; :: thesis: (Delete (M,i,j)) * (K,U) = M * ((K + 1),U)

then (Delete (M,i,j)) * (K,U) = (Line (M,(K + 1))) . U by A12, A3, A13, A14, A15, A19, A20, FINSEQ_3:110;

hence (Delete (M,i,j)) * (K,U) = M * ((K + 1),U) by A5, A6, A8, A21, MATRIX_0:def 7; :: thesis: verum

end;assume U < J ; :: thesis: (Delete (M,i,j)) * (K,U) = M * ((K + 1),U)

then (Delete (M,i,j)) * (K,U) = (Line (M,(K + 1))) . U by A12, A3, A13, A14, A15, A19, A20, FINSEQ_3:110;

hence (Delete (M,i,j)) * (K,U) = M * ((K + 1),U) by A5, A6, A8, A21, MATRIX_0:def 7; :: thesis: verum

A23: U <= n9 by A5, A6, FINSEQ_1:1;

A24: width M = n by MATRIX_0:24;

A25: len (Line ((DelLine (M,i)),K)) = width M by A15, A19, A20, MATRIX_0:def 7;

then J in dom (Line ((DelLine (M,i)),K)) by A2, A24, FINSEQ_1:def 3;

then (Delete (M,i,j)) * (K,U) = (Line (M,(K + 1))) . (U + 1) by A12, A3, A13, A14, A15, A7, A19, A20, A22, A25, A23, FINSEQ_3:111, MATRIX_0:24;

hence (Delete (M,i,j)) * (K,U) = M * ((K + 1),(U + 1)) by A16, A24, MATRIX_0:def 7; :: thesis: verum

proof

hence
( ( k < i & m < j implies (Delete (M,i,j)) * (k,m) = M * (k,m) ) & ( k < i & m >= j implies (Delete (M,i,j)) * (k,m) = M * (k,(m + 1)) ) & ( k >= i & m < j implies (Delete (M,i,j)) * (k,m) = M * ((k + 1),m) ) & ( k >= i & m >= j implies (Delete (M,i,j)) * (k,m) = M * ((k + 1),(m + 1)) ) )
by A17; :: thesis: verum
assume
K < I
; :: thesis: ( ( U < J implies (Delete (M,i,j)) * (K,U) = M * (K,U) ) & ( U >= J implies (Delete (M,i,j)) * (K,U) = M * (K,(U + 1)) ) )

then A26: (DelLine (M,i)) . K = M . K by FINSEQ_3:110;

A27: M . K = Line (M,K) by A4, A6, A10, A8, MATRIX_0:60;

thus ( U < J implies (Delete (M,i,j)) * (K,U) = M * (K,U) ) :: thesis: ( U >= J implies (Delete (M,i,j)) * (K,U) = M * (K,(U + 1)) )

A31: U <= n9 by A5, A6, FINSEQ_1:1;

A32: width M = n by MATRIX_0:24;

A33: len (Line ((DelLine (M,i)),K)) = width M by A15, A26, A27, MATRIX_0:def 7;

then J in dom (Line ((DelLine (M,i)),K)) by A2, A32, FINSEQ_1:def 3;

then (Delete (M,i,j)) * (K,U) = (Line (M,K)) . (U + 1) by A12, A3, A13, A14, A15, A7, A26, A27, A30, A33, A31, FINSEQ_3:111, MATRIX_0:24;

hence (Delete (M,i,j)) * (K,U) = M * (K,(U + 1)) by A16, A32, MATRIX_0:def 7; :: thesis: verum

end;then A26: (DelLine (M,i)) . K = M . K by FINSEQ_3:110;

A27: M . K = Line (M,K) by A4, A6, A10, A8, MATRIX_0:60;

thus ( U < J implies (Delete (M,i,j)) * (K,U) = M * (K,U) ) :: thesis: ( U >= J implies (Delete (M,i,j)) * (K,U) = M * (K,(U + 1)) )

proof

assume A30:
U >= J
; :: thesis: (Delete (M,i,j)) * (K,U) = M * (K,(U + 1))
assume A28:
U < J
; :: thesis: (Delete (M,i,j)) * (K,U) = M * (K,U)

A29: width M = n9 + 1 by MATRIX_0:24;

(Delete (M,i,j)) * (K,U) = (Line (M,K)) . U by A12, A3, A13, A14, A15, A26, A27, A28, FINSEQ_3:110;

hence (Delete (M,i,j)) * (K,U) = M * (K,U) by A5, A6, A8, A29, MATRIX_0:def 7; :: thesis: verum

end;A29: width M = n9 + 1 by MATRIX_0:24;

(Delete (M,i,j)) * (K,U) = (Line (M,K)) . U by A12, A3, A13, A14, A15, A26, A27, A28, FINSEQ_3:110;

hence (Delete (M,i,j)) * (K,U) = M * (K,U) by A5, A6, A8, A29, MATRIX_0:def 7; :: thesis: verum

A31: U <= n9 by A5, A6, FINSEQ_1:1;

A32: width M = n by MATRIX_0:24;

A33: len (Line ((DelLine (M,i)),K)) = width M by A15, A26, A27, MATRIX_0:def 7;

then J in dom (Line ((DelLine (M,i)),K)) by A2, A32, FINSEQ_1:def 3;

then (Delete (M,i,j)) * (K,U) = (Line (M,K)) . (U + 1) by A12, A3, A13, A14, A15, A7, A26, A27, A30, A33, A31, FINSEQ_3:111, MATRIX_0:24;

hence (Delete (M,i,j)) * (K,U) = M * (K,(U + 1)) by A16, A32, MATRIX_0:def 7; :: thesis: verum