deffunc H₁( Element of NAT ) -> set = f . (D + n);
set p = f /^ n;
A1: rng f c= D by RELAT_1:def 19;

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

suppose A2: n < len f ; :: thesis: f /^ n is D -valued

then reconsider k = (len f) - n as Nat by NAT_1:21;
A3: len (f /^ n) = k by A2, Th16;
A4: 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 Element of NAT such that
A5: m in dom (f /^ n) and
A6: (f /^ n) . m = x by Th3;
m < len (f /^ n) by A5, NAT_1:45;
then m + n < k + n by A3, XREAL_1:8;
then A7: m + n in dom f by NAT_1:45;
(f /^ n) . m = f . (m + n) by A5, Def2;
hence x in rng f by A6, A7, FUNCT_1:def 5; :: thesis: verum

end;

for f2 being XFinSequence st rng f2 c= D holds
f2 is XFinSequence of D by RELAT_1:def 19;
hence f /^ n is D -valued by A1, A4, XBOOLE_1:1; :: thesis: verum

end;

suppose len f <= n ; :: thesis: f /^ n is D -valued

then f /^ n = <%> D by Th15;
hence f /^ n is D -valued ; :: thesis: verum

end;

end;