deffunc H₁( object ) -> set = {$1};
consider f being Function such that
A1: ( dom f = RAT & ( for x being object st x in RAT holds
f . x = H₁(x) ) ) from FUNCT_1:sch 3();
{ {n} where n is Element of RAT : P₁[n] } c= rng f

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { {n} where n is Element of RAT : P₁[n] } or x in rng f )
assume x in { {n} where n is Element of RAT : P₁[n] } ; :: thesis: x in rng f
then consider n being Element of RAT such that
A2: x = {n} and
P₁[n] ;
f . n = x by A1, A2;
hence x in rng f by A1, FUNCT_1:def 3; :: thesis: verum

end;

hence { {n} where n is Element of RAT : P₁[n] } is countable by A1, Lm1; :: thesis: verum