let d be XFinSequence of REAL ; :: thesis: for k being Nat st len d = 1 & d is nonnegative-yielding holds
seq_p d in Big_Oh ()

let k be Nat; :: thesis: ( len d = 1 & d is nonnegative-yielding implies seq_p d in Big_Oh () )
assume AS: ( len d = 1 & d is nonnegative-yielding ) ; :: thesis: seq_p d in Big_Oh ()
then consider a being Real such that
P1: ( a = d . 0 & ( for x being Nat holds () . x = a ) ) by LMXFIN5;
set y = seq_p d;
set c = a + 1;
XA1: a + 0 < a + 1 by XREAL_1:8;
0 in Segm 1 by NAT_1:44;
then ASX: 0 <= d . 0 by ;
A1: now :: thesis: for n being Element of NAT st n >= 2 holds
( () . n <= (a + 1) * (() . n) & () . n >= 0 )
let n be Element of NAT ; :: thesis: ( n >= 2 implies ( () . n <= (a + 1) * (() . n) & () . n >= 0 ) )
assume A2: n >= 2 ; :: thesis: ( () . n <= (a + 1) * (() . n) & () . n >= 0 )
then A3: n > 1 by XXREAL_0:2;
A4: (seq_n^ k) . n = n to_power k by ;
1 <= () . n
proof
per cases ( k = 0 or 0 < k ) ;
suppose k = 0 ; :: thesis: 1 <= () . n
hence 1 <= () . n by ; :: thesis: verum
end;
suppose 0 < k ; :: thesis: 1 <= () . n
hence 1 <= () . n by ; :: thesis: verum
end;
end;
end;
then 1 * a <= (() . n) * (a + 1) by ;
hence (seq_p d) . n <= (a + 1) * (() . n) by P1; :: thesis: () . n >= 0
thus (seq_p d) . n >= 0 by ; :: thesis: verum
end;
seq_p d is Element of Funcs (NAT,REAL) by FUNCT_2:8;
hence seq_p d in Big_Oh () by A1, P1, ASX; :: thesis: verum