set p = f /^ n;
deffunc H₁( Element of NAT ) -> set = f . ($1 + n);

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

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 & ( for m being Element of NAT st m in dom (f /^ n) holds
(f /^ n) . m = H₁(m) ) ) by A1, Def2;
rng (f /^ n) c= rng f

proof

let x be set ; :: 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) & (f /^ n) . m = x ) by FINSEQ_2:11;
A4: (f /^ n) . m = f . (m + n) by A1, A3, Def2;
( 1 <= m & m <= len (f /^ n) & m <= m + n ) by A3, FINSEQ_3:27, NAT_1:11;
then ( 1 <= m + n & m + n <= len f ) by A2, XREAL_1:21, XXREAL_0:2;
then m + n in dom f by FINSEQ_3:27;
hence x in rng f by A3, A4, FUNCT_1:def 5; :: thesis: verum

end;

then rng (f /^ n) c= D by XBOOLE_1:1;
hence f /^ n is FinSequence of D by FINSEQ_1:def 4; :: thesis: verum

end;

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

then f /^ n = <*> D by Def2;
hence f /^ n is FinSequence of D ; :: thesis: verum

end;

end;