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
A6:
x in (dom (F . 0 )) /\ (dom (G . 0 ))
and
A5:
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 PF = Partial_Sums F;
set PG = Partial_Sums G;
defpred S1[ Nat] means ((Partial_Sums F) . $1) . x <= ((Partial_Sums G) . $1) . x;
( (Partial_Sums F) . 0 = F . 0 & (Partial_Sums G) . 0 = G . 0 )
by Def0;
then B1:
S1[ 0 ]
by A5, A6;
B2:
for k being Nat st S1[k] holds
S1[k + 1]
proof
let k be
Nat;
:: thesis: ( S1[k] implies S1[k + 1] )
assume B20:
S1[
k]
;
:: thesis: S1[k + 1]
R1:
(F . (k + 1)) . x <= (G . (k + 1)) . x
by A5, A6;
B22:
(
(Partial_Sums F) . (k + 1) = ((Partial_Sums F) . k) + (F . (k + 1)) &
(Partial_Sums G) . (k + 1) = ((Partial_Sums G) . k) + (G . (k + 1)) )
by Def0;
(
dom ((Partial_Sums F) . (k + 1)) = dom (F . 0 ) &
dom ((Partial_Sums G) . (k + 1)) = dom (G . 0 ) )
by A1, A2, A3, A4, ADD0;
then
(
x in dom ((Partial_Sums F) . (k + 1)) &
x in dom ((Partial_Sums G) . (k + 1)) )
by A6, XBOOLE_0:def 4;
then B25:
(
((Partial_Sums F) . (k + 1)) . x = (((Partial_Sums F) . k) . x) + ((F . (k + 1)) . x) &
((Partial_Sums G) . (k + 1)) . x = (((Partial_Sums G) . k) . x) + ((G . (k + 1)) . x) )
by B22, MESFUNC1:def 3;
thus
S1[
k + 1]
by B25, R1, B20, XXREAL_3:38;
:: thesis: verum
end;
for k being Nat holds S1[k]
from NAT_1:sch 2(B1, B2);
hence
((Partial_Sums F) . n) . x <= ((Partial_Sums G) . n) . x
; :: thesis: verum