let X be non empty set ; for F, G being Functional_Sequence of X,ExtREAL
for n being Nat
for x being Element of X st F is additive & F is with_the_same_dom & G is additive & G is with_the_same_dom & x in (dom (F . 0)) /\ (dom (G . 0)) & ( for k being Nat
for y being Element of X st y in (dom (F . 0)) /\ (dom (G . 0)) holds
(F . k) . y <= (G . k) . y ) holds
((Partial_Sums F) . n) . x <= ((Partial_Sums G) . n) . x
let F, G be Functional_Sequence of X,ExtREAL; for n being Nat
for x being Element of X st F is additive & F is with_the_same_dom & G is additive & G is with_the_same_dom & x in (dom (F . 0)) /\ (dom (G . 0)) & ( for k being Nat
for y being Element of X st y in (dom (F . 0)) /\ (dom (G . 0)) holds
(F . k) . y <= (G . k) . y ) holds
((Partial_Sums F) . n) . x <= ((Partial_Sums G) . n) . x
let n be Nat; for x being Element of X st F is additive & F is with_the_same_dom & G is additive & G is with_the_same_dom & x in (dom (F . 0)) /\ (dom (G . 0)) & ( for k being Nat
for y being Element of X st y in (dom (F . 0)) /\ (dom (G . 0)) holds
(F . k) . y <= (G . k) . y ) holds
((Partial_Sums F) . n) . x <= ((Partial_Sums G) . n) . x
let x be Element of X; ( F is additive & F is with_the_same_dom & G is additive & G is with_the_same_dom & x in (dom (F . 0)) /\ (dom (G . 0)) & ( for k being Nat
for y being Element of X st y in (dom (F . 0)) /\ (dom (G . 0)) holds
(F . k) . y <= (G . k) . y ) implies ((Partial_Sums F) . n) . x <= ((Partial_Sums G) . n) . x )
assume that
A1:
F is additive
and
A2:
F is with_the_same_dom
and
A3:
G is additive
and
A4:
G is with_the_same_dom
and
A5:
x in (dom (F . 0)) /\ (dom (G . 0))
and
A6:
for k being Nat
for y being Element of X st y in (dom (F . 0)) /\ (dom (G . 0)) holds
(F . k) . y <= (G . k) . y
; ((Partial_Sums F) . n) . x <= ((Partial_Sums G) . n) . x
set PG = Partial_Sums G;
set PF = Partial_Sums F;
defpred S1[ Nat] means ((Partial_Sums F) . $1) . x <= ((Partial_Sums G) . $1) . x;
A7:
for k being Nat st S1[k] holds
S1[k + 1]
proof
let k be
Nat;
( S1[k] implies S1[k + 1] )
assume A8:
S1[
k]
;
S1[k + 1]
dom ((Partial_Sums F) . (k + 1)) = dom (F . 0)
by A1, A2, Th29;
then A9:
x in dom ((Partial_Sums F) . (k + 1))
by A5, XBOOLE_0:def 4;
dom ((Partial_Sums G) . (k + 1)) = dom (G . 0)
by A3, A4, Th29;
then A10:
x in dom ((Partial_Sums G) . (k + 1))
by A5, XBOOLE_0:def 4;
(Partial_Sums G) . (k + 1) = ((Partial_Sums G) . k) + (G . (k + 1))
by Def4;
then A11:
((Partial_Sums G) . (k + 1)) . x = (((Partial_Sums G) . k) . x) + ((G . (k + 1)) . x)
by A10, MESFUNC1:def 3;
(Partial_Sums F) . (k + 1) = ((Partial_Sums F) . k) + (F . (k + 1))
by Def4;
then A12:
((Partial_Sums F) . (k + 1)) . x = (((Partial_Sums F) . k) . x) + ((F . (k + 1)) . x)
by A9, MESFUNC1:def 3;
(F . (k + 1)) . x <= (G . (k + 1)) . x
by A5, A6;
hence
S1[
k + 1]
by A8, A12, A11, XXREAL_3:36;
verum
end;
A13:
(Partial_Sums G) . 0 = G . 0
by Def4;
(Partial_Sums F) . 0 = F . 0
by Def4;
then A14:
S1[ 0 ]
by A5, A6, A13;
for k being Nat holds S1[k]
from NAT_1:sch 2(A14, A7);
hence
((Partial_Sums F) . n) . x <= ((Partial_Sums G) . n) . x
; verum