let X be non empty set ; :: thesis: 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; :: thesis: 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; :: thesis: 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; :: thesis: ( 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) ; :: thesis: 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 ) ; :: thesis: 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;
now :: thesis: 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
let p be Real; :: thesis: ( 0 < p implies ex n being Nat st
for m being Nat st n <= m holds
|.((((Partial_Sums F) # x) . m) - (f . x)).| < p )
assume 0 < p ; :: thesis: ex n being Nat st
for m being Nat st n <= m holds
|.((((Partial_Sums F) # x) . m) - (f . x)).| < p
then consider n being Nat such that
A13: for m being Nat st n <= m holds
|.(((Partial_Sums (F # x)) . m) - (f . x)).| < p by A12;
take n = n; :: thesis: for m being Nat st n <= m holds
|.((((Partial_Sums F) # x) . m) - (f . x)).| < p
let m be Nat; :: thesis: ( n <= m implies |.((((Partial_Sums F) # x) . m) - (f . x)).| < p )
assume A14: n <= m ; :: thesis: |.((((Partial_Sums F) # x) . m) - (f . x)).| < p
(Partial_Sums (F # x)) . m = ((Partial_Sums F) # x) . m by A1, A2, A3, A4, Th32;
hence |.((((Partial_Sums F) # x) . m) - (f . x)).| < p by A13, A14; :: thesis: verum
end;
hence f . x = lim ((Partial_Sums F) # x) by A7, A8, A12, MESFUNC5:def 12; :: thesis: verum
end;
suppose A15: ( lim ((Partial_Sums F) # x) = +infty & (Partial_Sums F) # x is convergent_to_+infty ) ; :: thesis: f . x = lim ((Partial_Sums F) # x)
then A16: Partial_Sums (F # x) is convergent_to_+infty by A1, A2, A3, A4, Th33;
then Partial_Sums (F # x) is convergent ;
hence f . x = lim ((Partial_Sums F) # x) by A6, A15, A16, MESFUNC5:def 12; :: thesis: verum
end;
suppose A17: ( lim ((Partial_Sums F) # x) = -infty & (Partial_Sums F) # x is convergent_to_-infty ) ; :: thesis: f . x = lim ((Partial_Sums F) # x)
then A18: Partial_Sums (F # x) is convergent_to_-infty by A1, A2, A3, A4, Th33;
then Partial_Sums (F # x) is convergent ;
hence f . x = lim ((Partial_Sums F) # x) by A6, A17, A18, MESFUNC5:def 12; :: thesis: verum
end;
end;