let X be non empty set ; for F being Functional_Sequence of X,ExtREAL
for f being PartFunc of X,ExtREAL
for x being Element of X st F is additive & F is with_the_same_dom & dom f c= dom (F . 0) & x in dom f & F # x is summable & f . x = Sum (F # x) holds
f . x = lim ((Partial_Sums F) # x)
let F be Functional_Sequence of X,ExtREAL; for f being PartFunc of X,ExtREAL
for x being Element of X st F is additive & F is with_the_same_dom & dom f c= dom (F . 0) & x in dom f & F # x is summable & f . x = Sum (F # x) holds
f . x = lim ((Partial_Sums F) # x)
let f be PartFunc of X,ExtREAL; for x being Element of X st F is additive & F is with_the_same_dom & dom f c= dom (F . 0) & x in dom f & F # x is summable & f . x = Sum (F # x) holds
f . x = lim ((Partial_Sums F) # x)
let x be Element of X; ( F is additive & F is with_the_same_dom & dom f c= dom (F . 0) & x in dom f & F # x is summable & f . x = Sum (F # x) implies f . x = lim ((Partial_Sums F) # x) )
set PF = Partial_Sums F;
assume that
A1:
F is additive
and
A2:
F is with_the_same_dom
and
A3:
dom f c= dom (F . 0)
and
A4:
x in dom f
and
A5:
F # x is summable
and
A6:
f . x = Sum (F # x)
; f . x = lim ((Partial_Sums F) # x)
set PFx = Partial_Sums (F # x);
Partial_Sums (F # x) is convergent
by A5;
then A7:
(Partial_Sums F) # x is convergent
by A1, A2, A3, A4, Th33;
per cases
( ex g being Real st
( lim ((Partial_Sums F) # x) = g & ( for p being Real st 0 < p holds
ex n being Nat st
for m being Nat st n <= m holds
|.((((Partial_Sums F) # x) . m) - (lim ((Partial_Sums F) # x))).| < p ) & (Partial_Sums F) # x is convergent_to_finite_number ) or ( lim ((Partial_Sums F) # x) = +infty & (Partial_Sums F) # x is convergent_to_+infty ) or ( lim ((Partial_Sums F) # x) = -infty & (Partial_Sums F) # x is convergent_to_-infty ) )
by A7, MESFUNC5:def 12;
suppose A8:
ex
g being
Real st
(
lim ((Partial_Sums F) # x) = g & ( for
p being
Real st
0 < p holds
ex
n being
Nat st
for
m being
Nat st
n <= m holds
|.((((Partial_Sums F) # x) . m) - (lim ((Partial_Sums F) # x))).| < p ) &
(Partial_Sums F) # x is
convergent_to_finite_number )
;
f . x = lim ((Partial_Sums F) # x)then A9:
Partial_Sums (F # x) is
convergent_to_finite_number
by A1, A2, A3, A4, Th33;
then A10:
not
Partial_Sums (F # x) is
convergent_to_+infty
by MESFUNC5:50;
A11:
not
Partial_Sums (F # x) is
convergent_to_-infty
by A9, MESFUNC5:51;
Partial_Sums (F # x) is
convergent
by A9;
then A12:
ex
g being
Real st
(
f . x = g & ( for
p being
Real st
0 < p holds
ex
n being
Nat st
for
m being
Nat st
n <= m holds
|.(((Partial_Sums (F # x)) . m) - (f . x)).| < p ) &
Partial_Sums (F # x) is
convergent_to_finite_number )
by A6, A10, A11, MESFUNC5:def 12;
hence
f . x = lim ((Partial_Sums F) # x)
by A7, A8, A12, MESFUNC5:def 12;
verum end; end;