deffunc H_{1}( 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_{1}(x) ) )
from FUNCT_1:sch 3();

{ {n} where n is Element of RAT : P_{1}[n] } c= rng f
_{1}[n] } is countable
by A1, Lm1; :: thesis: verum

consider f being Function such that

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

f . x = H

{ {n} where n is Element of RAT : P

proof

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

assume x in { {n} where n is Element of RAT : P_{1}[n] }
; :: thesis: x in rng f

then consider n being Element of RAT such that

A2: x = {n} and

P_{1}[n]
;

f . n = x by A1, A2;

hence x in rng f by A1, FUNCT_1:def 3; :: thesis: verum

end;assume x in { {n} where n is Element of RAT : P

then consider n being Element of RAT such that

A2: x = {n} and

P

f . n = x by A1, A2;

hence x in rng f by A1, FUNCT_1:def 3; :: thesis: verum