let X be non empty set ; :: thesis: for n being Nat

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)) . n = ((Partial_Sums F) # x) . n

let n be Nat; :: 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)) . n = ((Partial_Sums F) # x) . n

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)) . n = ((Partial_Sums F) # x) . n

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)) . n = ((Partial_Sums F) # x) . n

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)) . n = ((Partial_Sums F) # x) . n )

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)) . n = ((Partial_Sums F) # x) . n

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

dom ((Partial_Sums F) . n) = dom (F . 0) by A1, Th32;

then A5: x in dom ((Partial_Sums F) . n) by A2, A3;

then A6: x in dom (Re ((Partial_Sums F) . n)) by COMSEQ_3:def 3;

A7: Re F is with_the_same_dom by A1;

then Im F is with_the_same_dom by Th25;

then A8: (Partial_Sums ((Im F) # x)) . n = ((Partial_Sums (Im F)) # x) . n by A3, A4, Th12;

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

then A9: (Partial_Sums ((Re F) # x)) . n = ((Partial_Sums (Re F)) # x) . n by A3, A7, Th12;

A10: Re ((Partial_Sums (F # x)) . n) = (Re (Partial_Sums (F # x))) . n by COMSEQ_3:def 5

.= (Partial_Sums (Re (F # x))) . n by COMSEQ_3:26

.= (Partial_Sums ((Re F) # x)) . n by A1, A2, A3, MESFUN7C:23

.= ((Partial_Sums (Re F)) . n) . x by A9, SEQFUNC:def 10

.= ((Re (Partial_Sums F)) . n) . x by Th29

.= (Re ((Partial_Sums F) . n)) . x by MESFUN7C:24

.= Re (((Partial_Sums F) . n) . x) by A6, COMSEQ_3:def 3

.= Re (((Partial_Sums F) # x) . n) by MESFUN7C:def 9 ;

A11: x in dom (Im ((Partial_Sums F) . n)) by A5, COMSEQ_3:def 4;

A12: Im ((Partial_Sums (F # x)) . n) = (Im (Partial_Sums (F # x))) . n by COMSEQ_3:def 6

.= (Partial_Sums (Im (F # x))) . n by COMSEQ_3:26

.= (Partial_Sums ((Im F) # x)) . n by A1, A2, A3, MESFUN7C:23

.= ((Partial_Sums (Im F)) . n) . x by A8, SEQFUNC:def 10

.= ((Im (Partial_Sums F)) . n) . x by Th29

.= (Im ((Partial_Sums F) . n)) . x by MESFUN7C:24

.= Im (((Partial_Sums F) . n) . x) by A11, COMSEQ_3:def 4

.= Im (((Partial_Sums F) # x) . n) by MESFUN7C:def 9 ;

thus (Partial_Sums (F # x)) . n = (Re ((Partial_Sums (F # x)) . n)) + ((Im ((Partial_Sums (F # x)) . n)) * <i>) by COMPLEX1:13

.= ((Partial_Sums F) # x) . n by A10, A12, COMPLEX1:13 ; :: thesis: verum

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)) . n = ((Partial_Sums F) # x) . n

let n be Nat; :: 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)) . n = ((Partial_Sums F) # x) . n

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)) . n = ((Partial_Sums F) # x) . n

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)) . n = ((Partial_Sums F) # x) . n

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)) . n = ((Partial_Sums F) # x) . n )

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)) . n = ((Partial_Sums F) # x) . n

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

dom ((Partial_Sums F) . n) = dom (F . 0) by A1, Th32;

then A5: x in dom ((Partial_Sums F) . n) by A2, A3;

then A6: x in dom (Re ((Partial_Sums F) . n)) by COMSEQ_3:def 3;

A7: Re F is with_the_same_dom by A1;

then Im F is with_the_same_dom by Th25;

then A8: (Partial_Sums ((Im F) # x)) . n = ((Partial_Sums (Im F)) # x) . n by A3, A4, Th12;

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

then A9: (Partial_Sums ((Re F) # x)) . n = ((Partial_Sums (Re F)) # x) . n by A3, A7, Th12;

A10: Re ((Partial_Sums (F # x)) . n) = (Re (Partial_Sums (F # x))) . n by COMSEQ_3:def 5

.= (Partial_Sums (Re (F # x))) . n by COMSEQ_3:26

.= (Partial_Sums ((Re F) # x)) . n by A1, A2, A3, MESFUN7C:23

.= ((Partial_Sums (Re F)) . n) . x by A9, SEQFUNC:def 10

.= ((Re (Partial_Sums F)) . n) . x by Th29

.= (Re ((Partial_Sums F) . n)) . x by MESFUN7C:24

.= Re (((Partial_Sums F) . n) . x) by A6, COMSEQ_3:def 3

.= Re (((Partial_Sums F) # x) . n) by MESFUN7C:def 9 ;

A11: x in dom (Im ((Partial_Sums F) . n)) by A5, COMSEQ_3:def 4;

A12: Im ((Partial_Sums (F # x)) . n) = (Im (Partial_Sums (F # x))) . n by COMSEQ_3:def 6

.= (Partial_Sums (Im (F # x))) . n by COMSEQ_3:26

.= (Partial_Sums ((Im F) # x)) . n by A1, A2, A3, MESFUN7C:23

.= ((Partial_Sums (Im F)) . n) . x by A8, SEQFUNC:def 10

.= ((Im (Partial_Sums F)) . n) . x by Th29

.= (Im ((Partial_Sums F) . n)) . x by MESFUN7C:24

.= Im (((Partial_Sums F) . n) . x) by A11, COMSEQ_3:def 4

.= Im (((Partial_Sums F) # x) . n) by MESFUN7C:def 9 ;

thus (Partial_Sums (F # x)) . n = (Re ((Partial_Sums (F # x)) . n)) + ((Im ((Partial_Sums (F # x)) . n)) * <i>) by COMPLEX1:13

.= ((Partial_Sums F) # x) . n by A10, A12, COMPLEX1:13 ; :: thesis: verum