set IT = { t where t is Element of Funcs (NAT,REAL) : ex c being Real ex N being Element of NAT st
( c > 0 & ( for n being Element of NAT st n >= N holds
( t . n <= c * (f . n) & t . n >= 0 ) ) ) } ;
A1: { t where t is Element of Funcs (NAT,REAL) : ex c being Real ex N being Element of NAT st
( c > 0 & ( for n being Element of NAT st n >= N holds
( t . n <= c * (f . n) & t . n >= 0 ) ) ) } 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 c being Real ex N being Element of NAT st
( c > 0 & ( for n being Element of NAT st n >= N holds
( t . n <= c * (f . n) & t . n >= 0 ) ) ) } or x is set )
assume x in { t where t is Element of Funcs (NAT,REAL) : ex c being Real ex N being Element of NAT st
( c > 0 & ( for n being Element of NAT st n >= N holds
( t . n <= c * (f . n) & t . n >= 0 ) ) ) } ; :: thesis: x is set
then ex t being Element of Funcs (NAT,REAL) st
( x = t & ex c being Real ex N being Element of NAT st
( c > 0 & ( for n being Element of NAT st n >= N holds
( t . n <= c * (f . n) & t . n >= 0 ) ) ) ) ;
hence x is set ; :: thesis: verum
end;
consider N being Nat such that
A2: for n being Nat st n >= N holds
f . n >= 0 by Def2;
A3: N in NAT by ORDINAL1:def 12;
A4: f is Element of Funcs (NAT,REAL) by FUNCT_2:8;
for n being Element of NAT st n >= N holds
( f . n <= 1 * (f . n) & f . n >= 0 ) by A2;
then ex c being Real ex N being Element of NAT st
( c > 0 & ( for n being Element of NAT st n >= N holds
( f . n <= c * (f . n) & f . n >= 0 ) ) ) by A3;
then f in { t where t is Element of Funcs (NAT,REAL) : ex c being Real ex N being Element of NAT st
( c > 0 & ( for n being Element of NAT st n >= N holds
( t . n <= c * (f . n) & t . n >= 0 ) ) ) } by A4;
then reconsider IT1 = { t where t is Element of Funcs (NAT,REAL) : ex c being Real ex N being Element of NAT st
( c > 0 & ( for n being Element of NAT st n >= N holds
( t . n <= c * (f . n) & t . n >= 0 ) ) ) } 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 c being Real ex N being Element of NAT st
( c > 0 & ( for n being Element of NAT st n >= N holds
( t . n <= c * (f . n) & t . n >= 0 ) ) ) } ;
then ex t being Element of Funcs (NAT,REAL) st
( x = t & ex c being Real ex N being Element of NAT st
( c > 0 & ( for n being Element of NAT st n >= N holds
( t . n <= c * (f . n) & t . n >= 0 ) ) ) ) ;
hence x is sequence of REAL ; :: thesis: verum
end;
hence { t where t is Element of Funcs (NAT,REAL) : ex c being Real ex N being Element of NAT st
( c > 0 & ( for n being Element of NAT st n >= N holds
( t . n <= c * (f . n) & t . n >= 0 ) ) ) } is FUNCTION_DOMAIN of NAT , REAL by FUNCT_2:def 12; :: thesis: verum