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 ;
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 ;
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 ;
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 ;
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 ;
BF11: (Delete (L,i,j)) * (k,m) = L * (k,m) by ;
[k,m] in [:(Seg (n + 1)),(Seg (n + 1)):] by ;
then [k,m] in Indices M by MATRIX_0:24;
hence (Delete (M,i,j)) * (k,m) = (Delete (L,i,j)) * (k,m) by ; :: 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 ;
BF21: (Delete (L,i,j)) * (k,m) = L * (k,(m + 1)) by ;
[k,(m + 1)] in [:(Seg (n + 1)),(Seg (n + 1)):] by ;
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 ; :: 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 ;
BF31: (Delete (L,i,j)) * (k,m) = L * ((k + 1),m) by ;
[(k + 1),m] in [:(Seg (n + 1)),(Seg (n + 1)):] by ;
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 ; :: 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 ;
BF41: (Delete (L,i,j)) * (k,m) = L * ((k + 1),(m + 1)) by ;
[(k + 1),(m + 1)] in [:(Seg (n + 1)),(Seg (n + 1)):] by ;
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 ; :: thesis: verum
end;
end;