let X be non empty set ; for f being with_the_same_dom Functional_Sequence of X,COMPLEX st ( for x being Element of X st x in dom (f . 0) holds
f # x is convergent ) holds
( lim (Re f) = Re (lim f) & lim (Im f) = Im (lim f) )
let f be with_the_same_dom Functional_Sequence of X,COMPLEX; ( ( for x being Element of X st x in dom (f . 0) holds
f # x is convergent ) implies ( lim (Re f) = Re (lim f) & lim (Im f) = Im (lim f) ) )
dom (lim (Re f)) = dom ((Re f) . 0)
by MESFUNC8:def 9;
then A1:
dom (lim (Re f)) = dom (f . 0)
by Def11;
A2:
dom (Re (lim f)) = dom (lim f)
by COMSEQ_3:def 3;
then A3:
dom (lim (Re f)) = dom (Re (lim f))
by A1, Def10;
assume A4:
for x being Element of X st x in dom (f . 0) holds
f # x is convergent
; ( lim (Re f) = Re (lim f) & lim (Im f) = Im (lim f) )
A5:
now for x being Element of X st x in dom (lim (Re f)) holds
(lim (Re f)) . x = (Re (lim f)) . xlet x be
Element of
X;
( x in dom (lim (Re f)) implies (lim (Re f)) . x = (Re (lim f)) . x )assume A6:
x in dom (lim (Re f))
;
(lim (Re f)) . x = (Re (lim f)) . xthen A7:
f # x is
convergent
by A4, A1;
then
Re (f # x) is
convergent
;
then A8:
(Re f) # x is
convergent
by A1, A6, Th23;
(lim (Re f)) . x =
lim (R_EAL ((Re f) # x))
by A6, Th14
.=
lim ((Re f) # x)
by A8, RINFSUP2:14
;
then
(lim (Re f)) . x = lim (Re (f # x))
by A1, A6, Th23;
then A9:
(lim (Re f)) . x = Re (lim (f # x))
by A7, COMSEQ_3:41;
(Re (lim f)) . x = Re ((lim f) . x)
by A3, A6, COMSEQ_3:def 3;
hence
(lim (Re f)) . x = (Re (lim f)) . x
by A2, A3, A6, A9, Def10;
verum end;
Re (lim f) is PartFunc of X,ExtREAL
by NUMBERS:31, RELSET_1:7;
hence
lim (Re f) = Re (lim f)
by A3, A5, PARTFUN1:5; lim (Im f) = Im (lim f)
dom (lim (Im f)) = dom ((Im f) . 0)
by MESFUNC8:def 9;
then A10:
dom (lim (Im f)) = dom (f . 0)
by Def12;
A11:
dom (Im (lim f)) = dom (lim f)
by COMSEQ_3:def 4;
then A12:
dom (lim (Im f)) = dom (Im (lim f))
by A10, Def10;
A13:
now for x being Element of X st x in dom (lim (Im f)) holds
(lim (Im f)) . x = (Im (lim f)) . xlet x be
Element of
X;
( x in dom (lim (Im f)) implies (lim (Im f)) . x = (Im (lim f)) . x )assume A14:
x in dom (lim (Im f))
;
(lim (Im f)) . x = (Im (lim f)) . xthen A15:
f # x is
convergent
by A4, A10;
then
Im (f # x) is
convergent
;
then A16:
(Im f) # x is
convergent
by A10, A14, Th23;
(lim (Im f)) . x =
lim (R_EAL ((Im f) # x))
by A14, Th14
.=
lim ((Im f) # x)
by A16, RINFSUP2:14
;
then
(lim (Im f)) . x = lim (Im (f # x))
by A10, A14, Th23;
then A17:
(lim (Im f)) . x = Im (lim (f # x))
by A15, COMSEQ_3:41;
(Im (lim f)) . x = Im ((lim f) . x)
by A12, A14, COMSEQ_3:def 4;
hence
(lim (Im f)) . x = (Im (lim f)) . x
by A11, A12, A14, A17, Def10;
verum end;
Im (lim f) is PartFunc of X,ExtREAL
by NUMBERS:31, RELSET_1:7;
hence
lim (Im f) = Im (lim f)
by A12, A13, PARTFUN1:5; verum