deffunc H₁( Nat) -> Element of COMPLEX = (z . $1) *' ;
consider p being FinSequence such that
A1: ( len p = len z & ( for k being Nat st k in dom p holds
p . k = H₁(k) ) ) from FINSEQ_1:sch 2();
rng p c= COMPLEX

proof

let s2 be set ; :: according to TARSKI:def 3 :: thesis: ( not s2 in rng p or s2 in COMPLEX )
assume s2 in rng p ; :: thesis: s2 in COMPLEX
then consider s1 being set such that
A2: s1 in dom p and
A3: s2 = p . s1 by FUNCT_1:def 3;
reconsider nx = s1 as Element of NAT by A2;
p . nx = (z . nx) *' by A1, A2;
hence s2 in COMPLEX by A3; :: thesis: verum

end;

then A4: p is FinSequence of COMPLEX by FINSEQ_1:def 4;
for i being Nat st 1 <= i & i <= len z holds
(z . i) *' = p . i

proof

let i be Nat; :: thesis: ( 1 <= i & i <= len z implies (z . i) *' = p . i )
assume ( 1 <= i & i <= len z ) ; :: thesis: (z . i) *' = p . i
then i in dom p by A1, FINSEQ_3:25;
hence (z . i) *' = p . i by A1; :: thesis: verum

end;

hence ex b₁ being FinSequence of COMPLEX st
( len b₁ = len z & ( for i being Nat st 1 <= i & i <= len z holds
b₁ . i = (z . i) *' ) ) by A1, A4; :: thesis: verum