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

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