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

proof

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

end;

hence { F₁(n) where n is Nat : P₁[n] } is countable by A1, CARD_3:93; :: thesis: verum