let n, i, j, k, m be Nat; :: thesis: 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; :: thesis: ( 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)) ; :: thesis: (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 ) ; :: thesis: (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; :: thesis: verum

end;

suppose ( k < i & m >= j ) ; :: thesis: (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; :: thesis: verum

end;

suppose ( k >= i & m < j ) ; :: thesis: (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; :: thesis: verum

end;

suppose ( k >= i & m >= j ) ; :: thesis: (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; :: thesis: verum

end;

end;