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 ;
suppose A4: k > p .. f ; :: thesis: f /. k in rng (f :- p)
reconsider q = f /. k as Element of D ;
1 <= p .. f by ;
then 1 <= k by ;
then k in dom f by ;
then A5: q in rng (f /^ (p .. f)) by ;
f :- p = <*p*> ^ (f /^ (p .. f)) by FINSEQ_5:def 2;
then rng (f :- p) = () \/ (rng (f /^ (p .. f))) by FINSEQ_1:31;
hence f /. k in rng (f :- p) by ; :: thesis: verum
end;
suppose k = p .. f ; :: thesis: f /. k in rng (f :- p)
then f /. k = p by ;
hence f /. k in rng (f :- p) by Th61; :: thesis: verum
end;
end;