set p = f /^ n;

per cases
( n <= len f or len f < n )
;

end;

suppose A1:
n <= len f
; :: thesis: f /^ n is FinSequence of D

then reconsider k = (len f) - n as Element of NAT by NAT_1:21;

A2: len (f /^ n) = k by A1, Def1;

rng (f /^ n) c= rng f

hence f /^ n is FinSequence of D by FINSEQ_1:def 4; :: thesis: verum

end;A2: len (f /^ n) = k by A1, Def1;

rng (f /^ n) c= rng f

proof

then
rng (f /^ n) c= D
by XBOOLE_1:1;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in rng (f /^ n) or x in rng f )

assume x in rng (f /^ n) ; :: thesis: x in rng f

then consider m being Nat such that

A3: m in dom (f /^ n) and

A4: (f /^ n) . m = x by FINSEQ_2:10;

m <= len (f /^ n) by A3, FINSEQ_3:25;

then A5: m + n <= len f by A2, XREAL_1:19;

A6: m <= m + n by NAT_1:11;

1 <= m by A3, FINSEQ_3:25;

then 1 <= m + n by A6, XXREAL_0:2;

then A7: m + n in dom f by A5, FINSEQ_3:25;

(f /^ n) . m = f . (m + n) by A1, A3, Def1;

hence x in rng f by A4, A7, FUNCT_1:def 3; :: thesis: verum

end;assume x in rng (f /^ n) ; :: thesis: x in rng f

then consider m being Nat such that

A3: m in dom (f /^ n) and

A4: (f /^ n) . m = x by FINSEQ_2:10;

m <= len (f /^ n) by A3, FINSEQ_3:25;

then A5: m + n <= len f by A2, XREAL_1:19;

A6: m <= m + n by NAT_1:11;

1 <= m by A3, FINSEQ_3:25;

then 1 <= m + n by A6, XXREAL_0:2;

then A7: m + n in dom f by A5, FINSEQ_3:25;

(f /^ n) . m = f . (m + n) by A1, A3, Def1;

hence x in rng f by A4, A7, FUNCT_1:def 3; :: thesis: verum

hence f /^ n is FinSequence of D by FINSEQ_1:def 4; :: thesis: verum