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:81;
reconsider I = i, J = j, K = k, U = m as Element of NAT by ORDINAL1:def 13;
n9 <= n9 + 1 by NAT_1:11;
then A8: Seg n9 c= Seg n by FINSEQ_1:7;
A9: len M = n by MATRIX_1:25;
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_2:def 6;
len (Delete (M,i,j)) = n9 by A6, MATRIX_1:25;
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_2:18;
width (Delete (M,i,j)) = n9 by A6, MATRIX_1:25;
then A14: (Line ((Delete (M,i,j)),k)) . m = (Delete (M,i,j)) * (k,m) by A5, A6, MATRIX_1:def 8;
A15: Line ((DelLine (M,i)),k) = (DelLine (M,i)) . k by A4, A6, A11, MATRIX_2:18;
A16: m + 1 in Seg (n9 + 1) by A5, A6, FINSEQ_1:81;
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:3;
then A19: (DelLine (M,i)) . K = M . (K + 1) by A1, A9, A10, A7, A18, FINSEQ_3:120;
A20: M . (K + 1) = Line (M,(K + 1)) by A10, A7, MATRIX_2:18;
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_1:25;
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:119;
hence (Delete (M,i,j)) * (K,U) = M * ((K + 1),U) by A5, A6, A8, A21, MATRIX_1:def 8; :: thesis: verum

end;

assume A23: U >= J ; :: thesis: (Delete (M,i,j)) * (K,U) = M * ((K + 1),(U + 1))
A24: U <= n9 by A5, A6, FINSEQ_1:3;
A25: width M = n by MATRIX_1:25;
A26: len (Line ((DelLine (M,i)),K)) = width M by A15, A19, A20, MATRIX_1:def 8;
then J in dom (Line ((DelLine (M,i)),K)) by A2, A25, 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, A23, A26, A24, FINSEQ_3:120, MATRIX_1:25;
hence (Delete (M,i,j)) * (K,U) = M * ((K + 1),(U + 1)) by A16, A25, MATRIX_1:def 8; :: 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 A27: (DelLine (M,i)) . K = M . K by FINSEQ_3:119;
A28: M . K = Line (M,K) by A4, A6, A10, A8, MATRIX_2:18;
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 A29: U < J ; :: thesis: (Delete (M,i,j)) * (K,U) = M * (K,U)
A30: width M = n9 + 1 by MATRIX_1:25;
(Delete (M,i,j)) * (K,U) = (Line (M,K)) . U by A12, A3, A13, A14, A15, A27, A28, A29, FINSEQ_3:119;
hence (Delete (M,i,j)) * (K,U) = M * (K,U) by A5, A6, A8, A30, MATRIX_1:def 8; :: thesis: verum

end;

assume A31: U >= J ; :: thesis: (Delete (M,i,j)) * (K,U) = M * (K,(U + 1))
A32: U <= n9 by A5, A6, FINSEQ_1:3;
A33: width M = n by MATRIX_1:25;
A34: len (Line ((DelLine (M,i)),K)) = width M by A15, A27, A28, MATRIX_1:def 8;
then J in dom (Line ((DelLine (M,i)),K)) by A2, A33, FINSEQ_1:def 3;
then (Delete (M,i,j)) * (K,U) = (Line (M,K)) . (U + 1) by A12, A3, A13, A14, A15, A7, A27, A28, A31, A34, A32, FINSEQ_3:120, MATRIX_1:25;
hence (Delete (M,i,j)) * (K,U) = M * (K,(U + 1)) by A16, A33, MATRIX_1:def 8; :: 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