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