let f be eventually-nonnegative Real_Sequence; :: thesis: for c being positive Real holds Big_Oh f = Big_Oh (c (#) f)
let c be positive Real; :: thesis: Big_Oh f = Big_Oh (c (#) f)

now :: thesis: for x being object holds
( ( x in Big_Oh f implies x in Big_Oh (c (#) f) ) & ( x in Big_Oh (c (#) f) implies x in Big_Oh f ) )

let x be object ; :: thesis: ( ( x in Big_Oh f implies x in Big_Oh (c (#) f) ) & ( x in Big_Oh (c (#) f) implies x in Big_Oh f ) )

hereby :: thesis: ( x in Big_Oh (c (#) f) implies x in Big_Oh f )

assume x in Big_Oh f ; :: thesis: x in Big_Oh (c (#) f)
then consider t being Element of Funcs (NAT,REAL) such that
A1: x = t 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 * (f . n) & t . n >= 0 ) ) ) ;
consider c1 being Real, N being Element of NAT such that
A3: c1 > 0 and
A4: for n being Element of NAT st n >= N holds
( t . n <= c1 * (f . n) & t . n >= 0 ) by A2;

A5: now :: thesis: for n being Element of NAT st n >= N holds
( t . n <= (c1 * (c ")) * ((c (#) f) . n) & t . n >= 0 )

let n be Element of NAT ; :: thesis: ( n >= N implies ( t . n <= (c1 * (c ")) * ((c (#) f) . n) & t . n >= 0 ) )
assume A6: n >= N ; :: thesis: ( t . n <= (c1 * (c ")) * ((c (#) f) . n) & t . n >= 0 )
then t . n <= (c1 * 1) * (f . n) by A4;
then t . n <= (c1 * ((c ") * c)) * (f . n) by XCMPLX_0:def 7;
then t . n <= (c1 * (c ")) * (c * (f . n)) ;
hence ( t . n <= (c1 * (c ")) * ((c (#) f) . n) & t . n >= 0 ) by A4, A6, SEQ_1:9; :: thesis: verum

end;

c1 * (c ") > 0 * (c ") by A3, XREAL_1:68;
hence x in Big_Oh (c (#) f) by A1, A5; :: thesis: verum

end;

assume x in Big_Oh (c (#) f) ; :: thesis: x in Big_Oh f
then consider t being Element of Funcs (NAT,REAL) such that
A7: x = t and
A8: ex c1 being Real ex N being Element of NAT st
( c1 > 0 & ( for n being Element of NAT st n >= N holds
( t . n <= c1 * ((c (#) f) . n) & t . n >= 0 ) ) ) ;
consider c1 being Real, N being Element of NAT such that
A9: c1 > 0 and
A10: for n being Element of NAT st n >= N holds
( t . n <= c1 * ((c (#) f) . n) & t . n >= 0 ) by A8;

A11: now :: thesis: for n being Element of NAT st n >= N holds
( t . n <= (c1 * c) * (f . n) & t . n >= 0 )

let n be Element of NAT ; :: thesis: ( n >= N implies ( t . n <= (c1 * c) * (f . n) & t . n >= 0 ) )
assume A12: n >= N ; :: thesis: ( t . n <= (c1 * c) * (f . n) & t . n >= 0 )
then t . n <= c1 * ((c (#) f) . n) by A10;
then t . n <= c1 * (c * (f . n)) by SEQ_1:9;
hence ( t . n <= (c1 * c) * (f . n) & t . n >= 0 ) by A10, A12; :: thesis: verum

end;

c1 * c > 0 * c by A9, XREAL_1:68;
hence x in Big_Oh f by A7, A11; :: thesis: verum

end;

hence Big_Oh f = Big_Oh (c (#) f) by TARSKI:2; :: thesis: verum