let n, i, j, k, m be Nat; for M being Matrix of n + 1,F_Real st 0 < n & M is Matrix of n + 1,INT & [i,j] in Indices M & [k,m] in Indices (Delete (M,i,j)) holds
(Delete (M,i,j)) * (k,m) is Element of INT
let M be Matrix of n + 1,F_Real; ( 0 < n & M is Matrix of n + 1,INT & [i,j] in Indices M & [k,m] in Indices (Delete (M,i,j)) implies (Delete (M,i,j)) * (k,m) is Element of INT )
assume that
0 < n
and
A2:
M is Matrix of n + 1,INT
and
A3:
[i,j] in Indices M
and
A4:
[k,m] in Indices (Delete (M,i,j))
; (Delete (M,i,j)) * (k,m) is Element of INT
[i,j] in [:(Seg (n + 1)),(Seg (n + 1)):]
by A3, MATRIX_0:24;
then A5:
( i in Seg (n + 1) & j in Seg (n + 1) )
by ZFMISC_1:87;
set M0 = Delete (M,i,j);
(n + 1) -' 1 = n
by NAT_D:34;
then
( len (Delete (M,i,j)) = n & width (Delete (M,i,j)) = n & Indices (Delete (M,i,j)) = [:(Seg n),(Seg n):] )
by MATRIX_0:24;
then D5:
( k in Seg n & m in Seg n )
by A4, ZFMISC_1:87;
then D3:
( k in Seg ((n + 1) -' 1) & m in Seg ((n + 1) -' 1) )
by NAT_D:34;
FC0:
( 1 <= k & k <= n & 1 <= m & m <= n )
by FINSEQ_1:1, D5;
then
( 1 <= k & k + 0 <= n + 1 & 1 <= m & m + 0 <= n + 1 )
by XREAL_1:7;
then FC1:
( k in Seg (n + 1) & m in Seg (n + 1) )
by FINSEQ_1:1;
( 1 + 0 <= k + 1 & k + 1 <= n + 1 & 1 + 0 <= m + 1 & m + 1 <= n + 1 )
by FC0, XREAL_1:6;
then FC3:
( k + 1 in Seg (n + 1) & m + 1 in Seg (n + 1) )
by FINSEQ_1:1;
per cases
( ( k < i & m < j ) or ( k < i & m >= j ) or ( k >= i & m < j ) or ( k >= i & m >= j ) )
;
suppose
(
k < i &
m < j )
;
(Delete (M,i,j)) * (k,m) is Element of INT then F11:
(Delete (M,i,j)) * (
k,
m)
= M * (
k,
m)
by LAPLACE:13, A5, D3;
[k,m] in [:(Seg (n + 1)),(Seg (n + 1)):]
by FC1, ZFMISC_1:87;
then
[k,m] in Indices M
by MATRIX_0:24;
hence
(Delete (M,i,j)) * (
k,
m) is
Element of
INT
by A2, F11, LmSign1B;
verum end; suppose
(
k < i &
m >= j )
;
(Delete (M,i,j)) * (k,m) is Element of INT then F21:
(Delete (M,i,j)) * (
k,
m)
= M * (
k,
(m + 1))
by LAPLACE:13, A5, D3;
[k,(m + 1)] in [:(Seg (n + 1)),(Seg (n + 1)):]
by FC1, FC3, ZFMISC_1:87;
then
[k,(m + 1)] in Indices M
by MATRIX_0:24;
hence
(Delete (M,i,j)) * (
k,
m) is
Element of
INT
by A2, F21, LmSign1B;
verum end; suppose
(
k >= i &
m < j )
;
(Delete (M,i,j)) * (k,m) is Element of INT then F31:
(Delete (M,i,j)) * (
k,
m)
= M * (
(k + 1),
m)
by LAPLACE:13, A5, D3;
[(k + 1),m] in [:(Seg (n + 1)),(Seg (n + 1)):]
by FC1, FC3, ZFMISC_1:87;
then
[(k + 1),m] in Indices M
by MATRIX_0:24;
hence
(Delete (M,i,j)) * (
k,
m) is
Element of
INT
by A2, F31, LmSign1B;
verum end; suppose
(
k >= i &
m >= j )
;
(Delete (M,i,j)) * (k,m) is Element of INT then F41:
(Delete (M,i,j)) * (
k,
m)
= M * (
(k + 1),
(m + 1))
by LAPLACE:13, A5, D3;
[(k + 1),(m + 1)] in [:(Seg (n + 1)),(Seg (n + 1)):]
by FC3, ZFMISC_1:87;
then
[(k + 1),(m + 1)] in Indices M
by MATRIX_0:24;
hence
(Delete (M,i,j)) * (
k,
m) is
Element of
INT
by A2, F41, LmSign1B;
verum end;