set IT = { t where t is Element of Funcs NAT ,REAL : ex f, g being Element of Funcs NAT ,REAL ex N being Element of NAT st
( f in F & g in G & ( for n being Element of NAT st n >= N holds
t . n = (f . n) to_power (g . n) ) ) } ;

A1: now

consider g being set such that
A2: g in G by XBOOLE_0:def 1;
g is Function of NAT ,REAL by A2, FUNCT_2:def 13;
then reconsider g = g as Element of Funcs NAT ,REAL by FUNCT_2:11;
consider f being set such that
A3: f in F by XBOOLE_0:def 1;
f is Function of NAT ,REAL by A3, FUNCT_2:def 13;
then reconsider f = f as Element of Funcs NAT ,REAL by FUNCT_2:11;
defpred S₁[ Element of NAT , Real] means $2 = (f . $1) to_power (g . $1);
A4: for x being Element of NAT ex y being Element of REAL st S₁[x,y] ;
consider t being Function of NAT ,REAL such that
A5: for x being Element of NAT holds S₁[x,t . x] from FUNCT_2:sch 3(A4);
reconsider t = t as Element of Funcs NAT ,REAL by FUNCT_2:11;
for x being Element of NAT st x >= 0 holds
t . x = (f . x) to_power (g . x) by A5;
then t in { t where t is Element of Funcs NAT ,REAL : ex f, g being Element of Funcs NAT ,REAL ex N being Element of NAT st
( f in F & g in G & ( for n being Element of NAT st n >= N holds
t . n = (f . n) to_power (g . n) ) ) } by A3, A2;
hence not { t where t is Element of Funcs NAT ,REAL : ex f, g being Element of Funcs NAT ,REAL ex N being Element of NAT st
( f in F & g in G & ( for n being Element of NAT st n >= N holds
t . n = (f . n) to_power (g . n) ) ) } is empty ; :: thesis: verum

end;

{ t where t is Element of Funcs NAT ,REAL : ex f, g being Element of Funcs NAT ,REAL ex N being Element of NAT st
( f in F & g in G & ( for n being Element of NAT st n >= N holds
t . n = (f . n) to_power (g . n) ) ) } is functional

proof

let x be set ; :: according to FUNCT_1:def 19 :: thesis: ( not x in { t where t is Element of Funcs NAT ,REAL : ex f, g being Element of Funcs NAT ,REAL ex N being Element of NAT st
( f in F & g in G & ( for n being Element of NAT st n >= N holds
t . n = (f . n) to_power (g . n) ) ) } or x is set )
assume x in { t where t is Element of Funcs NAT ,REAL : ex f, g being Element of Funcs NAT ,REAL ex N being Element of NAT st
( f in F & g in G & ( for n being Element of NAT st n >= N holds
t . n = (f . n) to_power (g . n) ) ) } ; :: thesis: x is set
then ex t being Element of Funcs NAT ,REAL st
( x = t & ex f, g being Element of Funcs NAT ,REAL ex N being Element of NAT st
( f in F & g in G & ( for n being Element of NAT st n >= N holds
t . n = (f . n) to_power (g . n) ) ) ) ;
hence x is set ; :: thesis: verum

end;

then reconsider IT1 = { t where t is Element of Funcs NAT ,REAL : ex f, g being Element of Funcs NAT ,REAL ex N being Element of NAT st
( f in F & g in G & ( for n being Element of NAT st n >= N holds
t . n = (f . n) to_power (g . 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 f, g being Element of Funcs NAT ,REAL ex N being Element of NAT st
( f in F & g in G & ( for n being Element of NAT st n >= N holds
t . n = (f . n) to_power (g . n) ) ) } ;
then ex t being Element of Funcs NAT ,REAL st
( x = t & ex f, g being Element of Funcs NAT ,REAL ex N being Element of NAT st
( f in F & g in G & ( for n being Element of NAT st n >= N holds
t . n = (f . n) to_power (g . n) ) ) ) ;
hence x is Function of NAT ,REAL ; :: thesis: verum

end;

hence { t where t is Element of Funcs NAT ,REAL : ex f, g being Element of Funcs NAT ,REAL ex N being Element of NAT st
( f in F & g in G & ( for n being Element of NAT st n >= N holds
t . n = (f . n) to_power (g . n) ) ) } is FUNCTION_DOMAIN of NAT , REAL by FUNCT_2:def 13; :: thesis: verum