reconsider m0 = p . 0 as Element of NAT by A1, ORDINAL1:def 13;
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
A2: ( len q = m0 & ( for k being Nat st k in dom q holds
q . k = H₁(k) ) ) ;
A3: dom q = Seg m0 by A2, FINSEQ_1:def 3;
rng q c= D

proof

let y be set ; :: 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 set such that
A4: ( x in dom q & y = q . x ) by FUNCT_1:def 5;
reconsider k0 = x as Element of NAT by A4;
A6: k0 in Seg m0 by A2, A4, FINSEQ_1:def 3;
A7: ( q . k0 = p . k0 & y = p . k0 ) by A2, A4;
A8: ( 1 <= k0 & k0 <= m0 ) by A6, FINSEQ_1:3;
A9: rng p c= D by RELAT_1:def 19;
m0 < len p by A1, NAT_1:45;
then k0 < len p by A8, XXREAL_0:2;
then k0 in dom p by NAT_1:45;
then y in rng p by A7, FUNCT_1:def 5;
hence y in D by A9; :: thesis: verum

end;

then reconsider q0 = q as FinSequence of D by FINSEQ_1:def 4;
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 ) )

proof

let m be Nat; :: thesis: ( m = p . 0 implies ( len q0 = m & ( for i being Nat st 1 <= i & i <= m holds
q0 . i = p . i ) ) )
assume A10: m = p . 0 ; :: thesis: ( len q0 = m & ( for i being Nat st 1 <= i & i <= m holds
q0 . i = p . i ) )
for i being Nat st 1 <= i & i <= m0 holds
q0 . i = p . i

proof

let i be Nat; :: thesis: ( 1 <= i & i <= m0 implies q0 . i = p . i )
assume ( 1 <= i & i <= m0 ) ; :: thesis: q0 . i = p . i
then i in Seg m0 by FINSEQ_1:3;
hence q0 . i = p . i by A2, A3; :: thesis: verum

end;

hence ( len q0 = m & ( for i being Nat st 1 <= i & i <= m holds
q0 . i = p . i ) ) by A2, A10; :: thesis: verum

end;

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