let x be set ; :: thesis: for D being non empty set
for p being Element of D
for f being FinSequence of D st x in rng f & p in rng f & x .. f >= p .. f holds
x in rng (f :- p)
let D be non empty set ; :: thesis: for p being Element of D
for f being FinSequence of D st x in rng f & p in rng f & x .. f >= p .. f holds
x in rng (f :- p)
let p be Element of D; :: thesis: for f being FinSequence of D st x in rng f & p in rng f & x .. f >= p .. f holds
x in rng (f :- p)
let f be FinSequence of D; :: thesis: ( x in rng f & p in rng f & x .. f >= p .. f implies x in rng (f :- p) )
assume that
A1: x in rng f and
A2: p in rng f and
A3: x .. f >= p .. f ; :: thesis: x in rng (f :- p)

per cases ( x .. f > p .. f or x .. f = p .. f ) by A3, XXREAL_0:1;

suppose A4: x .. f > p .. f ; :: thesis: x in rng (f :- p)

rng f c= D by FINSEQ_1:def 4;
then reconsider q = x as Element of D by A1;
f :- p = <*p*> ^ (f /^ (p .. f)) by FINSEQ_5:def 2;
then A5: rng (f :- p) = (rng <*p*>) \/ (rng (f /^ (p .. f))) by FINSEQ_1:31;
q in rng (f /^ (p .. f)) by A1, A4, Th57;
hence x in rng (f :- p) by A5, XBOOLE_0:def 3; :: thesis: verum

end;

suppose x .. f = p .. f ; :: thesis: x in rng (f :- p)

then x = f . (p .. f) by A1, FINSEQ_4:19
.= p by A2, FINSEQ_4:19 ;
hence x in rng (f :- p) by Th61; :: thesis: verum

end;

end;