let D be non empty set ; :: thesis: for p being Element of D
for f being FinSequence of D
for x being set 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
for x being set 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: for x being set st x in rng f & p in rng f & x .. f <= p .. f holds
x in rng (f -: p)
let x be set ; :: 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)
set g = f -: p;
set i = x .. f;
1 <= x .. f by A1, FINSEQ_4:21;
then A4: x .. f in Seg (p .. f) by A3;
Seg (len (f -: p)) = dom (f -: p) by FINSEQ_1:def 3;
then A5: x .. f in dom (f -: p) by A2, A4, Th42;
then (f -: p) . (x .. f) in rng (f -: p) by FUNCT_1:def 3;
then (f -: p) /. (x .. f) in rng (f -: p) by A5, PARTFUN1:def 6;
then A6: f /. (x .. f) in rng (f -: p) by A2, A4, Th43;
x .. f in dom f by A1, FINSEQ_4:20;
then f . (x .. f) in rng (f -: p) by A6, PARTFUN1:def 6;
hence x in rng (f -: p) by A1, FINSEQ_4:19; :: thesis: verum