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 ;
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 (f /^ (p .. f))) by FINSEQ_1:31;
q in rng (f /^ (p .. f)) by A1, A4, Th57;
hence x in rng (f :- p) by ; :: thesis: verum
end;
suppose x .. f = p .. f ; :: thesis: x in rng (f :- p)
then x = f . (p .. f) by
.= p by ;
hence x in rng (f :- p) by Th61; :: thesis: verum
end;
end;