let k be Nat; :: thesis:
let d be XFinSequence of REAL ; :: thesis:
let a be Real; :: thesis:
let y be Real_Sequence; :: thesis:
assume that
A1: 0 < a and
A2: len d = k and
A3: for x being Nat holds y . x = a * (x to_power k) ; :: thesis:

per cases ;

suppose K1: k = 0 ; :: thesis:

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

proof

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;

suppose B4: k <> 0 ; :: thesis:

reconsider c = |.d.| as XFinSequence of REAL ;
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, TLNEG36;
take N ; :: thesis:
thus for x being Nat st N <= x holds
|.((seq_p d) . x).| <= y . x :: thesis:

proof

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

proof

let i be Nat; :: thesis:
assume i in dom (c (#) (seq_a^ (x,1,0))) ; :: thesis:
then X5: i in dom c by LMXFIN1;
then (((c . i) * (x to_power i)) * k) / k <= (a * (x to_power k)) / k by XREAL_1:72, A0, A4;
then (c . i) * (x to_power i) <= (a * (x to_power k)) / k by B4, XCMPLX_1:89;
then (c . i) * (x to_power i) <= (y . x) / k by A3;
hence (c (#) (seq_a^ (x,1,0))) . i <= (y . x) / k by X5, LMXFIN2; :: thesis:

end;

then Sum (c (#) (seq_a^ (x,1,0))) <= ((y . x) / k) * (len (c (#) (seq_a^ (x,1,0)))) by AFINSQ_2:59;
then P6: (seq_p c) . x <= y . x by P1, NN0, A2, B4, XCMPLX_1:87;
|.((seq_p d) . x).| <= (seq_p c) . x by TLNEG41;
hence |.((seq_p d) . x).| <= y . x by XXREAL_0:2, P6; :: thesis:

end;

end;

end;