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
let p be Element of D; :: thesis: for f being FinSequence of D st p in rng f holds
len (f :- p) <= len f
let f be FinSequence of D; :: thesis: ( p in rng f implies len (f :- p) <= len f )
assume A1: p in rng f ; :: thesis: len (f :- p) <= len f
then len (f :- p) = ((len f) - (p .. f)) + 1 by FINSEQ_5:53;
then A2: (len (f :- p)) - 1 = (len f) - (p .. f) ;
1 <= p .. f by A1, FINSEQ_4:31;
then (len f) - 1 >= (len f) - (p .. f) by XREAL_1:12;
hence len (f :- p) <= len f by A2, XREAL_1:11; :: thesis: verum