let D be non empty set ; :: thesis: for p being Element of D
for f being FinSequence of D st p in rng f holds
len (f :- p) = ((len f) - (p .. f)) + 1
let p be Element of D; :: thesis: for f being FinSequence of D st p in rng f holds
len (f :- p) = ((len f) - (p .. f)) + 1
let f be FinSequence of D; :: thesis: ( p in rng f implies len (f :- p) = ((len f) - (p .. f)) + 1 )
assume A1: p in rng f ; :: thesis: len (f :- p) = ((len f) - (p .. f)) + 1
then A2: p .. f <= len f by FINSEQ_4:21;
consider i being Element of NAT such that
A3: i + 1 = p .. f and
A4: f :- p = f /^ i by A1, Th49;
i <= p .. f by A3, NAT_1:11;
then i <= len f by A2, XXREAL_0:2;
hence len (f :- p) = (len f) - i by A4, RFINSEQ:def 1
.= ((len f) - (p .. f)) + 1 by A3 ;
:: thesis: verum