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 ) & x in D ) ; :: thesis: (Partial_Sums (F # x)) . n = ((Partial_Sums F) # x) . n
dom ((Partial_Sums F) . n) = dom (F . 0 ) by A1, ADD0c;
then x in dom ((Partial_Sums F) . n) by A2;
then A4: ( x in dom (Re ((Partial_Sums F) . n)) & x in dom (Im ((Partial_Sums F) . n)) ) by MESFUN6C:def 1, MESFUN6C:def 2;
B1: Re F is with_the_same_dom by A1, Lm33a;
then B4: Im F is with_the_same_dom by Lm33b;
( D c= dom ((Re F) . 0 ) & D c= dom ((Im F) . 0 ) ) by A2, MESFUN7C:def 11, MESFUN7C:def 12;
then B3: ( (Partial_Sums ((Re F) # x)) . n = ((Partial_Sums (Re F)) # x) . n & (Partial_Sums ((Im F) # x)) . n = ((Partial_Sums (Im F)) # x) . n ) by A2, B1, B4, Cor00;
C0: n is Element of NAT by ORDINAL1:def 13;
then C1: Re ((Partial_Sums (F # x)) . n) = (Re (Partial_Sums (F # x))) . n by COMSEQ_3:def 3
.= (Partial_Sums (Re (F # x))) . n by COMSEQ_3:26
.= (Partial_Sums ((Re F) # x)) . n by A1, A2, MESFUN7C:23
.= ((Partial_Sums (Re F)) . n) . x by C0, B3, SEQFUNC:def 11
.= ((Re (Partial_Sums F)) . n) . x by Lm326
.= (Re ((Partial_Sums F) . n)) . x by MESFUN7C:24
.= Re (((Partial_Sums F) . n) . x) by A4, MESFUN6C:def 1
.= Re (((Partial_Sums F) # x) . n) by MESFUN7C:def 9 ;
D1: Im ((Partial_Sums (F # x)) . n) = (Im (Partial_Sums (F # x))) . n by C0, COMSEQ_3:def 4
.= (Partial_Sums (Im (F # x))) . n by COMSEQ_3:26
.= (Partial_Sums ((Im F) # x)) . n by A1, A2, MESFUN7C:23
.= ((Partial_Sums (Im F)) . n) . x by C0, B3, SEQFUNC:def 11
.= ((Im (Partial_Sums F)) . n) . x by Lm326
.= (Im ((Partial_Sums F) . n)) . x by MESFUN7C:24
.= Im (((Partial_Sums F) . n) . x) by A4, MESFUN6C:def 2
.= 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:29
.= ((Partial_Sums F) # x) . n by C1, D1, COMPLEX1:29 ; :: thesis: verum