consider f being Function such that
A1: ( dom f = NAT & ( for x being set st x in NAT holds
f . x = F₁(x) ) ) from FUNCT_1:sch 3();
{ F₁(n) where n is Element of NAT : P₁[n] } c= rng f

proof

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

end;

hence { F₁(n) where n is Element of NAT : P₁[n] } is countable by A1, CARD_3:127; :: thesis: verum