let X be non empty set ; 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; 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; 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; ( 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)
; 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
; verum