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)

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;

end;

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;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