consider f being Function such that

A1: ( dom f = NAT & ( for x being object st x in NAT holds

f . x = F_{1}(x) ) )
from FUNCT_1:sch 3();

{ F_{1}(n) where n is Nat : P_{1}[n] } c= rng f
_{1}(n) where n is Nat : P_{1}[n] } is countable
by A1, CARD_3:93; :: thesis: verum

A1: ( dom f = NAT & ( for x being object st x in NAT holds

f . x = F

{ F

proof

hence
{ F
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { F_{1}(n) where n is Nat : P_{1}[n] } or x in rng f )

assume x in { F_{1}(n) where n is Nat : P_{1}[n] }
; :: thesis: x in rng f

then consider n being Nat such that

A2: x = F_{1}(n)
and

P_{1}[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;assume x in { F

then consider n being Nat such that

A2: x = F

P

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