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;

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 )
;

end;

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;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

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;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