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

proof

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

proof

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 A22: U >= J ; :: thesis: (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 < 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)) ) ) )

proof

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

proof

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;

assume A30: U >= J ; :: thesis: (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;

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