let f, t be positive Real_Sequence; :: thesis: ( t in Big_Omega f iff ex d being Real st
( d > 0 & ( for n being Element of NAT holds d * (f . n) <= t . n ) ) )

hereby :: thesis: ( ex d being Real st
( d > 0 & ( for n being Element of NAT holds d * (f . n) <= t . n ) ) implies t in Big_Omega f )

assume t in Big_Omega f ; :: thesis: ex d being Real st
( d > 0 & ( for n being Element of NAT holds d * (f . n) <= t . n ) )
then consider s being Element of Funcs (NAT,REAL) such that
A1: s = t and
A2: ex d being Real ex N being Element of NAT st
( d > 0 & ( for n being Element of NAT st n >= N holds
( d * (f . n) <= s . n & s . n >= 0 ) ) ) ;
consider d being Real, N being Element of NAT such that
A3: d > 0 and
A4: for n being Element of NAT st n >= N holds
( d * (f . n) <= s . n & s . n >= 0 ) by A2;

per cases ( N = 0 or N > 0 ) ;

suppose A5: N = 0 ; :: thesis: ex d being Real st
( d > 0 & ( for n being Element of NAT holds d * (f . n) <= t . n ) )

take d = d; :: thesis: ( d > 0 & ( for n being Element of NAT holds d * (f . n) <= t . n ) )
thus d > 0 by A3; :: thesis: for n being Element of NAT holds d * (f . n) <= t . n
let n be Element of NAT ; :: thesis: d * (f . n) <= t . n
thus d * (f . n) <= t . n by A1, A4, A5; :: thesis: verum

end;

suppose A6: N > 0 ; :: thesis: ex d being Real st
( d > 0 & ( for n being Element of NAT holds d * (f . n) <= t . n ) )

deffunc H₁( Element of NAT ) -> Element of REAL = (t . $1) / (f . $1);
reconsider B = { H₁(n) where n is Element of NAT : n < N } as non empty finite Subset of REAL from ASYMPT_0:sch 3(A6);
set b = min B;
A7: for n being Element of NAT st n < N holds
(min B) * (f . n) <= t . n

proof

let n be Element of NAT ; :: thesis: ( n < N implies (min B) * (f . n) <= t . n )
A8: f . n > 0 by Def3;
assume n < N ; :: thesis: (min B) * (f . n) <= t . n
then (t . n) / (f . n) in B ;
then (t . n) / (f . n) >= min B by XXREAL_2:def 7;
then ((t . n) / (f . n)) * (f . n) >= (min B) * (f . n) by A8, XREAL_1:64;
hence (min B) * (f . n) <= t . n by A8, XCMPLX_1:87; :: thesis: verum

end;

thus ex d being Real st
( d > 0 & ( for n being Element of NAT holds d * (f . n) <= t . n ) ) :: thesis: verum

proof

per cases ( min B <= d or min B > d ) ;

suppose A9: min B <= d ; :: thesis: ex d being Real st
( d > 0 & ( for n being Element of NAT holds d * (f . n) <= t . n ) )

reconsider b = min B as Element of REAL by XREAL_0:def 1;
take b ; :: thesis: ( b > 0 & ( for n being Element of NAT holds b * (f . n) <= t . n ) )
b in B by XXREAL_2:def 7;
then consider n1 being Element of NAT such that
A10: b = (t . n1) / (f . n1) and
n1 < N ;
( t . n1 > 0 & f . n1 > 0 ) by Def3;
then (t . n1) * ((f . n1) ") > 0 * ((f . n1) ") by XREAL_1:68;
hence b > 0 by A10, XCMPLX_0:def 9; :: thesis: for n being Element of NAT holds b * (f . n) <= t . n
let n be Element of NAT ; :: thesis: b * (f . n) <= t . n
thus b * (f . n) <= t . n :: thesis: verum

proof

per cases ( n < N or n >= N ) ;

suppose n < N ; :: thesis: b * (f . n) <= t . n

hence b * (f . n) <= t . n by A7; :: thesis: verum

end;

suppose A11: n >= N ; :: thesis: b * (f . n) <= t . n

f . n > 0 by Def3;
then A12: b * (f . n) <= d * (f . n) by A9, XREAL_1:64;
d * (f . n) <= t . n by A1, A4, A11;
hence b * (f . n) <= t . n by A12, XXREAL_0:2; :: thesis: verum

end;

end;

end;

end;

suppose A13: min B > d ; :: thesis: ex d being Real st
( d > 0 & ( for n being Element of NAT holds d * (f . n) <= t . n ) )

take d ; :: thesis: ( d > 0 & ( for n being Element of NAT holds d * (f . n) <= t . n ) )
thus d > 0 by A3; :: thesis: for n being Element of NAT holds d * (f . n) <= t . n
let n be Element of NAT ; :: thesis: d * (f . n) <= t . n
thus d * (f . n) <= t . n :: thesis: verum

proof

per cases ( n < N or n >= N ) ;

suppose A14: n < N ; :: thesis: d * (f . n) <= t . n

f . n > 0 by Def3;
then A15: d * (f . n) <= (min B) * (f . n) by A13, XREAL_1:64;
(min B) * (f . n) <= t . n by A7, A14;
hence d * (f . n) <= t . n by A15, XXREAL_0:2; :: thesis: verum

end;

suppose n >= N ; :: thesis: d * (f . n) <= t . n

hence d * (f . n) <= t . n by A1, A4; :: thesis: verum

end;

end;

end;

end;

end;

end;

end;

end;

end;

given d being Real such that A16: d > 0 and
A17: for n being Element of NAT holds d * (f . n) <= t . n ; :: thesis: t in Big_Omega f
( t is Element of Funcs (NAT,REAL) & ( for n being Element of NAT st n >= 0 holds
( d * (f . n) <= t . n & t . n >= 0 ) ) ) by A17, Def3, FUNCT_2:8;
hence t in Big_Omega f by A16; :: thesis: verum