let n, i, j 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 holds

Delete (M,i,j) = Delete (L,i,j)

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 holds

Delete (M,i,j) = Delete (L,i,j)

let L be Matrix of n + 1,F_Rat; :: thesis: ( 0 < n & M = L & [i,j] in Indices M implies Delete (M,i,j) = Delete (L,i,j) )

assume that

A1: 0 < n and

A2: M = L and

A3: [i,j] in Indices M ; :: thesis: Delete (M,i,j) = Delete (L,i,j)

set M0 = Delete (M,i,j);

set L0 = Delete (L,i,j);

X39: (n + 1) -' 1 = n by NAT_D:34;

then D2: ( 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;

BD2: ( len (Delete (L,i,j)) = n & width (Delete (L,i,j)) = n & Indices (Delete (L,i,j)) = [:(Seg n),(Seg n):] ) by MATRIX_0:24, X39;

for i1, j1 being Nat st [i1,j1] in Indices (Delete (M,i,j)) holds

(Delete (M,i,j)) * (i1,j1) = (Delete (L,i,j)) * (i1,j1) by LmSign1F, A1, A2, A3;

hence Delete (M,i,j) = Delete (L,i,j) by BD2, D2, ZMATRLIN:4; :: thesis: verum

for L being Matrix of n + 1,F_Rat st 0 < n & M = L & [i,j] in Indices M holds

Delete (M,i,j) = Delete (L,i,j)

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 holds

Delete (M,i,j) = Delete (L,i,j)

let L be Matrix of n + 1,F_Rat; :: thesis: ( 0 < n & M = L & [i,j] in Indices M implies Delete (M,i,j) = Delete (L,i,j) )

assume that

A1: 0 < n and

A2: M = L and

A3: [i,j] in Indices M ; :: thesis: Delete (M,i,j) = Delete (L,i,j)

set M0 = Delete (M,i,j);

set L0 = Delete (L,i,j);

X39: (n + 1) -' 1 = n by NAT_D:34;

then D2: ( 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;

BD2: ( len (Delete (L,i,j)) = n & width (Delete (L,i,j)) = n & Indices (Delete (L,i,j)) = [:(Seg n),(Seg n):] ) by MATRIX_0:24, X39;

for i1, j1 being Nat st [i1,j1] in Indices (Delete (M,i,j)) holds

(Delete (M,i,j)) * (i1,j1) = (Delete (L,i,j)) * (i1,j1) by LmSign1F, A1, A2, A3;

hence Delete (M,i,j) = Delete (L,i,j) by BD2, D2, ZMATRLIN:4; :: thesis: verum