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)
B1: Re F is with_the_same_dom by A1, Lm33a;
then B4: Im F is with_the_same_dom by Lm33b;
( dom (Re f) = dom f & dom (Im f) = dom f ) by MESFUN6C:def 1, MESFUN6C:def 2;
then B2: ( dom (Re f) c= dom ((Re F) . 0 ) & dom (Im f) c= dom ((Im F) . 0 ) ) by A2, MESFUN7C:def 11, MESFUN7C:def 12;
B3: ( x in dom (Re f) & x in dom (Im f) ) by A3, MESFUN6C:def 1, MESFUN6C:def 2;
then B5: ( (Re f) . x = Re (f . x) & (Im f) . x = Im (f . x) ) by MESFUN6C:def 1, MESFUN6C:def 2;
( Re (F # x) = (Re F) # x & Im (F # x) = (Im F) # x ) by A1, A2, A3, MESFUN7C:23;
then Sum (F # x) = (Sum ((Re F) # x)) + ((Sum ((Im F) # x)) * <i> ) by A4, COMSEQ_3:54;
then ( Re (Sum (F # x)) = Sum ((Re F) # x) & Im (Sum (F # x)) = Sum ((Im F) # x) ) by COMPLEX1:28;
then ( (Re f) . x = Sum ((Re F) # x) & (Im f) . x = Sum ((Im F) # x) ) by A5, B3, MESFUN6C:def 1, MESFUN6C:def 2;
then B6: ( (Re f) . x = lim ((Partial_Sums (Re F)) # x) & (Im f) . x = lim ((Partial_Sums (Im F)) # x) ) by B1, B2, B3, B4, Th934r;
Partial_Sums (F # x) is convergent by A4;
then (Partial_Sums F) # x is convergent by A1, A2, A3, Cor01c;
then C1: ( 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;
C2: Partial_Sums F is with_the_same_dom by A1, ADD5c;
dom ((Partial_Sums F) . 0 ) = dom (F . 0 ) by A1, ADD0c;
then ( (Re (Partial_Sums F)) # x = Re ((Partial_Sums F) # x) & (Im (Partial_Sums F)) # x = Im ((Partial_Sums F) # x) ) by A2, A3, C2, MESFUN7C:23;
then C3: ( lim ((Partial_Sums (Re F)) # x) = lim (Re ((Partial_Sums F) # x)) & lim ((Partial_Sums (Im F)) # x) = lim (Im ((Partial_Sums F) # x)) ) by Lm326;
thus f . x = (Re (f . x)) + ((Im (f . x)) * <i> ) by COMPLEX1:29
.= lim ((Partial_Sums F) # x) by B5, B6, C1, C3, COMPLEX1:29 ; :: thesis: verum