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 1 <= p .. f by FINSEQ_4:21;
then A2: (len f) - 1 >= (len f) - (p .. f) by XREAL_1:10;
len (f :- p) = ((len f) - (p .. f)) + 1 by A1, FINSEQ_5:50;
then (len (f :- p)) - 1 = (len f) - (p .. f) ;
hence len (f :- p) <= len f by A2, XREAL_1:9; :: thesis: verum