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) and

A3: x in D ; :: thesis: ( Partial_Sums (F # x) is convergent iff (Partial_Sums F) # x is convergent )

A4: D c= dom ((Re F) . 0) by A2, MESFUN7C:def 11;

A5: D c= dom ((Im F) . 0) by A2, MESFUN7C:def 12;

A6: ( dom ((Partial_Sums F) . 0) = dom (F . 0) & Partial_Sums F is with_the_same_dom ) by A1, Th32, Th34;

A7: Re F is with_the_same_dom by A1;

then A8: Im F is with_the_same_dom by Th25;

then Im ((Partial_Sums F) # x) is convergent ;

then A12: (Im (Partial_Sums F)) # x is convergent by A2, A3, A6, MESFUN7C:23;

A13: (Im F) # x = Im (F # x) by A1, A2, A3, MESFUN7C:23;

Re ((Partial_Sums F) # x) is convergent by A11;

then A14: (Re (Partial_Sums F)) # x is convergent by A2, A3, A6, MESFUN7C:23;

( Partial_Sums ((Im F) # x) is convergent iff (Partial_Sums (Im F)) # x is convergent ) by A3, A8, A5, Th13;

then A15: Im (Partial_Sums (F # x)) is convergent by A12, A13, Th29, COMSEQ_3:26;

A16: (Re F) # x = Re (F # x) by A1, A2, A3, MESFUN7C:23;

( Partial_Sums ((Re F) # x) is convergent iff (Partial_Sums (Re F)) # x is convergent ) by A3, A7, A4, Th13;

then Re (Partial_Sums (F # x)) is convergent by A14, A16, Th29, COMSEQ_3:26;

hence Partial_Sums (F # x) is convergent by A15, COMSEQ_3:42; :: thesis: verum

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) and

A3: x in D ; :: thesis: ( Partial_Sums (F # x) is convergent iff (Partial_Sums F) # x is convergent )

A4: D c= dom ((Re F) . 0) by A2, MESFUN7C:def 11;

A5: D c= dom ((Im F) . 0) by A2, MESFUN7C:def 12;

A6: ( dom ((Partial_Sums F) . 0) = dom (F . 0) & Partial_Sums F is with_the_same_dom ) by A1, Th32, Th34;

A7: Re F is with_the_same_dom by A1;

then A8: Im F is with_the_same_dom by Th25;

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

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

then Im (Partial_Sums (F # x)) is convergent ;

then Partial_Sums (Im (F # x)) is convergent by COMSEQ_3:26;

then Partial_Sums ((Im F) # x) is convergent by A1, A2, A3, MESFUN7C:23;

then (Partial_Sums (Im F)) # x is convergent by A3, A8, A5, Th13;

then (Im (Partial_Sums F)) # x is convergent by Th29;

then A10: Im ((Partial_Sums F) # x) is convergent by A2, A3, A6, MESFUN7C:23;

Re (Partial_Sums (F # x)) is convergent by A9;

then Partial_Sums (Re (F # x)) is convergent by COMSEQ_3:26;

then Partial_Sums ((Re F) # x) is convergent by A1, A2, A3, MESFUN7C:23;

then (Partial_Sums (Re F)) # x is convergent by A3, A7, A4, Th13;

then (Re (Partial_Sums F)) # x is convergent by Th29;

then Re ((Partial_Sums F) # x) is convergent by A2, A3, A6, MESFUN7C:23;

hence (Partial_Sums F) # x is convergent by A10, COMSEQ_3:42; :: thesis: verum

end;then Im (Partial_Sums (F # x)) is convergent ;

then Partial_Sums (Im (F # x)) is convergent by COMSEQ_3:26;

then Partial_Sums ((Im F) # x) is convergent by A1, A2, A3, MESFUN7C:23;

then (Partial_Sums (Im F)) # x is convergent by A3, A8, A5, Th13;

then (Im (Partial_Sums F)) # x is convergent by Th29;

then A10: Im ((Partial_Sums F) # x) is convergent by A2, A3, A6, MESFUN7C:23;

Re (Partial_Sums (F # x)) is convergent by A9;

then Partial_Sums (Re (F # x)) is convergent by COMSEQ_3:26;

then Partial_Sums ((Re F) # x) is convergent by A1, A2, A3, MESFUN7C:23;

then (Partial_Sums (Re F)) # x is convergent by A3, A7, A4, Th13;

then (Re (Partial_Sums F)) # x is convergent by Th29;

then Re ((Partial_Sums F) # x) is convergent by A2, A3, A6, MESFUN7C:23;

hence (Partial_Sums F) # x is convergent by A10, COMSEQ_3:42; :: thesis: verum

then Im ((Partial_Sums F) # x) is convergent ;

then A12: (Im (Partial_Sums F)) # x is convergent by A2, A3, A6, MESFUN7C:23;

A13: (Im F) # x = Im (F # x) by A1, A2, A3, MESFUN7C:23;

Re ((Partial_Sums F) # x) is convergent by A11;

then A14: (Re (Partial_Sums F)) # x is convergent by A2, A3, A6, MESFUN7C:23;

( Partial_Sums ((Im F) # x) is convergent iff (Partial_Sums (Im F)) # x is convergent ) by A3, A8, A5, Th13;

then A15: Im (Partial_Sums (F # x)) is convergent by A12, A13, Th29, COMSEQ_3:26;

A16: (Re F) # x = Re (F # x) by A1, A2, A3, MESFUN7C:23;

( Partial_Sums ((Re F) # x) is convergent iff (Partial_Sums (Re F)) # x is convergent ) by A3, A7, A4, Th13;

then Re (Partial_Sums (F # x)) is convergent by A14, A16, Th29, COMSEQ_3:26;

hence Partial_Sums (F # x) is convergent by A15, COMSEQ_3:42; :: thesis: verum