let n, i, j be Nat; 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; ( 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
; 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 ;
( 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))
;
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 ;
( z in rng p implies z in INT )
assume
z in rng p
;
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;
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;
verum
end;
hence
Delete (M,i,j) is Matrix of n,INT
by A1, D2, MATRIX_0:9, MATRIX_0:20; verum