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 :: thesis: 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

consider g being object such that
A2: g in G by XBOOLE_0:def 1;
g is sequence of REAL by A2, FUNCT_2:def 12;
then reconsider g = g as Element of Funcs (NAT,REAL) by FUNCT_2:8;
consider f being object such that
A3: f in F by XBOOLE_0:def 1;
f is sequence of REAL by A3, FUNCT_2:def 12;
then reconsider f = f as Element of Funcs (NAT,REAL) by FUNCT_2:8;
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]

proof

let x be Element of NAT ; :: thesis: ex y being Element of REAL st S₁[x,y]
reconsider y = (f . x) to_power (g . x) as Element of REAL by XREAL_0:def 1;
take y ; :: thesis: S₁[x,y]
thus S₁[x,y] ; :: thesis: verum

end;

consider t being sequence of 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:8;
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 object ; :: according to FUNCT_1:def 13 :: 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 :: thesis: for x being Element of IT1 holds x is sequence of REAL

let x be Element of IT1; :: thesis: x is sequence of 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 sequence of 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 12; :: thesis: verum