let n, i, j, k, m be Nat; :: thesis: for M being Matrix of n + 1,F_Real
for L being Matrix of n + 1,F_Rat st 0 < n & M = L & [i,j] in Indices M & [k,m] in Indices (Delete (M,i,j)) holds
(Delete (M,i,j)) * (k,m) = (Delete (L,i,j)) * (k,m)
let M be Matrix of n + 1,F_Real; :: thesis: for L being Matrix of n + 1,F_Rat st 0 < n & M = L & [i,j] in Indices M & [k,m] in Indices (Delete (M,i,j)) holds
(Delete (M,i,j)) * (k,m) = (Delete (L,i,j)) * (k,m)
let L be Matrix of n + 1,F_Rat; :: thesis: ( 0 < n & M = L & [i,j] in Indices M & [k,m] in Indices (Delete (M,i,j)) implies (Delete (M,i,j)) * (k,m) = (Delete (L,i,j)) * (k,m) )
assume that
0 < n and
A2: M = L and
A3: [i,j] in Indices M and
A4: [k,m] in Indices (Delete (M,i,j)) ; :: thesis: (Delete (M,i,j)) * (k,m) = (Delete (L,i,j)) * (k,m)
[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) ) ;
( 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) ) ;

per cases ( ( k < i & m < j ) or ( k < i & m >= j ) or ( k >= i & m < j ) or ( k >= i & m >= j ) ) ;

suppose CS1: ( k < i & m < j ) ; :: thesis: (Delete (M,i,j)) * (k,m) = (Delete (L,i,j)) * (k,m)

then F11: (Delete (M,i,j)) * (k,m) = M * (k,m) by LAPLACE:13, A5, D3;
BF11: (Delete (L,i,j)) * (k,m) = L * (k,m) by LAPLACE:13, A5, D3, CS1;
[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) = (Delete (L,i,j)) * (k,m) by A2, F11, BF11, ZMATRLIN:1; :: thesis: verum

end;

suppose CS2: ( k < i & m >= j ) ; :: thesis: (Delete (M,i,j)) * (k,m) = (Delete (L,i,j)) * (k,m)

then F21: (Delete (M,i,j)) * (k,m) = M * (k,(m + 1)) by LAPLACE:13, A5, D3;
BF21: (Delete (L,i,j)) * (k,m) = L * (k,(m + 1)) by LAPLACE:13, A5, D3, CS2;
[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) = (Delete (L,i,j)) * (k,m) by A2, F21, BF21, ZMATRLIN:1; :: thesis: verum

end;

suppose CS3: ( k >= i & m < j ) ; :: thesis: (Delete (M,i,j)) * (k,m) = (Delete (L,i,j)) * (k,m)

then F31: (Delete (M,i,j)) * (k,m) = M * ((k + 1),m) by LAPLACE:13, A5, D3;
BF31: (Delete (L,i,j)) * (k,m) = L * ((k + 1),m) by LAPLACE:13, A5, CS3, 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) = (Delete (L,i,j)) * (k,m) by A2, F31, BF31, ZMATRLIN:1; :: thesis: verum

end;

suppose CS4: ( k >= i & m >= j ) ; :: thesis: (Delete (M,i,j)) * (k,m) = (Delete (L,i,j)) * (k,m)

then F41: (Delete (M,i,j)) * (k,m) = M * ((k + 1),(m + 1)) by LAPLACE:13, A5, D3;
BF41: (Delete (L,i,j)) * (k,m) = L * ((k + 1),(m + 1)) by LAPLACE:13, A5, D3, CS4;
[(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) = (Delete (L,i,j)) * (k,m) by A2, F41, BF41, ZMATRLIN:1; :: thesis: verum

end;

end;