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
rng (f :- p) c= rng f
let p be Element of D; :: thesis: for f being FinSequence of D st p in rng f holds
rng (f :- p) c= rng f
let f be FinSequence of D; :: thesis: ( p in rng f implies rng (f :- p) c= rng f )
assume p in rng f ; :: thesis: rng (f :- p) c= rng f
then ex i being Element of NAT st
( i + 1 = p .. f & f :- p = f /^ i ) by Th49;
hence rng (f :- p) c= rng f by Th33; :: thesis: verum