let X be non empty set ; for S being SigmaField of X
for F being Functional_Sequence of X,ExtREAL st F is additive & F is with_the_same_dom & ( for x being Element of X st x in dom (F . 0) holds
F # x is summable ) holds
lim (Partial_Sums (- F)) = - (lim (Partial_Sums F))
let S be SigmaField of X; for F being Functional_Sequence of X,ExtREAL st F is additive & F is with_the_same_dom & ( for x being Element of X st x in dom (F . 0) holds
F # x is summable ) holds
lim (Partial_Sums (- F)) = - (lim (Partial_Sums F))
let F be Functional_Sequence of X,ExtREAL; ( F is additive & F is with_the_same_dom & ( for x being Element of X st x in dom (F . 0) holds
F # x is summable ) implies lim (Partial_Sums (- F)) = - (lim (Partial_Sums F)) )
assume that
A1:
F is additive
and
A2:
F is with_the_same_dom
and
A3:
for x being Element of X st x in dom (F . 0) holds
F # x is summable
; lim (Partial_Sums (- F)) = - (lim (Partial_Sums F))
set G = - F;
for n being Element of NAT holds (Partial_Sums (- F)) . n = (- (Partial_Sums F)) . n
by Th42;
then A4:
Partial_Sums (- F) = - (Partial_Sums F)
by FUNCT_2:def 7;
A5: dom (lim (Partial_Sums (- F))) =
dom ((Partial_Sums (- F)) . 0)
by MESFUNC8:def 9
.=
dom ((- F) . 0)
by MESFUNC9:def 4
.=
dom (- (F . 0))
by Th37
.=
dom (F . 0)
by MESFUNC1:def 7
;
A6:
dom (- (lim (Partial_Sums F))) = dom (lim (Partial_Sums F))
by MESFUNC1:def 7;
then A7: dom (- (lim (Partial_Sums F))) =
dom ((Partial_Sums F) . 0)
by MESFUNC8:def 9
.=
dom (F . 0)
by MESFUNC9:def 4
;
for x being Element of X st x in dom (lim (Partial_Sums (- F))) holds
(lim (Partial_Sums (- F))) . x = (- (lim (Partial_Sums F))) . x
proof
let x be
Element of
X;
( x in dom (lim (Partial_Sums (- F))) implies (lim (Partial_Sums (- F))) . x = (- (lim (Partial_Sums F))) . x )
assume A8:
x in dom (lim (Partial_Sums (- F)))
;
(lim (Partial_Sums (- F))) . x = (- (lim (Partial_Sums F))) . x
then
F # x is
summable
by A3, A5;
then
Partial_Sums (F # x) is
convergent
by MESFUNC9:def 2;
then A9:
(Partial_Sums F) # x is
convergent
by A1, A2, A8, A5, MESFUNC9:33;
(Partial_Sums (- F)) # x = - ((Partial_Sums F) # x)
by A4, Th38;
then A10:
lim ((Partial_Sums (- F)) # x) = - (lim ((Partial_Sums F) # x))
by A9, DBLSEQ_3:17;
(- (lim (Partial_Sums F))) . x = - ((lim (Partial_Sums F)) . x)
by A7, A5, A8, MESFUNC1:def 7;
then
(- (lim (Partial_Sums F))) . x = - (lim ((Partial_Sums F) # x))
by A7, A5, A8, A6, MESFUNC8:def 9;
hence
(lim (Partial_Sums (- F))) . x = (- (lim (Partial_Sums F))) . x
by A8, A10, MESFUNC8:def 9;
verum
end;
hence
lim (Partial_Sums (- F)) = - (lim (Partial_Sums F))
by A7, A5, PARTFUN1:5; verum