set IT = { t where t is Element of Funcs NAT ,REAL : ex c, d being Real ex N being Element of NAT st
( c > 0 & d > 0 & ( for n being Element of NAT st n >= N & n in X holds
( d * (f . n) <= t . n & t . n <= c * (f . n) ) ) ) } ;
A1: { t where t is Element of Funcs NAT ,REAL : ex c, d being Real ex N being Element of NAT st
( c > 0 & d > 0 & ( for n being Element of NAT st n >= N & n in X holds
( d * (f . n) <= t . n & t . n <= c * (f . n) ) ) ) } is functional

proof

let x be set ; :: according to FRAENKEL:def 1 :: thesis: ( not x in { t where t is Element of Funcs NAT ,REAL : ex c, d being Real ex N being Element of NAT st
( c > 0 & d > 0 & ( for n being Element of NAT st n >= N & n in X holds
( d * (f . n) <= t . n & t . n <= c * (f . n) ) ) ) } or x is set )
assume x in { t where t is Element of Funcs NAT ,REAL : ex c, d being Real ex N being Element of NAT st
( c > 0 & d > 0 & ( for n being Element of NAT st n >= N & n in X holds
( d * (f . n) <= t . n & t . n <= c * (f . n) ) ) ) } ; :: thesis: x is set
then ex t being Element of Funcs NAT ,REAL st
( x = t & ex c, d being Real ex N being Element of NAT st
( c > 0 & d > 0 & ( for n being Element of NAT st n >= N & n in X holds
( d * (f . n) <= t . n & t . n <= c * (f . n) ) ) ) ) ;
hence x is set ; :: thesis: verum

end;

A2: f is Element of Funcs NAT ,REAL by FUNCT_2:11;
for n being Element of NAT st n >= 0 & n in X holds
( 1 * (f . n) <= f . n & f . n <= 1 * (f . n) ) ;
then f in { t where t is Element of Funcs NAT ,REAL : ex c, d being Real ex N being Element of NAT st
( c > 0 & d > 0 & ( for n being Element of NAT st n >= N & n in X holds
( d * (f . n) <= t . n & t . n <= c * (f . n) ) ) ) } by A2;
then reconsider IT1 = { t where t is Element of Funcs NAT ,REAL : ex c, d being Real ex N being Element of NAT st
( c > 0 & d > 0 & ( for n being Element of NAT st n >= N & n in X holds
( d * (f . n) <= t . n & t . n <= c * (f . n) ) ) ) } as non empty functional set by A1;

now

let x be Element of IT1; :: thesis: x is Function of NAT , REAL
x in { t where t is Element of Funcs NAT ,REAL : ex c, d being Real ex N being Element of NAT st
( c > 0 & d > 0 & ( for n being Element of NAT st n >= N & n in X holds
( d * (f . n) <= t . n & t . n <= c * (f . n) ) ) ) } ;
then consider t being Element of Funcs NAT ,REAL such that
A3: x = t and
ex c, d being Real ex N being Element of NAT st
( c > 0 & d > 0 & ( for n being Element of NAT st n >= N & n in X holds
( d * (f . n) <= t . n & t . n <= c * (f . n) ) ) ) ;
thus x is Function of NAT , REAL by A3; :: thesis: verum

end;

hence { t where t is Element of Funcs NAT ,REAL : ex c, d being Real ex N being Element of NAT st
( c > 0 & d > 0 & ( for n being Element of NAT st n >= N & n in X holds
( d * (f . n) <= t . n & t . n <= c * (f . n) ) ) ) } is FUNCTION_DOMAIN of NAT , REAL by FRAENKEL:def 2; :: thesis: verum