let n be natural number ; :: 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 )
assume A1: x in rng f ; :: thesis: ( x in rng (Del f,n) or x = f . n )
then consider j being set such that
A2: ( j in dom f & x = f . j ) by FUNCT_1:def 5;
reconsider n' = n as Element of NAT by ORDINAL1:def 13;
assume A3: not x in rng (Del f,n) ; :: thesis: x = f . n
assume A4: not x = f . n ; :: thesis: contradiction
for X being set st card X = 0 holds
X = {} ;
then consider m being natural number such that
A5: len f = m + 1 by NAT_1:6, A1, RELAT_1:60;
reconsider m' = m as Element of NAT by ORDINAL1:def 13;
A6: n in dom f by A1, A3, FINSEQ_3:113;
then A7: len (Del f,n) = m by A5, FINSEQ_3:118;
A8: j in Seg (m + 1) by A5, A2, FINSEQ_1:def 3;
reconsider j = j as Element of NAT by A2;
n in Seg (m + 1) by A5, A6, FINSEQ_1:def 3;
then A9: ( 1 <= n & n <= m + 1 ) by FINSEQ_1:3;

per cases ( j < n' or j >= n' ) ;

suppose A10: j < n' ; :: thesis: contradiction

then ( len f = m' + 1 & j < n' ) by A5;
then (Del f,n') . j = f . j by FINSEQ_3:119;
then not j in dom (Del f,n) by A2, A3, FUNCT_1:def 5;
then not j in Seg m by A7, FINSEQ_1:def 3;
then ( j < 1 or j > m ) ;
then ( j > m & j <= m + 1 ) by A8, FINSEQ_1:3;
hence contradiction by A9, A10, NAT_1:8; :: thesis: verum

end;

suppose A11: j >= n' ; :: thesis: contradiction

set j' = j -' 1;
j > n' by A11, A4, A2, XXREAL_0:1;
then j >= n' + 1 by NAT_1:13;
then A12: j - 1 >= (n' + 1) - 1 by XREAL_1:11;
j <= m + 1 by A8, FINSEQ_1:3;
then j - 1 <= (m + 1) - 1 by XREAL_1:11;
then A13: ( len f = m' + 1 & n' in dom f & n' <= j -' 1 & j -' 1 <= m' ) by A5, A12, XREAL_0:def 2, A1, A3, FINSEQ_3:113;
then A14: (Del f,n') . (j -' 1) = f . ((j -' 1) + 1) by FINSEQ_3:120;
j -' 1 >= n' by A12, XREAL_0:def 2;
then j -' 1 >= 1 by A9, XXREAL_0:2;
then j -' 1 in Seg m by A13;
then j -' 1 in dom (Del f,n) by A7, FINSEQ_1:def 3;
then f . j <> f . ((j -' 1) + 1) by A2, A3, A14, FUNCT_1:def 5;
then f . j <> f . ((j - 1) + 1) by A12, XREAL_0:def 2;
hence contradiction ; :: thesis: verum

end;

end;