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 consider i being Element of NAT such that
A2: i + 1 = p .. f and
A3: f :- p = f /^ i by Th52;
( i <= p .. f & p .. f <= len f ) by A1, A2, FINSEQ_4:31, NAT_1:11;
then i <= len f by XXREAL_0:2;
hence len (f :- p) = (len f) - i by A3, RFINSEQ:def 2
.= ((len f) - (p .. f)) + 1 by A2 ;
:: thesis: verum