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:53;
then t1 = (10 to_power 1) * (10 to_power 2) by POWER:30;
then A3: t1 = 10 to_power (1 + 2) by POWER:32;
then A4: t2 = 10 to_power (3 + 3) by A2, POWER:32
.= 10 to_power 6 ;
A5: 10 to_power 3 = 10 to_power (2 + 1)
.= (10 to_power 2) * (10 to_power 1) by POWER:32
.= (10 to_power 2) * 10 by POWER:30
.= (10 ^2 ) * 10 by POWER:53
.= 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:66;
then A10: 18 * t1 < 54 * k by A3, A5, XXREAL_0:2;
(54 * k) + 0 <= (54 * k) + 27 by XREAL_1:9;
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:8;
((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:8;
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

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:21;
then (3 * t2) - ((18 * t1) * n) > 0 ;
then A16: 3 * t2 > 0 + ((18 * t1) * n) by XREAL_1:22;
(18 * t1) * n >= (18 * t1) * 400 by A15, XREAL_1:66;
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:32;
hence contradiction by A3, A5; :: thesis: verum

end;

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

end;

A17: now

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:53;
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:22;
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:11;
hence f in Big_Oh (seq_n^ 2) by A17; :: thesis: verum