theorem :: ASYMPT_1:15

for f being Real_Sequence st f in Big_Oh (seq_n^ 1) holds
f (#) f in Big_Oh (seq_n^ 2)