let X be non empty set ; :: thesis:
let F be Functional_Sequence of X,ExtREAL; :: thesis:
let x be Element of X; :: thesis:
let D be set ; :: thesis:
set PFx = 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: D c= dom (F . 0) and
A4: x in D ; :: thesis:

hereby :: thesis:

assume Partial_Sums (F # x) is convergent_to_finite_number ; :: thesis:
then consider g being Real such that
A6: 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) - g).| < p ;

now :: thesis:

let p be Real; :: thesis:
assume 0 < p ; :: thesis:
then consider n being Nat such that
A7: for m being Nat st n <= m holds
|.(((Partial_Sums (F # x)) . m) - g).| < p by A6;
take n = n; :: thesis:
let m be Nat; :: thesis:
assume A8: n <= m ; :: thesis:
(Partial_Sums (F # x)) . m = ((Partial_Sums F) # x) . m by A1, A2, A3, A4, Th32;
hence |.((((Partial_Sums F) # x) . m) - g).| < p by A7, A8; :: thesis:

end;

hence (Partial_Sums F) # x is convergent_to_finite_number ; :: thesis:

end;

hereby :: thesis:

assume (Partial_Sums F) # x is convergent_to_finite_number ; :: thesis:
then consider g being Real such that
A10: 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) - g).| < p ;

now :: thesis:

let p be Real; :: thesis:
assume 0 < p ; :: thesis:
then consider n being Nat such that
A11: for m being Nat st n <= m holds
|.((((Partial_Sums F) # x) . m) - g).| < p by A10;
take n = n; :: thesis:
let m be Nat; :: thesis:
assume A12: n <= m ; :: thesis:
(Partial_Sums (F # x)) . m = ((Partial_Sums F) # x) . m by A1, A2, A3, A4, Th32;
hence |.(((Partial_Sums (F # x)) . m) - g).| < p by A11, A12; :: thesis:

end;

hence Partial_Sums (F # x) is convergent_to_finite_number ; :: thesis:

end;

hereby :: thesis:

assume A14: Partial_Sums (F # x) is convergent_to_+infty ; :: thesis:

now :: thesis:

let r be Real; :: thesis:
assume 0 < r ; :: thesis:
then consider n being Nat such that
A15: for m being Nat st n <= m holds
r <= (Partial_Sums (F # x)) . m by A14;
take n = n; :: thesis:
let m be Nat; :: thesis:
assume n <= m ; :: thesis:
then r <= (Partial_Sums (F # x)) . m by A15;
hence r <= ((Partial_Sums F) # x) . m by A1, A2, A3, A4, Th32; :: thesis:

end;

hence (Partial_Sums F) # x is convergent_to_+infty ; :: thesis:

end;

hereby :: thesis:

assume A17: (Partial_Sums F) # x is convergent_to_+infty ; :: thesis:

now :: thesis:

let r be Real; :: thesis:
assume 0 < r ; :: thesis:
then consider n being Nat such that
A18: for m being Nat st n <= m holds
r <= ((Partial_Sums F) # x) . m by A17;
take n = n; :: thesis:
let m be Nat; :: thesis:
assume n <= m ; :: thesis:
then r <= ((Partial_Sums F) # x) . m by A18;
hence r <= (Partial_Sums (F # x)) . m by A1, A2, A3, A4, Th32; :: thesis:

end;

hence Partial_Sums (F # x) is convergent_to_+infty ; :: thesis:

end;

hereby :: thesis:

assume A20: Partial_Sums (F # x) is convergent_to_-infty ; :: thesis:

now :: thesis:

let r be Real; :: thesis:
assume r < 0 ; :: thesis:
then consider n being Nat such that
A21: for m being Nat st n <= m holds
(Partial_Sums (F # x)) . m <= r by A20;
take n = n; :: thesis:
let m be Nat; :: thesis:
assume n <= m ; :: thesis:
then (Partial_Sums (F # x)) . m <= r by A21;
hence ((Partial_Sums F) # x) . m <= r by A1, A2, A3, A4, Th32; :: thesis:

end;

hence (Partial_Sums F) # x is convergent_to_-infty ; :: thesis:

end;

hereby :: thesis:

assume A23: (Partial_Sums F) # x is convergent_to_-infty ; :: thesis:

now :: thesis:

let r be Real; :: thesis:
assume r < 0 ; :: thesis:
then consider n being Nat such that
A24: for m being Nat st n <= m holds
((Partial_Sums F) # x) . m <= r by A23;
take n = n; :: thesis:
let m be Nat; :: thesis:
assume n <= m ; :: thesis:
then ((Partial_Sums F) # x) . m <= r by A24;
hence (Partial_Sums (F # x)) . m <= r by A1, A2, A3, A4, Th32; :: thesis:

end;

hence Partial_Sums (F # x) is convergent_to_-infty ; :: thesis:

end;

hereby :: thesis:

assume A25: Partial_Sums (F # x) is convergent ; :: thesis:

per cases by A25;

suppose Partial_Sums (F # x) is convergent_to_+infty ; :: thesis:

hence (Partial_Sums F) # x is convergent by A13; :: thesis:

end;

suppose Partial_Sums (F # x) is convergent_to_-infty ; :: thesis:

hence (Partial_Sums F) # x is convergent by A19; :: thesis:

end;

suppose Partial_Sums (F # x) is convergent_to_finite_number ; :: thesis:

hence (Partial_Sums F) # x is convergent by A5; :: thesis:

end;

assume A26: (Partial_Sums F) # x is convergent ; :: thesis:

per cases ) # x is convergent_to_+infty or (Partial_Sums F) # x is convergent_to_-infty or (Partial_Sums F) # x is convergent_to_finite_number ) by A26;

suppose (Partial_Sums F) # x is convergent_to_+infty ; :: thesis:

hence Partial_Sums (F # x) is convergent by A16; :: thesis:

end;

suppose (Partial_Sums F) # x is convergent_to_-infty ; :: thesis:

hence Partial_Sums (F # x) is convergent by A22; :: thesis:

end;

suppose (Partial_Sums F) # x is convergent_to_finite_number ; :: thesis:

hence Partial_Sums (F # x) is convergent by A9; :: thesis:

end;