set g = seq_n^ 2;
consider t1 being Element of NAT such that
A1: t1 = (10 * 10) * 10 ;
consider t2 being Element of NAT such that
A2: t2 = t1 * t1 ;
t1 = 10 * (10 ^2) by A1;
then t1 = 10 * (10 to_power 2) by POWER:46;
then t1 = (10 to_power 1) * (10 to_power 2) by POWER:25;
then A3: t1 = 10 to_power (1 + 2) by POWER:27;
then A4: t2 = 10 to_power (3 + 3) by A2, POWER:27
.= 10 to_power 6 ;
A5: 10 to_power 3 = 10 to_power (2 + 1)
.= (10 to_power 2) * (10 to_power 1) by POWER:27
.= (10 to_power 2) * 10 by POWER:25
.= (10 ^2) * 10 by POWER:46
.= 1000 ;
A6: for n being Element of NAT st n >= 400 holds
((18 * t1) * n) - (3 * t2) < 27 * (n ^2)

proof

defpred S₁[ Nat] means ((18 * t1) * $1) - (3 * t2) < 27 * ($1 ^2);
A7: for k being Nat st k >= 400 & S₁[k] holds
S₁[k + 1]

proof

let k be Nat; :: thesis: ( k >= 400 & S₁[k] implies S₁[k + 1] )
assume that
A8: k >= 400 and
A9: ((18 * t1) * k) - (3 * t2) < 27 * (k ^2) ; :: thesis: S₁[k + 1]
54 * 400 <= 54 * k by A8, XREAL_1:64;
then A10: 18 * t1 < 54 * k by A3, A5, XXREAL_0:2;
(54 * k) + 0 <= (54 * k) + 27 by XREAL_1:7;
then 18 * t1 < (54 * k) + 27 by A10, XXREAL_0:2;
then A11: (27 * (k ^2)) + (18 * t1) < (27 * (k ^2)) + ((54 * k) + 27) by XREAL_1:6;
((18 * t1) * (k + 1)) - (3 * t2) = (((18 * t1) * k) - (3 * t2)) + (18 * t1) ;
then ((18 * t1) * (k + 1)) - (3 * t2) < (27 * (k ^2)) + (18 * t1) by A9, XREAL_1:6;
hence S₁[k + 1] by A11, XXREAL_0:2; :: thesis: verum

end;

A12: S₁[400] by A2, A3, A5;
for n being Nat st n >= 400 holds
S₁[n] from NAT_1:sch 8(A12, A7);
hence for n being Element of NAT st n >= 400 holds
((18 * t1) * n) - (3 * t2) < 27 * (n ^2) ; :: thesis: verum

end;

let f be Real_Sequence; :: thesis: ( ( for n being Element of NAT holds f . n = ((3 * (10 to_power 6)) - ((18 * (10 to_power 3)) * n)) + (27 * (n ^2)) ) implies f in Big_Oh (seq_n^ 2) )
assume A13: for n being Element of NAT holds f . n = ((3 * (10 to_power 6)) - ((18 * (10 to_power 3)) * n)) + (27 * (n ^2)) ; :: thesis: f in Big_Oh (seq_n^ 2)
A14: for n being Element of NAT st n >= 400 holds
f . n <= 27 * (n ^2)

proof

let n be Element of NAT ; :: thesis: ( n >= 400 implies f . n <= 27 * (n ^2) )
assume A15: n >= 400 ; :: thesis: f . n <= 27 * (n ^2)

now :: thesis: not f . n > 27 * (n ^2)

assume f . n > 27 * (n ^2) ; :: thesis: contradiction
then ((3 * t2) - ((18 * (10 to_power 3)) * n)) + (27 * (n ^2)) > 27 * (n ^2) by A13, A4;
then (3 * t2) + (- ((18 * t1) * n)) > (27 * (n ^2)) - (27 * (n ^2)) by A3, XREAL_1:19;
then (3 * t2) - ((18 * t1) * n) > 0 ;
then A16: 3 * t2 > 0 + ((18 * t1) * n) by XREAL_1:20;
(18 * t1) * n >= (18 * t1) * 400 by A15, XREAL_1:64;
then 3 * (10 to_power (3 + 3)) > t1 * 7200 by A4, A16, XXREAL_0:2;
then 3 * ((10 to_power 3) * (10 to_power 3)) > t1 * 7200 by POWER:27;
hence contradiction by A3, A5; :: thesis: verum

end;

hence f . n <= 27 * (n ^2) ; :: thesis: verum

end;

A17: now :: thesis: for n being Element of NAT st n >= 400 holds
( f . n <= 27 * ((seq_n^ 2) . n) & f . n >= 0 )

let n be Element of NAT ; :: thesis: ( n >= 400 implies ( f . n <= 27 * ((seq_n^ 2) . n) & f . n >= 0 ) )
assume A18: n >= 400 ; :: thesis: ( f . n <= 27 * ((seq_n^ 2) . n) & f . n >= 0 )
then f . n <= 27 * (n ^2) by A14;
then f . n <= 27 * (n to_power 2) by POWER:46;
hence f . n <= 27 * ((seq_n^ 2) . n) by A18, Def3; :: thesis: f . n >= 0
0 + (((18 * t1) * n) - (3 * t2)) < 27 * (n ^2) by A6, A18;
then 0 < (27 * (n ^2)) - (((18 * t1) * n) - (3 * t2)) by XREAL_1:20;
then 0 < ((3 * (10 to_power 6)) - ((18 * t1) * n)) + (27 * (n ^2)) by A4;
hence f . n >= 0 by A13, A3; :: thesis: verum

end;

f is Element of Funcs (NAT,REAL) by FUNCT_2:8;
hence f in Big_Oh (seq_n^ 2) by A17; :: thesis: verum