let c, d be XFinSequence of REAL ; :: thesis: ( len d = len c & ( for i being Nat st i in dom d holds
d . i = |.(c . i).| ) implies for n being Nat holds (seq_p c) . n <= (seq_p d) . n )
assume AS: ( len d = len c & ( for i being Nat st i in dom d holds
d . i = |.(c . i).| ) ) ; :: thesis: for n being Nat holds (seq_p c) . n <= (seq_p d) . n
let x be Nat; :: thesis: (seq_p c) . x <= (seq_p d) . x
P1: (seq_p c) . x = Sum (c (#) (seq_a^ (x,1,0))) by defseqp;
P2: (seq_p d) . x = Sum (d (#) (seq_a^ (x,1,0))) by defseqp;
dom (d (#) (seq_a^ (x,1,0))) = dom d by LMXFIN1
.= dom (c (#) (seq_a^ (x,1,0))) by LMXFIN1, AS ;
then D1: len (d (#) (seq_a^ (x,1,0))) = len (c (#) (seq_a^ (x,1,0))) ;
for i being Nat st i in dom (c (#) (seq_a^ (x,1,0))) holds
(c (#) (seq_a^ (x,1,0))) . i <= (d (#) (seq_a^ (x,1,0))) . i

proof

let i be Nat; :: thesis: ( i in dom (c (#) (seq_a^ (x,1,0))) implies (c (#) (seq_a^ (x,1,0))) . i <= (d (#) (seq_a^ (x,1,0))) . i )
assume i in dom (c (#) (seq_a^ (x,1,0))) ; :: thesis: (c (#) (seq_a^ (x,1,0))) . i <= (d (#) (seq_a^ (x,1,0))) . i
then P6: i in dom c by LMXFIN1;
then P7: (c (#) (seq_a^ (x,1,0))) . i = (c . i) * (x to_power i) by LMXFIN2;
P8: (d (#) (seq_a^ (x,1,0))) . i = (d . i) * (x to_power i) by P6, AS, LMXFIN2;
d . i = |.(c . i).| by AS, P6;
hence (c (#) (seq_a^ (x,1,0))) . i <= (d (#) (seq_a^ (x,1,0))) . i by XREAL_1:64, P7, P8, ABSVALUE:4; :: thesis: verum

end;

hence (seq_p c) . x <= (seq_p d) . x by D1, AFINSQ_2:57, P1, P2; :: thesis: verum