let X be non empty set ; :: thesis: for x being Element of X
for D being set
for F being Functional_Sequence of X,COMPLEX 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
for F being Functional_Sequence of X,COMPLEX 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: for F being Functional_Sequence of X,COMPLEX 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,COMPLEX ; :: 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 that
A1: F is with_the_same_dom and
A2: ( D c= dom (F . 0 ) & x in D ) ; :: thesis: ( Partial_Sums (F # x) is convergent iff (Partial_Sums F) # x is convergent )
A3: dom ((Partial_Sums F) . 0 ) = dom (F . 0 ) by A1, ADD0c;
A5: Partial_Sums F is with_the_same_dom by A1, ADD5c;
B1: Re F is with_the_same_dom by A1, Lm33a;
then B4: Im F is with_the_same_dom by Lm33b;
B2: ( D c= dom ((Re F) . 0 ) & D c= dom ((Im F) . 0 ) ) by A2, MESFUN7C:def 11, MESFUN7C:def 12;
then B3: ( ( Partial_Sums ((Re F) # x) is convergent implies (Partial_Sums (Re F)) # x is convergent ) & ( (Partial_Sums (Re F)) # x is convergent implies Partial_Sums ((Re F) # x) is convergent ) & ( Partial_Sums ((Im F) # x) is convergent implies (Partial_Sums (Im F)) # x is convergent ) & ( (Partial_Sums (Im F)) # x is convergent implies Partial_Sums ((Im F) # x) is convergent ) ) by A2, B1, B4, Cor01;

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
then ( Re (Partial_Sums (F # x)) is convergent & Im (Partial_Sums (F # x)) is convergent ) ;
then ( Partial_Sums (Re (F # x)) is convergent & Partial_Sums (Im (F # x)) is convergent ) by COMSEQ_3:26;
then ( Partial_Sums ((Re F) # x) is convergent & Partial_Sums ((Im F) # x) is convergent ) by A1, A2, MESFUN7C:23;
then ( (Partial_Sums (Re F)) # x is convergent & (Partial_Sums (Im F)) # x is convergent ) by A2, B1, B2, B4, Cor01;
then ( (Re (Partial_Sums F)) # x is convergent & (Im (Partial_Sums F)) # x is convergent ) by Lm326;
then ( Re ((Partial_Sums F) # x) is convergent & Im ((Partial_Sums F) # x) is convergent ) by A2, A3, A5, MESFUN7C:23;
hence (Partial_Sums F) # x is convergent by COMSEQ_3:42; :: thesis: verum

end;

assume (Partial_Sums F) # x is convergent ; :: thesis: Partial_Sums (F # x) is convergent
then ( Re ((Partial_Sums F) # x) is convergent & Im ((Partial_Sums F) # x) is convergent ) ;
then D1: ( (Re (Partial_Sums F)) # x is convergent & (Im (Partial_Sums F)) # x is convergent ) by A2, A3, A5, MESFUN7C:23;
( (Re F) # x = Re (F # x) & (Im F) # x = Im (F # x) ) by A1, A2, MESFUN7C:23;
then ( Re (Partial_Sums (F # x)) is convergent & Im (Partial_Sums (F # x)) is convergent ) by D1, B3, Lm326, COMSEQ_3:26;
hence Partial_Sums (F # x) is convergent by COMSEQ_3:42; :: thesis: verum