let X be non empty set ; :: thesis: 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; :: thesis: 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; :: thesis: 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; :: thesis: ( 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 ; :: thesis: ((Partial_Sums F) . n) . x <= ((Partial_Sums G) . n) . x
set PG = Partial_Sums G;
set PF = Partial_Sums F;
defpred S₁[ Nat] means ((Partial_Sums F) . $1) . x <= ((Partial_Sums G) . $1) . x;
A7: for k being Nat st S₁[k] holds
S₁[k + 1]

proof

let k be Nat; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume A8: S₁[k] ; :: thesis: S₁[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 S₁[k + 1] by A8, A12, A11, XXREAL_3:36; :: thesis: verum

end;

A13: (Partial_Sums G) . 0 = G . 0 by Def4;
(Partial_Sums F) . 0 = F . 0 by Def4;
then A14: S₁[ 0 ] by A5, A6, A13;
for k being Nat holds S₁[k] from NAT_1:sch 2(A14, A7);
hence ((Partial_Sums F) . n) . x <= ((Partial_Sums G) . n) . x ; :: thesis: verum