deffunc H₁( Nat) -> set = q . ($1 + 1);
ex p being XFinSequence st
( len p = len q & ( for k being Nat st k in len q holds
p . k = H₁(k) ) ) from AFINSQ_1:sch 2();
then consider p being XFinSequence such that
A1: len p = len q and
A2: for k being Nat st k in len q holds
p . k = H₁(k) ;
rng p c= D

proof

let y be set ; :: according to TARSKI:def 3 :: thesis: ( not y in rng p or y in D )
A3: rng q c= D by FINSEQ_1:def 4;
assume y in rng p ; :: thesis: y in D
then consider x being set such that
A4: x in dom p and
A5: y = p . x by FUNCT_1:def 3;
reconsider nx = x as Element of NAT by A4;
nx < len q by A1, A4, NAT_1:44;
then A6: nx + 1 <= len q by NAT_1:13;
0 + 1 <= nx + 1 by NAT_1:13;
then nx + 1 in Seg (len q) by A6, FINSEQ_1:1;
then nx + 1 in dom q by FINSEQ_1:def 3;
then A7: q . (nx + 1) in rng q by FUNCT_1:def 3;
p . nx = q . (nx + 1) by A1, A2, A4;
hence y in D by A5, A7, A3; :: thesis: verum

end;

then A8: p is XFinSequence of D by RELAT_1:def 19;
for i being Nat st i < len q holds
q . (i + 1) = p . i

proof

let i be Nat; :: thesis: ( i < len q implies q . (i + 1) = p . i )
assume i < len q ; :: thesis: q . (i + 1) = p . i
then ( i in NAT & i in len q ) by NAT_1:44, ORDINAL1:def 12;
hence q . (i + 1) = p . i by A2; :: thesis: verum

end;

hence ex b₁ being XFinSequence of D st
( len b₁ = len q & ( for i being Nat st i < len q holds
q . (i + 1) = b₁ . i ) ) by A1, A8; :: thesis: verum