set t = seq_n^ (- 1);
reconsider F = {(seq_n^ 1)} as FUNCTION_DOMAIN of NAT , REAL by FUNCT_2:121;
take F ; :: thesis: ( F = {(seq_n^ 1)} & ( 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)) )
thus F = {(seq_n^ 1)} ; :: thesis: ( ( 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)) )

A1: now :: thesis: for n being Element of NAT holds (seq_n^ (- 1)) . n <= (seq_n^ 1) . n

let n be Element of NAT ; :: thesis: (seq_n^ (- 1)) . b₁ <= (seq_n^ 1) . b₁

per cases ( n = 0 or n > 0 ) ;

suppose A2: n = 0 ; :: thesis: (seq_n^ (- 1)) . b₁ <= (seq_n^ 1) . b₁

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

end;

suppose A3: n > 0 ; :: thesis: (seq_n^ (- 1)) . b₁ <= (seq_n^ 1) . b₁

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

proof

per cases ( n = 1 or n > 1 ) by A4, XXREAL_0:1;

suppose A6: n = 1 ; :: thesis: n to_power (- 1) <= n to_power 1

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

end;

suppose n > 1 ; :: thesis: n to_power (- 1) <= n to_power 1

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

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: verum

end;

end;

end;

now :: thesis: not seq_n^ (- 1) in F to_power (Big_Oh (seq_const 1))

assume A7: seq_n^ (- 1) in F to_power (Big_Oh (seq_const 1)) ; :: thesis: contradiction
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;

now :: thesis: for n being Element of NAT holds not n >= max (N0,2)

let n be Element of NAT ; :: thesis: not n >= max (N0,2)
assume A11: n >= max (N0,2) ; :: thesis: contradiction
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: verum

end;

hence contradiction ; :: thesis: verum

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: verum