let n be Nat; :: thesis: for f being FinSequence
for x being set st x in rng f & not x in rng (Del (f,n)) holds
x = f . n
let f be FinSequence; :: thesis: for x being set st x in rng f & not x in rng (Del (f,n)) holds
x = f . n
let x be set ; :: thesis: ( x in rng f & not x in rng (Del (f,n)) implies x = f . n )
reconsider n9 = n as Element of NAT by ORDINAL1:def 12;
assume A1: x in rng f ; :: thesis: ( x in rng (Del (f,n)) or x = f . n )
then consider j being object such that
A2: j in dom f and
A3: x = f . j by FUNCT_1:def 3;
for X being set st card X = 0 holds
X = {} ;
then consider m being Nat such that
A4: len f = m + 1 by A1, NAT_1:6, RELAT_1:38;
A5: j in Seg (m + 1) by A2, A4, FINSEQ_1:def 3;
assume A6: not x in rng (Del (f,n)) ; :: thesis: x = f . n
then A7: n in dom f by A1, FINSEQ_3:104;
then A8: len (Del (f,n)) = m by A4, FINSEQ_3:109;
A9: n in Seg (m + 1) by A4, A7, FINSEQ_1:def 3;
then A10: 1 <= n by FINSEQ_1:1;
reconsider j = j as Element of NAT by A2;
reconsider m9 = m as Element of NAT by ORDINAL1:def 12;
assume A11: not x = f . n ; :: thesis: contradiction
A12: n <= m + 1 by A9, FINSEQ_1:1;

per cases ( j < n9 or j >= n9 ) ;

suppose A13: j < n9 ; :: thesis: contradiction

then (Del (f,n9)) . j = f . j by FINSEQ_3:110;
then not j in dom (Del (f,n)) by A3, A6, FUNCT_1:def 3;
then not j in Seg m by A8, FINSEQ_1:def 3;
then A14: ( j < 1 or j > m ) ;
j <= m + 1 by A5, FINSEQ_1:1;
hence contradiction by A5, A12, A13, A14, FINSEQ_1:1, NAT_1:8; :: thesis: verum

end;

suppose A15: j >= n9 ; :: thesis: contradiction

set j9 = j -' 1;
j <= m + 1 by A5, FINSEQ_1:1;
then j - 1 <= (m + 1) - 1 by XREAL_1:9;
then A16: j -' 1 <= m9 by XREAL_0:def 2;
j > n9 by A3, A11, A15, XXREAL_0:1;
then j >= n9 + 1 by NAT_1:13;
then A17: j - 1 >= (n9 + 1) - 1 by XREAL_1:9;
then j -' 1 >= n9 by XREAL_0:def 2;
then j -' 1 >= 1 by A10, XXREAL_0:2;
then j -' 1 in Seg m by A16;
then A18: j -' 1 in dom (Del (f,n)) by A8, FINSEQ_1:def 3;
A19: n9 in dom f by A1, A6, FINSEQ_3:104;
n9 <= j -' 1 by A17, XREAL_0:def 2;
then (Del (f,n9)) . (j -' 1) = f . ((j -' 1) + 1) by A4, A19, A16, FINSEQ_3:111;
then f . j <> f . ((j -' 1) + 1) by A3, A6, A18, FUNCT_1:def 3;
then f . j <> f . ((j - 1) + 1) by A17, XREAL_0:def 2;
hence contradiction ; :: thesis: verum

end;

end;