set N = 0 ;
take 0 ; :: thesis:
thus for x being Nat st 0 <= x holds
|.((seq_p d) . x).| <= y . x :: thesis:

let x be Nat; :: thesis:
assume 0 <= x ; :: thesis:
D2: |.((seq_p d) . x).| = 0 by COMPLEX1:44, A2, K1, TLNEG1;
y . x = a * (x to_power k) by A3;
hence |.((seq_p d) . x).| <= y . x by D2, A1; :: thesis:

end;

end;

let r be Real; :: thesis:
assume r in rng c ; :: thesis:
then consider x being object such that
RC: ( x in dom c & r = c . x ) by FUNCT_1:def 3;
thus 0 <= r by RC, B3; :: thesis:

end;

then B3T: c is nonnegative-yielding ;
len c = k by A2, VALUED_1:def 11;
then consider N being Nat such that
A4: for x being Nat st N <= x holds
for i being Nat st i in dom c holds
((c . i) * (x to_power i)) * k <= a * (x to_power k) by A1, B3T, TLNEG36;
take N ; :: thesis:
thus for x being Nat st N <= x holds
|.((seq_p d) . x).| <= y . x :: thesis:

let x be Nat; :: thesis:
assume A0: N <= x ; :: thesis:
NN0: dom (c (#) (seq_a^ (x,1,0))) = dom c by LMXFIN1
.= dom d by VALUED_1:def 11 ;
P1: (seq_p c) . x = Sum (c (#) (seq_a^ (x,1,0))) by defseqp;
for i being Nat st i in dom (c (#) (seq_a^ (x,1,0))) holds
(c (#) (seq_a^ (x,1,0))) . i <= (y . x) / k

end;

end;