let n, i, j be Nat; :: thesis: for M being Matrix of n + 1,F_Real st 0 < n & M is Matrix of n + 1,INT & [i,j] in Indices M holds
Delete (M,i,j) is Matrix of n,INT
let M be Matrix of n + 1,F_Real; :: thesis: ( 0 < n & M is Matrix of n + 1,INT & [i,j] in Indices M implies Delete (M,i,j) is Matrix of n,INT )
assume that
A1: 0 < n and
A2: M is Matrix of n + 1,INT and
A3: [i,j] in Indices M ; :: thesis: Delete (M,i,j) is Matrix of n,INT
set M0 = Delete (M,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;
for x being object st x in rng (Delete (M,i,j)) holds
ex p being FinSequence of INT st
( x = p & len p = n )

proof

let x be object ; :: thesis: ( x in rng (Delete (M,i,j)) implies ex p being FinSequence of INT st
( x = p & len p = n ) )
assume S1: x in rng (Delete (M,i,j)) ; :: thesis: ex p being FinSequence of INT st
( x = p & len p = n )
then reconsider p = x as FinSequence of the carrier of F_Real by FINSEQ_2:def 3;
S3: len p = n by S1, X39, MATRIX_0:def 2;
for z being object st z in rng p holds
z in INT

proof

let z be object ; :: thesis: ( z in rng p implies z in INT )
assume z in rng p ; :: thesis: z in INT
then consider j1 being object such that
S4: ( j1 in dom p & z = p . j1 ) by FUNCT_1:def 3;
S5: j1 in Seg n by S3, S4, FINSEQ_1:def 3;
reconsider j1 = j1 as Nat by S4;
consider i1 being object such that
S6: ( i1 in dom (Delete (M,i,j)) & x = (Delete (M,i,j)) . i1 ) by S1, FUNCT_1:def 3;
reconsider i1 = i1 as Nat by S6;
S8: [i1,j1] in Indices (Delete (M,i,j)) by D2, S5, S6, ZFMISC_1:87;
then consider q being FinSequence of F_Real such that
S9: ( q = (Delete (M,i,j)) . i1 & (Delete (M,i,j)) * (i1,j1) = q . j1 ) by MATRIX_0:def 5;
(Delete (M,i,j)) * (i1,j1) is Element of INT by A1, A2, A3, S8, LmSign1F;
hence z in INT by S4, S6, S9; :: thesis: verum

end;

then rng p c= INT ;
then p is FinSequence of INT by FINSEQ_1:def 4;
hence ex p being FinSequence of INT st
( x = p & len p = n ) by S3; :: thesis: verum

end;

hence Delete (M,i,j) is Matrix of n,INT by A1, D2, MATRIX_0:9, MATRIX_0:20; :: thesis: verum