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)

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]

let k be Nat; :: thesis:
assume that
A8: k >= 400 and
A9: ((18 * t1) * k) - (3 * t2) < 27 * (k ^2) ; :: thesis:
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:

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:

end;

let f be Real_Sequence; :: thesis:
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:
A14: for n being Element of NAT st n >= 400 holds
f . n <= 27 * (n ^2)

assume f . n > 27 * (n ^2) ; :: thesis:
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:

end;

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

end;

let n be Element of NAT ; :: thesis:
assume A18: n >= 400 ; :: thesis:
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:
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:

end;