let X be non empty set ; :: thesis: for x being Element of X

for F being Functional_Sequence of X,COMPLEX

for f being PartFunc of X,COMPLEX st F is with_the_same_dom & dom f c= dom (F . 0) & x in dom f & F # x is summable & f . x = Sum (F # x) holds

f . x = lim ((Partial_Sums F) # x)

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

for f being PartFunc of X,COMPLEX st F is with_the_same_dom & dom f c= dom (F . 0) & x in dom f & F # x is summable & f . x = Sum (F # x) holds

f . x = lim ((Partial_Sums F) # x)

let F be Functional_Sequence of X,COMPLEX; :: thesis: for f being PartFunc of X,COMPLEX st F is with_the_same_dom & dom f c= dom (F . 0) & x in dom f & F # x is summable & f . x = Sum (F # x) holds

f . x = lim ((Partial_Sums F) # x)

let f be PartFunc of X,COMPLEX; :: thesis: ( F is with_the_same_dom & dom f c= dom (F . 0) & x in dom f & F # x is summable & f . x = Sum (F # x) implies f . x = lim ((Partial_Sums F) # x) )

assume that

A1: F is with_the_same_dom and

A2: dom f c= dom (F . 0) and

A3: x in dom f and

A4: F # x is summable and

A5: f . x = Sum (F # x) ; :: thesis: f . x = lim ((Partial_Sums F) # x)

dom (Re f) = dom f by COMSEQ_3:def 3;

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

Partial_Sums (F # x) is convergent by A4;

then (Partial_Sums F) # x is convergent by A1, A2, A3, Th35;

then A7: ( lim (Re ((Partial_Sums F) # x)) = Re (lim ((Partial_Sums F) # x)) & lim (Im ((Partial_Sums F) # x)) = Im (lim ((Partial_Sums F) # x)) ) by COMSEQ_3:41;

dom (Im f) = dom f by COMSEQ_3:def 4;

then A8: dom (Im f) c= dom ((Im F) . 0) by A2, MESFUN7C:def 12;

A9: x in dom (Im f) by A3, COMSEQ_3:def 4;

then A10: (Im f) . x = Im (f . x) by COMSEQ_3:def 4;

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

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

then A12: lim ((Partial_Sums (Re F)) # x) = lim (Re ((Partial_Sums F) # x)) by Th29;

(Im (Partial_Sums F)) # x = Im ((Partial_Sums F) # x) by A2, A3, A11, MESFUN7C:23;

then A13: lim ((Partial_Sums (Im F)) # x) = lim (Im ((Partial_Sums F) # x)) by Th29;

A14: x in dom (Re f) by A3, COMSEQ_3:def 3;

then A15: (Re f) . x = Re (f . x) by COMSEQ_3:def 3;

A16: Re F is with_the_same_dom by A1;

then A17: Im F is with_the_same_dom by Th25;

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

then A18: Sum (F # x) = (Sum ((Re F) # x)) + ((Sum ((Im F) # x)) * <i>) by A4, COMSEQ_3:53;

then Re (Sum (F # x)) = Sum ((Re F) # x) by COMPLEX1:12;

then (Re f) . x = Sum ((Re F) # x) by A5, A14, COMSEQ_3:def 3;

then A19: (Re f) . x = lim ((Partial_Sums (Re F)) # x) by A16, A6, A14, Th14;

Im (Sum (F # x)) = Sum ((Im F) # x) by A18, COMPLEX1:12;

then (Im f) . x = Sum ((Im F) # x) by A5, A9, COMSEQ_3:def 4;

then A20: (Im f) . x = lim ((Partial_Sums (Im F)) # x) by A17, A8, A9, Th14;

thus f . x = (Re (f . x)) + ((Im (f . x)) * <i>) by COMPLEX1:13

.= lim ((Partial_Sums F) # x) by A15, A10, A19, A20, A7, A12, A13, COMPLEX1:13 ; :: thesis: verum

for F being Functional_Sequence of X,COMPLEX

for f being PartFunc of X,COMPLEX st F is with_the_same_dom & dom f c= dom (F . 0) & x in dom f & F # x is summable & f . x = Sum (F # x) holds

f . x = lim ((Partial_Sums F) # x)

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

for f being PartFunc of X,COMPLEX st F is with_the_same_dom & dom f c= dom (F . 0) & x in dom f & F # x is summable & f . x = Sum (F # x) holds

f . x = lim ((Partial_Sums F) # x)

let F be Functional_Sequence of X,COMPLEX; :: thesis: for f being PartFunc of X,COMPLEX st F is with_the_same_dom & dom f c= dom (F . 0) & x in dom f & F # x is summable & f . x = Sum (F # x) holds

f . x = lim ((Partial_Sums F) # x)

let f be PartFunc of X,COMPLEX; :: thesis: ( F is with_the_same_dom & dom f c= dom (F . 0) & x in dom f & F # x is summable & f . x = Sum (F # x) implies f . x = lim ((Partial_Sums F) # x) )

assume that

A1: F is with_the_same_dom and

A2: dom f c= dom (F . 0) and

A3: x in dom f and

A4: F # x is summable and

A5: f . x = Sum (F # x) ; :: thesis: f . x = lim ((Partial_Sums F) # x)

dom (Re f) = dom f by COMSEQ_3:def 3;

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

Partial_Sums (F # x) is convergent by A4;

then (Partial_Sums F) # x is convergent by A1, A2, A3, Th35;

then A7: ( lim (Re ((Partial_Sums F) # x)) = Re (lim ((Partial_Sums F) # x)) & lim (Im ((Partial_Sums F) # x)) = Im (lim ((Partial_Sums F) # x)) ) by COMSEQ_3:41;

dom (Im f) = dom f by COMSEQ_3:def 4;

then A8: dom (Im f) c= dom ((Im F) . 0) by A2, MESFUN7C:def 12;

A9: x in dom (Im f) by A3, COMSEQ_3:def 4;

then A10: (Im f) . x = Im (f . x) by COMSEQ_3:def 4;

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

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

then A12: lim ((Partial_Sums (Re F)) # x) = lim (Re ((Partial_Sums F) # x)) by Th29;

(Im (Partial_Sums F)) # x = Im ((Partial_Sums F) # x) by A2, A3, A11, MESFUN7C:23;

then A13: lim ((Partial_Sums (Im F)) # x) = lim (Im ((Partial_Sums F) # x)) by Th29;

A14: x in dom (Re f) by A3, COMSEQ_3:def 3;

then A15: (Re f) . x = Re (f . x) by COMSEQ_3:def 3;

A16: Re F is with_the_same_dom by A1;

then A17: Im F is with_the_same_dom by Th25;

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

then A18: Sum (F # x) = (Sum ((Re F) # x)) + ((Sum ((Im F) # x)) * <i>) by A4, COMSEQ_3:53;

then Re (Sum (F # x)) = Sum ((Re F) # x) by COMPLEX1:12;

then (Re f) . x = Sum ((Re F) # x) by A5, A14, COMSEQ_3:def 3;

then A19: (Re f) . x = lim ((Partial_Sums (Re F)) # x) by A16, A6, A14, Th14;

Im (Sum (F # x)) = Sum ((Im F) # x) by A18, COMPLEX1:12;

then (Im f) . x = Sum ((Im F) # x) by A5, A9, COMSEQ_3:def 4;

then A20: (Im f) . x = lim ((Partial_Sums (Im F)) # x) by A17, A8, A9, Th14;

thus f . x = (Re (f . x)) + ((Im (f . x)) * <i>) by COMPLEX1:13

.= lim ((Partial_Sums F) # x) by A15, A10, A19, A20, A7, A12, A13, COMPLEX1:13 ; :: thesis: verum