let f, g be eventually-nonnegative Real_Sequence; :: thesis: ( f in Big_Oh g implies Big_Oh f c= Big_Oh g )
assume f in Big_Oh g ; :: thesis: Big_Oh f c= Big_Oh g
then consider t being Element of Funcs (NAT,REAL) such that
A1: t = f and
A2: 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 * (g . n) & t . n >= 0 ) ) ) ;
consider ct being Real, Nt being Element of NAT such that
ct > 0 and
A3: for n being Element of NAT st n >= Nt holds
( t . n <= ct * (g . n) & t . n >= 0 ) by A2;
consider Ng being Nat such that
A4: for n being Nat st n >= Ng holds
g . n >= 0 by Def2;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in Big_Oh f or x in Big_Oh g )
assume x in Big_Oh f ; :: thesis: x in Big_Oh g
then consider s being Element of Funcs (NAT,REAL) such that
A5: s = x and
A6: ex c being Real ex N being Element of NAT st
( c > 0 & ( for n being Element of NAT st n >= N holds
( s . n <= c * (f . n) & s . n >= 0 ) ) ) ;
consider cs being Real, Ns being Element of NAT such that
A7: cs > 0 and
A8: for n being Element of NAT st n >= Ns holds
( s . n <= cs * (f . n) & s . n >= 0 ) by A6;

now :: thesis: ex c being object st
( c > 0 & ex N being Element of NAT st
for n being Element of NAT st n >= N holds
( s . n <= c * (g . n) & s . n >= 0 ) )

take c = max ((cs * ct),(max (cs,ct))); :: thesis: ( c > 0 & ex N being Element of NAT st
for n being Element of NAT st n >= N holds
( s . n <= c * (g . n) & s . n >= 0 ) )
c >= max (cs,ct) by XXREAL_0:25;
hence c > 0 by A7, XXREAL_0:25; :: thesis: ex N being Element of NAT st
for n being Element of NAT st n >= N holds
( s . n <= c * (g . n) & s . n >= 0 )
reconsider N = max ((max (Ns,Nt)),Ng) as Element of NAT by ORDINAL1:def 12;
take N = N; :: thesis: for n being Element of NAT st n >= N holds
( s . n <= c * (g . n) & s . n >= 0 )
let n be Element of NAT ; :: thesis: ( n >= N implies ( s . n <= c * (g . n) & s . n >= 0 ) )
assume A9: n >= N ; :: thesis: ( s . n <= c * (g . n) & s . n >= 0 )
A10: N >= max (Ns,Nt) by XXREAL_0:25;
max (Ns,Nt) >= Nt by XXREAL_0:25;
then N >= Nt by A10, XXREAL_0:2;
then n >= Nt by A9, XXREAL_0:2;
then t . n <= ct * (g . n) by A3;
then A11: cs * (t . n) <= cs * (ct * (g . n)) by A7, XREAL_1:64;
N >= Ng by XXREAL_0:25;
then n >= Ng by A9, XXREAL_0:2;
then g . n >= 0 by A4;
then (cs * ct) * (g . n) <= c * (g . n) by XREAL_1:64, XXREAL_0:25;
then A12: cs * (t . n) <= c * (g . n) by A11, XXREAL_0:2;
max (Ns,Nt) >= Ns by XXREAL_0:25;
then N >= Ns by A10, XXREAL_0:2;
then A13: n >= Ns by A9, XXREAL_0:2;
then s . n <= cs * (f . n) by A8;
hence s . n <= c * (g . n) by A1, A12, XXREAL_0:2; :: thesis: s . n >= 0
thus s . n >= 0 by A8, A13; :: thesis: verum

end;

hence x in Big_Oh g by A5; :: thesis: verum