let X be non empty set ; :: thesis: for F being Functional_Sequence of X,REAL

for x being Element of X

for D being set st F is with_the_same_dom & D c= dom (F . 0) & x in D holds

( Partial_Sums (F # x) is convergent iff (Partial_Sums F) # x is convergent )

let F be Functional_Sequence of X,REAL; :: thesis: for x being Element of X

for D being set st F is with_the_same_dom & D c= dom (F . 0) & x in D holds

( Partial_Sums (F # x) is convergent iff (Partial_Sums F) # x is convergent )

let x be Element of X; :: thesis: for D being set st F is with_the_same_dom & D c= dom (F . 0) & x in D holds

( Partial_Sums (F # x) is convergent iff (Partial_Sums F) # x is convergent )

let D be set ; :: thesis: ( F is with_the_same_dom & D c= dom (F . 0) & x in D implies ( Partial_Sums (F # x) is convergent iff (Partial_Sums F) # x is convergent ) )

assume A1: ( F is with_the_same_dom & D c= dom (F . 0) & x in D ) ; :: thesis: ( Partial_Sums (F # x) is convergent iff (Partial_Sums F) # x is convergent )

A2: R_EAL (F # x) = (R_EAL F) # x by MESFUN7C:1;

Partial_Sums (R_EAL F) = R_EAL (Partial_Sums F) by Th7;

then A3: (Partial_Sums (R_EAL F)) # x = (Partial_Sums F) # x by MESFUN7C:1;

A4: Partial_Sums (F # x) = R_EAL (Partial_Sums (F # x))

.= Partial_Sums (R_EAL (F # x)) by Th5 ;

A5: R_EAL F is additive by Th9;

then (Partial_Sums (R_EAL F)) # x is convergent_to_finite_number by A3, RINFSUP2:14;

then Partial_Sums ((R_EAL F) # x) is convergent_to_finite_number by A1, A5, MESFUNC9:33;

hence Partial_Sums (F # x) is convergent by A4, A2, RINFSUP2:15; :: thesis: verum

for x being Element of X

for D being set st F is with_the_same_dom & D c= dom (F . 0) & x in D holds

( Partial_Sums (F # x) is convergent iff (Partial_Sums F) # x is convergent )

let F be Functional_Sequence of X,REAL; :: thesis: for x being Element of X

for D being set st F is with_the_same_dom & D c= dom (F . 0) & x in D holds

( Partial_Sums (F # x) is convergent iff (Partial_Sums F) # x is convergent )

let x be Element of X; :: thesis: for D being set st F is with_the_same_dom & D c= dom (F . 0) & x in D holds

( Partial_Sums (F # x) is convergent iff (Partial_Sums F) # x is convergent )

let D be set ; :: thesis: ( F is with_the_same_dom & D c= dom (F . 0) & x in D implies ( Partial_Sums (F # x) is convergent iff (Partial_Sums F) # x is convergent ) )

assume A1: ( F is with_the_same_dom & D c= dom (F . 0) & x in D ) ; :: thesis: ( Partial_Sums (F # x) is convergent iff (Partial_Sums F) # x is convergent )

A2: R_EAL (F # x) = (R_EAL F) # x by MESFUN7C:1;

Partial_Sums (R_EAL F) = R_EAL (Partial_Sums F) by Th7;

then A3: (Partial_Sums (R_EAL F)) # x = (Partial_Sums F) # x by MESFUN7C:1;

A4: Partial_Sums (F # x) = R_EAL (Partial_Sums (F # x))

.= Partial_Sums (R_EAL (F # x)) by Th5 ;

A5: R_EAL F is additive by Th9;

hereby :: thesis: ( (Partial_Sums F) # x is convergent implies Partial_Sums (F # x) is convergent )

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

then Partial_Sums (R_EAL (F # x)) is convergent_to_finite_number by A4, RINFSUP2:14;

then (Partial_Sums (R_EAL F)) # x is convergent_to_finite_number by A1, A5, A2, MESFUNC9:33;

hence (Partial_Sums F) # x is convergent by A3, RINFSUP2:15; :: thesis: verum

end;then Partial_Sums (R_EAL (F # x)) is convergent_to_finite_number by A4, RINFSUP2:14;

then (Partial_Sums (R_EAL F)) # x is convergent_to_finite_number by A1, A5, A2, MESFUNC9:33;

hence (Partial_Sums F) # x is convergent by A3, RINFSUP2:15; :: thesis: verum

then (Partial_Sums (R_EAL F)) # x is convergent_to_finite_number by A3, RINFSUP2:14;

then Partial_Sums ((R_EAL F) # x) is convergent_to_finite_number by A1, A5, MESFUNC9:33;

hence Partial_Sums (F # x) is convergent by A4, A2, RINFSUP2:15; :: thesis: verum