let j 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 & j + 1 in dom (f :- p) holds
j + (p .. f) in dom f
let D be non empty set ; :: thesis: for p being Element of D
for f being FinSequence of D st p in rng f & j + 1 in dom (f :- p) holds
j + (p .. f) in dom f
let p be Element of D; :: thesis: for f being FinSequence of D st p in rng f & j + 1 in dom (f :- p) holds
j + (p .. f) in dom f
let f be FinSequence of D; :: thesis: ( p in rng f & j + 1 in dom (f :- p) implies j + (p .. f) in dom f )
assume that
A1: p in rng f and
A2: j + 1 in dom (f :- p) ; :: thesis: j + (p .. f) in dom f
j + 1 <= len (f :- p) by A2, FINSEQ_3:25;
then j + 1 <= ((len f) - (p .. f)) + 1 by A1, Th50;
then j <= (len f) - (p .. f) by XREAL_1:6;
then A3: j + (p .. f) <= len f by XREAL_1:19;
A4: p .. f <= j + (p .. f) by NAT_1:11;
1 <= p .. f by A1, FINSEQ_4:21;
then 1 <= j + (p .. f) by A4, XXREAL_0:2;
hence j + (p .. f) in dom f by A3, FINSEQ_3:25; :: thesis: verum