let k be Nat; :: thesis: for d being XFinSequence of REAL

for a being Real

for y being Real_Sequence st 0 < a & len d = k & ( for x being Nat holds y . x = a * (x to_power k) ) holds

ex N being Nat st

for x being Nat st N <= x holds

|.((seq_p d) . x).| <= y . x

let d be XFinSequence of REAL ; :: thesis: for a being Real

for y being Real_Sequence st 0 < a & len d = k & ( for x being Nat holds y . x = a * (x to_power k) ) holds

ex N being Nat st

for x being Nat st N <= x holds

|.((seq_p d) . x).| <= y . x

let a be Real; :: thesis: for y being Real_Sequence st 0 < a & len d = k & ( for x being Nat holds y . x = a * (x to_power k) ) holds

ex N being Nat st

for x being Nat st N <= x holds

|.((seq_p d) . x).| <= y . x

let y be Real_Sequence; :: thesis: ( 0 < a & len d = k & ( for x being Nat holds y . x = a * (x to_power k) ) implies ex N being Nat st

for x being Nat st N <= x holds

|.((seq_p d) . x).| <= y . x )

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: ex N being Nat st

for x being Nat st N <= x holds

|.((seq_p d) . x).| <= y . x

for a being Real

for y being Real_Sequence st 0 < a & len d = k & ( for x being Nat holds y . x = a * (x to_power k) ) holds

ex N being Nat st

for x being Nat st N <= x holds

|.((seq_p d) . x).| <= y . x

let d be XFinSequence of REAL ; :: thesis: for a being Real

for y being Real_Sequence st 0 < a & len d = k & ( for x being Nat holds y . x = a * (x to_power k) ) holds

ex N being Nat st

for x being Nat st N <= x holds

|.((seq_p d) . x).| <= y . x

let a be Real; :: thesis: for y being Real_Sequence st 0 < a & len d = k & ( for x being Nat holds y . x = a * (x to_power k) ) holds

ex N being Nat st

for x being Nat st N <= x holds

|.((seq_p d) . x).| <= y . x

let y be Real_Sequence; :: thesis: ( 0 < a & len d = k & ( for x being Nat holds y . x = a * (x to_power k) ) implies ex N being Nat st

for x being Nat st N <= x holds

|.((seq_p d) . x).| <= y . x )

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: ex N being Nat st

for x being Nat st N <= x holds

|.((seq_p d) . x).| <= y . x

per cases
( k = 0 or k <> 0 )
;

end;

suppose K1:
k = 0
; :: thesis: ex N being Nat st

for x being Nat st N <= x holds

|.((seq_p d) . x).| <= y . x

for x being Nat st N <= x holds

|.((seq_p d) . x).| <= y . x

set N = 0 ;

take 0 ; :: thesis: for x being Nat st 0 <= x holds

|.((seq_p d) . x).| <= y . x

thus for x being Nat st 0 <= x holds

|.((seq_p d) . x).| <= y . x :: thesis: verum

end;take 0 ; :: thesis: for x being Nat st 0 <= x holds

|.((seq_p d) . x).| <= y . x

thus for x being Nat st 0 <= x holds

|.((seq_p d) . x).| <= y . x :: thesis: verum

suppose B4:
k <> 0
; :: thesis: ex N being Nat st

for x being Nat st N <= x holds

|.((seq_p d) . x).| <= y . x

for x being Nat st N <= x holds

|.((seq_p d) . x).| <= y . x

rng |.d.| c= REAL
;

then reconsider c = |.d.| as XFinSequence of REAL by RELAT_1:def 19;

B3: for i being Nat st i in dom c holds

0 <= c . i

0 <= r

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: for x being Nat st N <= x holds

|.((seq_p d) . x).| <= y . x

thus for x being Nat st N <= x holds

|.((seq_p d) . x).| <= y . x :: thesis: verum

end;then reconsider c = |.d.| as XFinSequence of REAL by RELAT_1:def 19;

B3: for i being Nat st i in dom c holds

0 <= c . i

proof

for r being Real st r in rng c holds
let i be Nat; :: thesis: ( i in dom c implies 0 <= c . i )

assume i in dom c ; :: thesis: 0 <= c . i

then c . i = |.(d . i).| by VALUED_1:def 11;

hence 0 <= c . i by COMPLEX1:46; :: thesis: verum

end;assume i in dom c ; :: thesis: 0 <= c . i

then c . i = |.(d . i).| by VALUED_1:def 11;

hence 0 <= c . i by COMPLEX1:46; :: thesis: verum

0 <= r

proof

then B3T:
c is nonnegative-yielding
;
let r be Real; :: thesis: ( r in rng c implies 0 <= r )

assume r in rng c ; :: thesis: 0 <= r

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: verum

end;assume r in rng c ; :: thesis: 0 <= r

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: verum

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: for x being Nat st N <= x holds

|.((seq_p d) . x).| <= y . x

thus for x being Nat st N <= x holds

|.((seq_p d) . x).| <= y . x :: thesis: verum

proof

let x be Nat; :: thesis: ( N <= x implies |.((seq_p d) . x).| <= y . x )

assume A0: N <= x ; :: thesis: |.((seq_p d) . x).| <= y . x

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

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: verum

end;assume A0: N <= x ; :: thesis: |.((seq_p d) . x).| <= y . x

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

then
Sum (c (#) (seq_a^ (x,1,0))) <= ((y . x) / k) * (len (c (#) (seq_a^ (x,1,0))))
by AFINSQ_2:59;
let i be Nat; :: thesis: ( i in dom (c (#) (seq_a^ (x,1,0))) implies (c (#) (seq_a^ (x,1,0))) . i <= (y . x) / k )

assume i in dom (c (#) (seq_a^ (x,1,0))) ; :: thesis: (c (#) (seq_a^ (x,1,0))) . i <= (y . x) / k

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: verum

end;assume i in dom (c (#) (seq_a^ (x,1,0))) ; :: thesis: (c (#) (seq_a^ (x,1,0))) . i <= (y . x) / k

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: verum

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: verum