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
A0: F is additive and
A1: F is with_the_same_dom and
A3: dom f c= dom (F . 0 ) and
A2: x in dom f and
A4: F # x is summable and
A5: 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 A4, Def2;
then A6: (Partial_Sums F) # x is convergent by A0, A1, A2, A3, Cor01;

per cases ( ex g being real number st
( lim ((Partial_Sums F) # x) = g & ( for p being real number 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 A6, MESFUNC5:def 12;

suppose D1: ex g being real number st
( lim ((Partial_Sums F) # x) = g & ( for p being real number 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 Partial_Sums (F # x) is convergent_to_finite_number by A0, A1, A2, A3, Cor01;
then ( Partial_Sums (F # x) is convergent & not Partial_Sums (F # x) is convergent_to_+infty & not Partial_Sums (F # x) is convergent_to_-infty ) by MESFUNC5:56, MESFUNC5:57, MESFUNC5:def 11;
then D4: ex g being real number st
( f . x = g & ( for p being real number 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 A5, MESFUNC5:def 12;

now

let p be real number ; :: 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
D5: for m being Nat st n <= m holds
|.(((Partial_Sums (F # x)) . m) - (f . x)).| < p by D4;
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 D6: n <= m ; :: thesis: |.((((Partial_Sums F) # x) . m) - (f . x)).| < p
(Partial_Sums (F # x)) . m = ((Partial_Sums F) # x) . m by A0, A1, A2, A3, Cor00;
hence |.((((Partial_Sums F) # x) . m) - (f . x)).| < p by D5, D6; :: thesis: verum

end;

hence f . x = lim ((Partial_Sums F) # x) by A6, D1, D4, MESFUNC5:def 12; :: thesis: verum

end;

suppose E0: ( lim ((Partial_Sums F) # x) = +infty & (Partial_Sums F) # x is convergent_to_+infty ) ; :: thesis: f . x = lim ((Partial_Sums F) # x)

then E1: Partial_Sums (F # x) is convergent_to_+infty by A0, A1, A2, A3, Cor01;
then ( Partial_Sums (F # x) is convergent & not Partial_Sums (F # x) is convergent_to_finite_number & not Partial_Sums (F # x) is convergent_to_-infty ) by MESFUNC5:56, MESFUNC5:def 11;
hence f . x = lim ((Partial_Sums F) # x) by E0, E1, A5, MESFUNC5:def 12; :: thesis: verum

end;

suppose F0: ( lim ((Partial_Sums F) # x) = -infty & (Partial_Sums F) # x is convergent_to_-infty ) ; :: thesis: f . x = lim ((Partial_Sums F) # x)

then F1: Partial_Sums (F # x) is convergent_to_-infty by A0, A1, A2, A3, Cor01;
then ( Partial_Sums (F # x) is convergent & not Partial_Sums (F # x) is convergent_to_finite_number & not Partial_Sums (F # x) is convergent_to_+infty ) by MESFUNC5:57, MESFUNC5:def 11;
hence f . x = lim ((Partial_Sums F) # x) by F0, F1, A5, MESFUNC5:def 12; :: thesis: verum

end;

end;