take 2 ; :: according to ASYMPT_0:def 4 :: thesis: for b₁ being Element of NAT holds
( not 2 <= b₁ or not ((seq_n^ 1) - (seq_const 1)) . b₁ <= 0 )
set g = seq_const 1;
set f = seq_n^ 1;
let n be Element of NAT ; :: thesis: ( not 2 <= n or not ((seq_n^ 1) - (seq_const 1)) . n <= 0 )
A1: (seq_const 1) . n = 1 by FUNCOP_1:7;
assume A2: n >= 2 ; :: thesis: not ((seq_n^ 1) - (seq_const 1)) . n <= 0
then A3: n > 1 + 0 by XXREAL_0:2;
A4: (seq_n^ 1) . n = n to_power 1 by A2, Def3
.= n by POWER:25 ;
((seq_n^ 1) - (seq_const 1)) . n = ((seq_n^ 1) . n) + ((- (seq_const 1)) . n) by SEQ_1:7
.= n + (- 1) by A4, A1, SEQ_1:10
.= n - 1 ;
hence not ((seq_n^ 1) - (seq_const 1)) . n <= 0 by A3, XREAL_1:20; :: thesis: verum