deffunc H₁( Nat) -> set = q . ($1 -' 1);
ex p being FinSequence st
( len p = len q & ( for k being Nat st k in dom p holds
p . k = H₁(k) ) ) from FINSEQ_1:sch 2();
then consider p being FinSequence such that
A1: len p = len q and
A2: for k being Nat st k in dom p 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 RELAT_1:def 19;
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;
A6: nx in Seg (len q) by A1, A4, FINSEQ_1:def 3;
then 1 <= nx by FINSEQ_1:1;
then nx - 1 >= 0 by XREAL_1:48;
then A7: nx - 1 = nx -' 1 by XREAL_0:def 2;
A8: nx -' 1 < (nx -' 1) + 1 by NAT_1:13;
nx <= len q by A6, FINSEQ_1:1;
then nx -' 1 < len q by A7, A8, XXREAL_0:2;
then nx -' 1 in dom q by NAT_1:44;
then A9: q . (nx -' 1) in rng q by FUNCT_1:def 3;
p . nx = q . (nx -' 1) by A2, A4;
hence y in D by A5, A9, A3; :: thesis: verum

end;

then A10: p is FinSequence of D by FINSEQ_1:def 4;
A11: dom p = Seg (len q) by A1, FINSEQ_1:def 3;
for i being Nat st 1 <= i & i <= len q holds
q . (i -' 1) = p . i

proof

let i be Nat; :: thesis: ( 1 <= i & i <= len q implies q . (i -' 1) = p . i )
assume ( 1 <= i & i <= len q ) ; :: thesis: q . (i -' 1) = p . i
then i in Seg (len q) by FINSEQ_1:1;
hence q . (i -' 1) = p . i by A2, A11; :: thesis: verum

end;

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