set t = seq_n^ (- 1);
reconsider F = {(seq_n^ 1)} as FUNCTION_DOMAIN of NAT , REAL by FUNCT_2:121;
take F ; :: thesis:
thus F = {(seq_n^ 1)} ; :: thesis:

A1: now :: thesis:

let n be Element of NAT ; :: thesis:

suppose A2: n = 0 ; :: thesis:

then (seq_n^ (- 1)) . n = 0 by Def3;
hence (seq_n^ (- 1)) . n <= (seq_n^ 1) . n by A2, Def3; :: thesis:

end;

suppose A3: n > 0 ; :: thesis:

then A4: n >= 0 + 1 by INT_1:7;
A5: n to_power (- 1) <= n to_power 1

per cases by A4, XXREAL_0:1;

suppose A6: n = 1 ; :: thesis:

then n to_power (- 1) = 1 by POWER:26;
hence n to_power (- 1) <= n to_power 1 by A6, POWER:26; :: thesis:

end;

suppose n > 1 ; :: thesis:

hence n to_power (- 1) <= n to_power 1 by PRE_FF:8; :: thesis:

end;

end;

end;

(seq_n^ (- 1)) . n = n to_power (- 1) by A3, Def3;
hence (seq_n^ (- 1)) . n <= (seq_n^ 1) . n by A3, A5, Def3; :: thesis:

end;

end;

end;

assume A7: seq_n^ (- 1) in F to_power (Big_Oh (seq_const 1)) ; :: thesis:
ex H being FUNCTION_DOMAIN of NAT , REAL st
( H = F & ( seq_n^ (- 1) in H to_power (Big_Oh (seq_const 1)) implies ex N being Element of NAT ex c being Real ex k being Element of NAT st
( c > 0 & ( for n being Element of NAT st n >= N holds
( 1 <= (seq_n^ (- 1)) . n & (seq_n^ (- 1)) . n <= c * ((seq_n^ k) . n) ) ) ) ) & ( ex N being Element of NAT ex c being Real ex k being Element of NAT st
( c > 0 & ( for n being Element of NAT st n >= N holds
( 1 <= (seq_n^ (- 1)) . n & (seq_n^ (- 1)) . n <= c * ((seq_n^ k) . n) ) ) ) implies seq_n^ (- 1) in H to_power (Big_Oh (seq_const 1)) ) ) by Th9;
then consider N0 being Element of NAT , c being Real, k being Element of NAT such that
c > 0 and
A8: for n being Element of NAT st n >= N0 holds
( 1 <= (seq_n^ (- 1)) . n & (seq_n^ (- 1)) . n <= c * ((seq_n^ k) . n) ) by A7;
set N = max (N0,2);
A9: max (N0,2) >= 2 by XXREAL_0:25;
A10: max (N0,2) >= N0 by XXREAL_0:25;

let n be Element of NAT ; :: thesis:
assume A11: n >= max (N0,2) ; :: thesis:
then n >= 2 by A9, XXREAL_0:2;
then A12: n > 1 by XXREAL_0:2;
n >= N0 by A10, A11, XXREAL_0:2;
then A13: (seq_n^ (- 1)) . n >= 1 by A8;
(seq_n^ (- 1)) . n = n to_power (- 1) by A9, A11, Def3;
hence contradiction by A13, A12, POWER:36; :: thesis:

end;

hence contradiction ; :: thesis:

end;

hence ( ( for n being Element of NAT holds (seq_n^ (- 1)) . n <= (seq_n^ 1) . n ) & not seq_n^ (- 1) in F to_power (Big_Oh (seq_const 1)) ) by A1; :: thesis: