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