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

for f being FinSequence of D st k < i & i in dom f holds

f /. i in rng (f /^ k)

let D be non empty set ; :: thesis: for f being FinSequence of D st k < i & i in dom f holds

f /. i in rng (f /^ k)

let f be FinSequence of D; :: thesis: ( k < i & i in dom f implies f /. i in rng (f /^ k) )

assume that

A1: k < i and

A2: i in dom f ; :: thesis: f /. i in rng (f /^ k)

reconsider j = i - k as Element of NAT by A1, INT_1:5;

j > 0 by A1, XREAL_1:50;

then A3: 1 <= j by NAT_1:14;

A4: i = j + k ;

A5: i <= len f by A2, FINSEQ_3:25;

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

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

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

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

then A6: j in dom (f /^ k) by A3, FINSEQ_3:25;

then f /. i = (f /^ k) /. j by A4, FINSEQ_5:27;

hence f /. i in rng (f /^ k) by A6, PARTFUN2:2; :: thesis: verum

for f being FinSequence of D st k < i & i in dom f holds

f /. i in rng (f /^ k)

let D be non empty set ; :: thesis: for f being FinSequence of D st k < i & i in dom f holds

f /. i in rng (f /^ k)

let f be FinSequence of D; :: thesis: ( k < i & i in dom f implies f /. i in rng (f /^ k) )

assume that

A1: k < i and

A2: i in dom f ; :: thesis: f /. i in rng (f /^ k)

reconsider j = i - k as Element of NAT by A1, INT_1:5;

j > 0 by A1, XREAL_1:50;

then A3: 1 <= j by NAT_1:14;

A4: i = j + k ;

A5: i <= len f by A2, FINSEQ_3:25;

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

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

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

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

then A6: j in dom (f /^ k) by A3, FINSEQ_3:25;

then f /. i = (f /^ k) /. j by A4, FINSEQ_5:27;

hence f /. i in rng (f /^ k) by A6, PARTFUN2:2; :: thesis: verum