reconsider F = {(seq_n^ 1)} as FUNCTION_DOMAIN of NAT , REAL by FUNCT_2:198;
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

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

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

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

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

end;

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

then A3: ( (seq_n^ (- 1)) . n = n to_power (- 1) & (seq_n^ 1) . n = n to_power 1 ) by Def3;
A4: n >= 0 + 1 by A2, INT_1:20;
n to_power (- 1) <= n to_power 1

proof

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

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

then ( n to_power (- 1) = 1 & n to_power 1 = 1 ) by POWER:31;
hence n to_power (- 1) <= n to_power 1 ; :: 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:10; :: thesis: verum

end;

end;

end;

hence (seq_n^ (- 1)) . n <= (seq_n^ 1) . n by A3; :: thesis: verum

end;

end;

end;

set t = seq_n^ (- 1);

now

assume A5: seq_n^ (- 1) in F to_power (Big_Oh (seq_const 1)) ; :: thesis: contradiction
consider H being FUNCTION_DOMAIN of NAT , REAL such that
A6: H = F and
A7: ( seq_n^ (- 1) in H to_power (Big_Oh (seq_const 1)) iff 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) ) ) ) ) by Th9;
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 A5, A6, A7;
set N = max N0,2;
A9: ( max N0,2 >= N0 & max N0,2 >= 2 ) by XXREAL_0:25;

now

let n be Element of NAT ; :: thesis: not n >= max N0,2
assume A10: n >= max N0,2 ; :: thesis: contradiction
then A11: ( n >= N0 & n >= 2 ) by A9, XXREAL_0:2;
then A12: (seq_n^ (- 1)) . n >= 1 by A8;
A13: n > 1 by A11, XXREAL_0:2;
(seq_n^ (- 1)) . n = n to_power (- 1) by A9, A10, Def3;
hence contradiction by A12, A13, POWER:41; :: 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