let n be Nat; :: thesis:
let K be Field; :: thesis:
let M be Matrix of n,K; :: thesis:
let i, j be Nat; :: thesis:
assume that
A1: i in Seg n and
A2: j in Seg n ; :: thesis:
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:
assume that
A4: k in Seg (n -' 1) and
A5: m in Seg (n -' 1) ; :: thesis:
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) ) ) )

assume A18: K >= I ; :: thesis:
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:

A21: width M = n by MATRIX_1:25;
assume U < J ; :: thesis:
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:

end;

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

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

proof

assume A29: U < J ; :: thesis:
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:

end;

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

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: