set f = seq_n^ 2;
set g = seq_n^ 3;
A1: seq_n^ 2 is Element of Funcs NAT ,REAL by FUNCT_2:11;

now

let n be Element of NAT ; :: thesis: ( n >= 2 implies ( (seq_n^ 2) . n <= 1 * ((seq_n^ 3) . n) & (seq_n^ 2) . n >= 0 ) )
assume A2: n >= 2 ; :: thesis: ( (seq_n^ 2) . n <= 1 * ((seq_n^ 3) . n) & (seq_n^ 2) . n >= 0 )
then A3: n > 1 by XXREAL_0:2;
A4: (seq_n^ 2) . n = n to_power 2 by A2, Def3;
(seq_n^ 3) . n = n to_power 3 by A2, Def3;
hence (seq_n^ 2) . n <= 1 * ((seq_n^ 3) . n) by A3, A4, POWER:44; :: thesis: (seq_n^ 2) . n >= 0
thus (seq_n^ 2) . n >= 0 by A4; :: thesis: verum

end;

hence seq_n^ 2 in Big_Oh (seq_n^ 3) by A1; :: thesis: verum