reconsider m0 = p . 0 as Element of NAT by A1, ORDINAL1:def 12;
deffunc H₁( set ) -> set = p . $1;
ex q being FinSequence st
( len q = m0 & ( for k being Nat st k in dom q holds
q . k = H₁(k) ) ) from FINSEQ_1:sch 2();
then consider q being FinSequence such that
A3: len q = m0 and
A4: for k being Nat st k in dom q holds
q . k = H₁(k) ;
rng q c= D

proof

A5: m0 < len p by A2, Lm1;
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in rng q or y in D )
assume y in rng q ; :: thesis: y in D
then consider x being object such that
A6: x in dom q and
A7: y = q . x by FUNCT_1:def 3;
reconsider k0 = x as Element of NAT by A6;
k0 in Seg m0 by A3, A6, FINSEQ_1:def 3;
then k0 <= m0 by FINSEQ_1:1;
then k0 < len p by A5, XXREAL_0:2;
then A8: k0 in dom p by Lm1;
y = p . k0 by A4, A6, A7;
then ( rng p c= D & y in rng p ) by A8, FUNCT_1:def 3, RELAT_1:def 19;
hence y in D ; :: thesis: verum

end;

then reconsider q0 = q as FinSequence of D by FINSEQ_1:def 4;
A9: dom q = Seg m0 by A3, FINSEQ_1:def 3;
for m being Nat st m = p . 0 holds
( len q0 = m & ( for i being Nat st 1 <= i & i <= m holds
q0 . i = p . i ) ) by A4, A9, FINSEQ_1:1, A3;
hence ex b₁ being FinSequence of D st
for m being Nat st m = p . 0 holds
( len b₁ = m & ( for i being Nat st 1 <= i & i <= m holds
b₁ . i = p . i ) ) ; :: thesis: verum