let k be Nat; :: thesis: for D being non empty set

for p being Element of D

for f being FinSequence of D st p in rng f & k <= len f & k >= p .. f holds

f /. k in rng (f :- p)

let D be non empty set ; :: thesis: for p being Element of D

for f being FinSequence of D st p in rng f & k <= len f & k >= p .. f holds

f /. k in rng (f :- p)

let p be Element of D; :: thesis: for f being FinSequence of D st p in rng f & k <= len f & k >= p .. f holds

f /. k in rng (f :- p)

let f be FinSequence of D; :: thesis: ( p in rng f & k <= len f & k >= p .. f implies f /. k in rng (f :- p) )

assume that

A1: p in rng f and

A2: k <= len f and

A3: k >= p .. f ; :: thesis: f /. k in rng (f :- p)

set x = f /. k;

for p being Element of D

for f being FinSequence of D st p in rng f & k <= len f & k >= p .. f holds

f /. k in rng (f :- p)

let D be non empty set ; :: thesis: for p being Element of D

for f being FinSequence of D st p in rng f & k <= len f & k >= p .. f holds

f /. k in rng (f :- p)

let p be Element of D; :: thesis: for f being FinSequence of D st p in rng f & k <= len f & k >= p .. f holds

f /. k in rng (f :- p)

let f be FinSequence of D; :: thesis: ( p in rng f & k <= len f & k >= p .. f implies f /. k in rng (f :- p) )

assume that

A1: p in rng f and

A2: k <= len f and

A3: k >= p .. f ; :: thesis: f /. k in rng (f :- p)

set x = f /. k;

per cases
( k > p .. f or k = p .. f )
by A3, XXREAL_0:1;

end;

suppose A4:
k > p .. f
; :: thesis: f /. k in rng (f :- p)

reconsider q = f /. k as Element of D ;

1 <= p .. f by A1, FINSEQ_4:21;

then 1 <= k by A3, XXREAL_0:2;

then k in dom f by A2, FINSEQ_3:25;

then A5: q in rng (f /^ (p .. f)) by A4, Th58;

f :- p = <*p*> ^ (f /^ (p .. f)) by FINSEQ_5:def 2;

then rng (f :- p) = (rng <*p*>) \/ (rng (f /^ (p .. f))) by FINSEQ_1:31;

hence f /. k in rng (f :- p) by A5, XBOOLE_0:def 3; :: thesis: verum

end;1 <= p .. f by A1, FINSEQ_4:21;

then 1 <= k by A3, XXREAL_0:2;

then k in dom f by A2, FINSEQ_3:25;

then A5: q in rng (f /^ (p .. f)) by A4, Th58;

f :- p = <*p*> ^ (f /^ (p .. f)) by FINSEQ_5:def 2;

then rng (f :- p) = (rng <*p*>) \/ (rng (f /^ (p .. f))) by FINSEQ_1:31;

hence f /. k in rng (f :- p) by A5, XBOOLE_0:def 3; :: thesis: verum