let f be Real_Sequence; ( f in Big_Oh (seq_n^ 1) implies f (#) f in Big_Oh (seq_n^ 2) )
set h = seq_n^ 2;
set g = seq_n^ 1;
assume
f in Big_Oh (seq_n^ 1)
; f (#) f in Big_Oh (seq_n^ 2)
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 * ((seq_n^ 1) . n) & t . n >= 0 ) ) )
;
consider c being Real, N being Element of NAT such that
A3:
c > 0
and
A4:
for n being Element of NAT st n >= N holds
( t . n <= c * ((seq_n^ 1) . n) & t . n >= 0 )
by A2;
set d = max (c,(c * c));
A5:
0 to_power 1 = 0
by POWER:def 2;
A6:
now ex N being Element of NAT st
for n being Element of NAT st n >= N holds
( (t (#) t) . n <= (max (c,(c * c))) * ((seq_n^ 2) . n) & (t (#) t) . n >= 0 )take N =
N;
for n being Element of NAT st n >= N holds
( (t (#) t) . n <= (max (c,(c * c))) * ((seq_n^ 2) . n) & (t (#) t) . n >= 0 )let n be
Element of
NAT ;
( n >= N implies ( (t (#) t) . n <= (max (c,(c * c))) * ((seq_n^ 2) . n) & (t (#) t) . n >= 0 ) )assume A7:
n >= N
;
( (t (#) t) . n <= (max (c,(c * c))) * ((seq_n^ 2) . n) & (t (#) t) . n >= 0 )then A8:
t . n >= 0
by A4;
for
n being
Element of
NAT holds
(seq_n^ 1) . n <= (seq_n^ 2) . n
then A14:
(seq_n^ 2) . n >= (seq_n^ 1) . n
;
(seq_n^ 1) . n >= 0
then A15:
(c * c) * ((seq_n^ 2) . n) <= (max (c,(c * c))) * ((seq_n^ 2) . n)
by A14, XREAL_1:64, XXREAL_0:25;
A16:
(n to_power 1) * (n to_power 1) = n to_power (1 + 1)
A17:
((seq_n^ 1) . n) * ((seq_n^ 1) . n) = (seq_n^ 2) . n
t . n <= c * ((seq_n^ 1) . n)
by A4, A7;
then
(t . n) * (t . n) <= (c * ((seq_n^ 1) . n)) * (c * ((seq_n^ 1) . n))
by A8, Lm20;
then
(t . n) * (t . n) <= (max (c,(c * c))) * ((seq_n^ 2) . n)
by A17, A15, XXREAL_0:2;
hence
(t (#) t) . n <= (max (c,(c * c))) * ((seq_n^ 2) . n)
by SEQ_1:8;
(t (#) t) . n >= 0
(t . n) * (t . n) >= (t . n) * 0
by A8;
hence
(t (#) t) . n >= 0
by SEQ_1:8;
verum end;
A20:
t (#) t is Element of Funcs (NAT,REAL)
by FUNCT_2:8;
max (c,(c * c)) > 0
by A3, XXREAL_0:25;
hence
f (#) f in Big_Oh (seq_n^ 2)
by A1, A20, A6; verum