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 & D c= dom (F . 0 ) ) and
A3: x in D ; :: thesis:

hereby :: thesis:

assume Partial_Sums (F # x) is convergent_to_finite_number ; :: thesis:
then consider g being real number such that
A4: 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) - (R_EAL g)).| < p by MESFUNC5:def 8;

now

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

end;

hence (Partial_Sums F) # x is convergent_to_finite_number by MESFUNC5:def 8; :: thesis:

end;

hereby :: thesis:

assume (Partial_Sums F) # x is convergent_to_finite_number ; :: thesis:
then consider g being real number such that
A7: 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) - (R_EAL g)).| < p by MESFUNC5:def 8;

now

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

end;

hence Partial_Sums (F # x) is convergent_to_finite_number by MESFUNC5:def 8; :: thesis:

end;

hereby :: thesis:

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

now

let r be real number ; :: thesis:
assume 0 < r ; :: thesis:
then consider n being Nat such that
B2: for m being Nat st n <= m holds
r <= (Partial_Sums (F # x)) . m by B1, MESFUNC5:def 9;
take n = n; :: thesis:
let m be Nat; :: thesis:
assume n <= m ; :: thesis:
then r <= (Partial_Sums (F # x)) . m by B2;
hence r <= ((Partial_Sums F) # x) . m by A1, A2, A3, Cor00; :: thesis:

end;

hence (Partial_Sums F) # x is convergent_to_+infty by MESFUNC5:def 9; :: thesis:

end;

hereby :: thesis:

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

now

let r be real number ; :: thesis:
assume 0 < r ; :: thesis:
then consider n being Nat such that
C2: for m being Nat st n <= m holds
r <= ((Partial_Sums F) # x) . m by C1, MESFUNC5:def 9;
take n = n; :: thesis:
let m be Nat; :: thesis:
assume n <= m ; :: thesis:
then r <= ((Partial_Sums F) # x) . m by C2;
hence r <= (Partial_Sums (F # x)) . m by A1, A2, A3, Cor00; :: thesis:

end;

hence Partial_Sums (F # x) is convergent_to_+infty by MESFUNC5:def 9; :: thesis:

end;

hereby :: thesis:

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

now

let r be real number ; :: thesis:
assume r < 0 ; :: thesis:
then consider n being Nat such that
D2: for m being Nat st n <= m holds
(Partial_Sums (F # x)) . m <= r by D1, MESFUNC5:def 10;
take n = n; :: thesis:
let m be Nat; :: thesis:
assume n <= m ; :: thesis:
then (Partial_Sums (F # x)) . m <= r by D2;
hence ((Partial_Sums F) # x) . m <= r by A1, A2, A3, Cor00; :: thesis:

end;

hence (Partial_Sums F) # x is convergent_to_-infty by MESFUNC5:def 10; :: thesis:

end;

hereby :: thesis:

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

now

let r be real number ; :: thesis:
assume r < 0 ; :: thesis:
then consider n being Nat such that
E2: for m being Nat st n <= m holds
((Partial_Sums F) # x) . m <= r by E1, MESFUNC5:def 10;
take n = n; :: thesis:
let m be Nat; :: thesis:
assume n <= m ; :: thesis:
then ((Partial_Sums F) # x) . m <= r by E2;
hence (Partial_Sums (F # x)) . m <= r by A1, A2, A3, Cor00; :: thesis:

end;

hence Partial_Sums (F # x) is convergent_to_-infty by MESFUNC5:def 10; :: thesis:

end;

hereby :: thesis:

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

per cases by F1, MESFUNC5:def 11;

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

hence (Partial_Sums F) # x is convergent by P3, MESFUNC5:def 11; :: thesis:

end;

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

hence (Partial_Sums F) # x is convergent by P5, MESFUNC5:def 11; :: thesis:

end;

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

hence (Partial_Sums F) # x is convergent by P1, MESFUNC5:def 11; :: thesis:

end;

assume F2: (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 F2, MESFUNC5:def 11;

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

hence Partial_Sums (F # x) is convergent by P4, MESFUNC5:def 11; :: thesis:

end;

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

hence Partial_Sums (F # x) is convergent by P6, MESFUNC5:def 11; :: thesis:

end;

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

hence Partial_Sums (F # x) is convergent by P2, MESFUNC5:def 11; :: thesis:

end;