let k be Nat; :: thesis: for D being non empty set

for p being Element of D

for f being FinSequence of D st p in rng f & p .. f > k holds

p in rng (f /^ k)

let D be non empty set ; :: thesis: for p being Element of D

for f being FinSequence of D st p in rng f & p .. f > k holds

p in rng (f /^ k)

let p be Element of D; :: thesis: for f being FinSequence of D st p in rng f & p .. f > k holds

p in rng (f /^ k)

let f be FinSequence of D; :: thesis: ( p in rng f & p .. f > k implies p in rng (f /^ k) )

assume that

A1: p in rng f and

A2: p .. f > k ; :: thesis: p in rng (f /^ k)

A3: k + (p .. (f /^ k)) = p .. f by A1, A2, Th56;

then p .. (f /^ k) <> 0 by A2;

then A4: 1 <= p .. (f /^ k) by NAT_1:14;

p .. f <= len f by A1, FINSEQ_4:21;

then k <= len f by A2, XXREAL_0:2;

then len (f /^ k) = (len f) - k by RFINSEQ:def 1;

then A5: (len (f /^ k)) + k = len f ;

k + (p .. (f /^ k)) <= len f by A1, A3, FINSEQ_4:21;

then p .. (f /^ k) <= len (f /^ k) by A5, XREAL_1:6;

then A6: p .. (f /^ k) in dom (f /^ k) by A4, FINSEQ_3:25;

then (f /^ k) /. (p .. (f /^ k)) in rng (f /^ k) by PARTFUN2:2;

then f /. (k + (p .. (f /^ k))) in rng (f /^ k) by A6, FINSEQ_5:27;

hence p in rng (f /^ k) by A1, A3, FINSEQ_5:38; :: thesis: verum

for p being Element of D

for f being FinSequence of D st p in rng f & p .. f > k holds

p in rng (f /^ k)

let D be non empty set ; :: thesis: for p being Element of D

for f being FinSequence of D st p in rng f & p .. f > k holds

p in rng (f /^ k)

let p be Element of D; :: thesis: for f being FinSequence of D st p in rng f & p .. f > k holds

p in rng (f /^ k)

let f be FinSequence of D; :: thesis: ( p in rng f & p .. f > k implies p in rng (f /^ k) )

assume that

A1: p in rng f and

A2: p .. f > k ; :: thesis: p in rng (f /^ k)

A3: k + (p .. (f /^ k)) = p .. f by A1, A2, Th56;

then p .. (f /^ k) <> 0 by A2;

then A4: 1 <= p .. (f /^ k) by NAT_1:14;

p .. f <= len f by A1, FINSEQ_4:21;

then k <= len f by A2, XXREAL_0:2;

then len (f /^ k) = (len f) - k by RFINSEQ:def 1;

then A5: (len (f /^ k)) + k = len f ;

k + (p .. (f /^ k)) <= len f by A1, A3, FINSEQ_4:21;

then p .. (f /^ k) <= len (f /^ k) by A5, XREAL_1:6;

then A6: p .. (f /^ k) in dom (f /^ k) by A4, FINSEQ_3:25;

then (f /^ k) /. (p .. (f /^ k)) in rng (f /^ k) by PARTFUN2:2;

then f /. (k + (p .. (f /^ k))) in rng (f /^ k) by A6, FINSEQ_5:27;

hence p in rng (f /^ k) by A1, A3, FINSEQ_5:38; :: thesis: verum