let X be non empty set ; :: thesis: 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; :: thesis: ( ( 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 ; :: thesis: ( lim (Re f) = Re (lim f) & lim (Im f) = Im (lim f) )

hence lim (Re f) = Re (lim f) by A3, A5, PARTFUN1:5; :: thesis: 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;

hence lim (Im f) = Im (lim f) by A12, A13, PARTFUN1:5; :: thesis: verum

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; :: thesis: ( ( 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 ; :: thesis: ( lim (Re f) = Re (lim f) & lim (Im f) = Im (lim f) )

A5: now :: thesis: for x being Element of X st x in dom (lim (Re f)) holds

(lim (Re f)) . x = (Re (lim f)) . x

Re (lim f) is PartFunc of X,ExtREAL
by NUMBERS:31, RELSET_1:7;(lim (Re f)) . x = (Re (lim f)) . x

let x be Element of X; :: thesis: ( x in dom (lim (Re f)) implies (lim (Re f)) . x = (Re (lim f)) . x )

assume A6: x in dom (lim (Re f)) ; :: thesis: (lim (Re f)) . x = (Re (lim f)) . x

then 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; :: thesis: verum

end;assume A6: x in dom (lim (Re f)) ; :: thesis: (lim (Re f)) . x = (Re (lim f)) . x

then 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; :: thesis: verum

hence lim (Re f) = Re (lim f) by A3, A5, PARTFUN1:5; :: thesis: 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 :: thesis: for x being Element of X st x in dom (lim (Im f)) holds

(lim (Im f)) . x = (Im (lim f)) . x

Im (lim f) is PartFunc of X,ExtREAL
by NUMBERS:31, RELSET_1:7;(lim (Im f)) . x = (Im (lim f)) . x

let x be Element of X; :: thesis: ( x in dom (lim (Im f)) implies (lim (Im f)) . x = (Im (lim f)) . x )

assume A14: x in dom (lim (Im f)) ; :: thesis: (lim (Im f)) . x = (Im (lim f)) . x

then 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; :: thesis: verum

end;assume A14: x in dom (lim (Im f)) ; :: thesis: (lim (Im f)) . x = (Im (lim f)) . x

then 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; :: thesis: verum

hence lim (Im f) = Im (lim f) by A12, A13, PARTFUN1:5; :: thesis: verum