deffunc H₁( Nat) -> Element of the carrier of G = (f /. $1) " ;
ex p being FinSequence st
( len p = len f & ( 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 f and
A2: for k being Nat st k in dom p holds
p . k = H₁(k) ;
rng p c= the carrier of G

proof

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in rng p or y in the carrier of G )
assume y in rng p ; :: thesis: y in the carrier of G
then consider x being object such that
A3: x in dom p and
A4: y = p . x by FUNCT_1:def 3;
reconsider k = x as Nat by A3;
p . k = (f /. k) " by A2, A3;
hence y in the carrier of G by A4; :: thesis: verum

end;

then reconsider q = p as FinSequence of G by FINSEQ_1:def 4;
A5: dom p = dom f by A1, FINSEQ_3:29;
for i being Nat st i in dom f holds
q /. i = (f /. i) "

proof

let i be Nat; :: thesis: ( i in dom f implies q /. i = (f /. i) " )
assume A6: i in dom f ; :: thesis: q /. i = (f /. i) "
hence q /. i = p . i by A5, PARTFUN1:def 6
.= (f /. i) " by A2, A5, A6 ;
:: thesis: verum

end;

hence ex b₁ being FinSequence of G st
( len b₁ = len f & ( for i being Nat st i in dom f holds
b₁ /. i = (f /. i) " ) ) by A1; :: thesis: verum