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

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