let c, d be XFinSequence of REAL ; ( 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).| ) )
; for n being Nat holds (seq_p c) . n <= (seq_p d) . n
let x be Nat; (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;
( 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)))
;
(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;
verum
end;
hence
(seq_p c) . x <= (seq_p d) . x
by D1, AFINSQ_2:57, P1, P2; verum