let i, k be Nat; 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 ; 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; ( k < i & i in dom f implies f /. i in rng (f /^ k) )
assume that
A1:
k < i
and
A2:
i in dom f
; 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; verum