let D be non empty set ; :: thesis: for p being Element of D
for f being FinSequence of D holds p in rng (f :- p)
let p be Element of D; :: thesis: for f being FinSequence of D holds p in rng (f :- p)
let f be FinSequence of D; :: thesis: p in rng (f :- p)
rng <*p*> = {p} by FINSEQ_1:39;
then A1: p in rng <*p*> by TARSKI:def 1;
f :- p = <*p*> ^ (f /^ (p .. f)) by FINSEQ_5:def 2;
then rng (f :- p) = (rng <*p*>) \/ (rng (f /^ (p .. f))) by FINSEQ_1:31;
hence p in rng (f :- p) by A1, XBOOLE_0:def 3; :: thesis: verum