let c be XFinSequence of REAL ; :: thesis: ex absc being XFinSequence of REAL st
( absc = |.c.| & ( for n being Nat holds (seq_p c) . n <= (seq_p absc) . n ) )
reconsider absc = |.c.| as XFinSequence of REAL ;
take absc ; :: thesis: ( absc = |.c.| & ( for n being Nat holds (seq_p c) . n <= (seq_p absc) . n ) )
thus absc = |.c.| ; :: thesis: for n being Nat holds (seq_p c) . n <= (seq_p absc) . n
let n be Nat; :: thesis: (seq_p c) . n <= (seq_p absc) . n
CL1: (seq_p c) . n = Sum (c (#) (seq_a^ (n,1,0))) by defseqp;
CL2: (seq_p absc) . n = Sum (absc (#) (seq_a^ (n,1,0))) by defseqp;
set mc = c (#) (seq_a^ (n,1,0));
set mac = absc (#) (seq_a^ (n,1,0));
px0: dom c = dom absc by VALUED_1:def 11;
dom (c (#) (seq_a^ (n,1,0))) = (dom c) /\ (dom (seq_a^ (n,1,0))) by VALUED_1:def 4;
then px: len (c (#) (seq_a^ (n,1,0))) = len (absc (#) (seq_a^ (n,1,0))) by px0, VALUED_1:def 4;
for x being Nat st x in dom (c (#) (seq_a^ (n,1,0))) holds
(c (#) (seq_a^ (n,1,0))) . x <= (absc (#) (seq_a^ (n,1,0))) . x

proof

let x be Nat; :: thesis: ( x in dom (c (#) (seq_a^ (n,1,0))) implies (c (#) (seq_a^ (n,1,0))) . x <= (absc (#) (seq_a^ (n,1,0))) . x )
CCL1: (c (#) (seq_a^ (n,1,0))) . x = (c . x) * ((seq_a^ (n,1,0)) . x) by VALUED_1:5;
CCL2: (absc (#) (seq_a^ (n,1,0))) . x = (absc . x) * ((seq_a^ (n,1,0)) . x) by VALUED_1:5;
PX2: (seq_a^ (n,1,0)) . x = n to_power ((1 * x) + 0) by ASYMPT_1:def 1
.= n to_power x ;
absc . x = |.(c . x).| by VALUED_1:18;
hence ( x in dom (c (#) (seq_a^ (n,1,0))) implies (c (#) (seq_a^ (n,1,0))) . x <= (absc (#) (seq_a^ (n,1,0))) . x ) by XREAL_1:64, CCL1, CCL2, ABSVALUE:4, PX2; :: thesis: verum

end;

hence (seq_p c) . n <= (seq_p absc) . n by CL1, CL2, AFINSQ_2:57, px; :: thesis: verum