take 2 ; :: according to ASYMPT_0:def 4 :: thesis: for b₁ being set 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 Nat; :: thesis: ( not 2 <= n or not ((seq_n^ 1) - (seq_const 1)) . n <= 0 )
A1: n in NAT by ORDINAL1:def 12;
A2: (seq_const 1) . n = 1 by FUNCOP_1:7, A1;
assume A3: n >= 2 ; :: thesis: not ((seq_n^ 1) - (seq_const 1)) . n <= 0
then A4: n > 1 + 0 by XXREAL_0:2;
A5: (seq_n^ 1) . n = n to_power 1 by A3, Def3, A1
.= 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 A5, A2, SEQ_1:10
.= n - 1 ;
hence not ((seq_n^ 1) - (seq_const 1)) . n <= 0 by A4, XREAL_1:20; :: thesis: verum