deffunc H₁( Nat) -> Element of NAT = p |-count (f . $1);
consider g being FinSequence such that
A1: len g = len f and
A2: for k being Nat st k in dom g holds
g . k = H₁(k) from FINSEQ_1:sch 2();

now :: thesis: for y being object st y in rng g holds
y in NAT

let y be object ; :: thesis: ( y in rng g implies y in NAT )
assume y in rng g ; :: thesis: y in NAT
then consider x being object such that
A3: x in dom g and
A4: y = g . x by FUNCT_1:def 3;
reconsider x = x as Element of NAT by A3;
y = H₁(x) by A2, A3, A4;
hence y in NAT ; :: thesis: verum

end;

then rng g c= NAT ;
then reconsider g = g as FinSequence of NAT by FINSEQ_1:def 4;
take g ; :: thesis: ( len g = len f & ( for i being set st i in dom g holds
g . i = p |-count (f . i) ) )
thus len g = len f by A1; :: thesis: for i being set st i in dom g holds
g . i = p |-count (f . i)
let i be set ; :: thesis: ( i in dom g implies g . i = p |-count (f . i) )
assume i in dom g ; :: thesis: g . i = p |-count (f . i)
hence g . i = p |-count (f . i) by A2; :: thesis: verum