deffunc H₁( Nat) -> Element of NAT = (f . $1) mod m;
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();
rng g c= NAT

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in rng g or x in NAT )
assume x in rng g ; :: thesis: x in NAT
then consider y being set such that
A3: y in dom g and
A4: x = g . y by FUNCT_1:def 5;
reconsider y = y as Element of NAT by A3;
g . y = (f . y) mod m by A2, A3;
hence x in NAT by A4; :: thesis: verum

end;

then reconsider g = g as FinSequence of NAT by FINSEQ_1:def 4;
take g ; :: thesis: ( len g = len f & ( for i being Nat st i in dom f holds
g . i = (f . i) mod m ) )
thus len g = len f by A1; :: thesis: for i being Nat st i in dom f holds
g . i = (f . i) mod m
let k be Nat; :: thesis: ( k in dom f implies g . k = (f . k) mod m )
assume k in dom f ; :: thesis: g . k = (f . k) mod m
then k in dom g by A1, FINSEQ_3:31;
hence g . k = (f . k) mod m by A2; :: thesis: verum