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

now

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 ) )
A11: ( cs <= max cs,ct & ct <= max cs,ct & c >= max cs,ct ) by XXREAL_0:25;
then A12: ( c >= cs & c >= ct & c >= cs * ct ) by XXREAL_0:2, XXREAL_0:25;
thus c > 0 by A7, A11; :: 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 )
take N = max (max Ns,Nt),Ng; :: 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 A13: n >= N ; :: thesis: ( s . n <= c * (g . n) & s . n >= 0 )
( N >= max Ns,Nt & max Ns,Nt >= Ns & max Ns,Nt >= Nt ) by XXREAL_0:25;
then ( N >= Ns & N >= Nt & N >= Ng ) by XXREAL_0:2, XXREAL_0:25;
then A14: ( n >= Ns & n >= Nt & n >= Ng ) by A13, XXREAL_0:2;
then t . n <= ct * (g . n) by A9;
then A15: cs * (t . n) <= cs * (ct * (g . n)) by A7, XREAL_1:66;
g . n >= 0 by A10, A14;
then (cs * ct) * (g . n) <= c * (g . n) by A12, XREAL_1:66;
then A16: cs * (t . n) <= c * (g . n) by A15, XXREAL_0:2;
s . n <= cs * (f . n) by A8, A14;
hence s . n <= c * (g . n) by A5, A16, XXREAL_0:2; :: thesis: s . n >= 0
thus s . n >= 0 by A8, A14; :: thesis: verum

end;

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