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) ) ;

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 ) )
;

end;

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

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

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

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