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;

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

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;

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

then f /. k = p by A1, FINSEQ_5:38;
hence f /. k in rng (f :- p) by Th61; :: thesis: verum

end;

end;