let X be non empty set ; :: thesis: for D being set

for F being Functional_Sequence of X,COMPLEX st F is with_the_same_dom & D = dom (F . 0) & ( for x being Element of X st x in D holds

F # x is convergent ) holds

(lim F) | D = lim (F || D)

let D be set ; :: thesis: for F being Functional_Sequence of X,COMPLEX st F is with_the_same_dom & D = dom (F . 0) & ( for x being Element of X st x in D holds

F # x is convergent ) holds

(lim F) | D = lim (F || D)

let F be Functional_Sequence of X,COMPLEX; :: thesis: ( F is with_the_same_dom & D = dom (F . 0) & ( for x being Element of X st x in D holds

F # x is convergent ) implies (lim F) | D = lim (F || D) )

set G = F || D;

assume that

A1: F is with_the_same_dom and

A2: D = dom (F . 0) and

A3: for x being Element of X st x in D holds

F # x is convergent ; :: thesis: (lim F) | D = lim (F || D)

A4: Re (F || D) = (Re F) || D by Th21;

(Re F) # x is convergent

then (lim (Re F)) | D = lim (Re (F || D)) by A4, A8, Th3;

then A10: (Re (lim F)) | D = lim (Re (F || D)) by A1, A2, A3, MESFUN7C:25;

A11: F || D is with_the_same_dom by A1, Th2;

then lim (Re (F || D)) = Re (lim (F || D)) by A5, MESFUN7C:25;

then A12: Re ((lim F) | D) = Re (lim (F || D)) by A10, Th20;

A13: for x being Element of X st x in D holds

(Im F) # x is convergent

D c= dom ((Im F) . 0) by A2, MESFUN7C:def 12;

then (lim (Im F)) | D = lim (Im (F || D)) by A15, A13, Th3;

then A16: (Im (lim F)) | D = lim (Im (F || D)) by A1, A2, A3, MESFUN7C:25;

lim (Im (F || D)) = Im (lim (F || D)) by A11, A5, MESFUN7C:25;

then A17: Im ((lim F) | D) = Im (lim (F || D)) by A16, Th20;

thus lim (F || D) = (Re (lim (F || D))) + (<i> (#) (Im (lim (F || D)))) by MESFUN6C:8

.= (lim F) | D by A12, A17, MESFUN6C:8 ; :: thesis: verum

for F being Functional_Sequence of X,COMPLEX st F is with_the_same_dom & D = dom (F . 0) & ( for x being Element of X st x in D holds

F # x is convergent ) holds

(lim F) | D = lim (F || D)

let D be set ; :: thesis: for F being Functional_Sequence of X,COMPLEX st F is with_the_same_dom & D = dom (F . 0) & ( for x being Element of X st x in D holds

F # x is convergent ) holds

(lim F) | D = lim (F || D)

let F be Functional_Sequence of X,COMPLEX; :: thesis: ( F is with_the_same_dom & D = dom (F . 0) & ( for x being Element of X st x in D holds

F # x is convergent ) implies (lim F) | D = lim (F || D) )

set G = F || D;

assume that

A1: F is with_the_same_dom and

A2: D = dom (F . 0) and

A3: for x being Element of X st x in D holds

F # x is convergent ; :: thesis: (lim F) | D = lim (F || D)

A4: Re (F || D) = (Re F) || D by Th21;

A5: now :: thesis: for x being Element of X st x in dom ((F || D) . 0) holds

(F || D) # x is convergent

A8:
for x being Element of X st x in D holds (F || D) # x is convergent

let x be Element of X; :: thesis: ( x in dom ((F || D) . 0) implies (F || D) # x is convergent )

dom ((F . 0) | D) = D by A2, RELAT_1:62;

then A6: dom ((F || D) . 0) = D by Def1;

assume A7: x in dom ((F || D) . 0) ; :: thesis: (F || D) # x is convergent

then F # x is convergent by A3, A6;

hence (F || D) # x is convergent by A1, A2, A7, A6, Th23; :: thesis: verum

end;dom ((F . 0) | D) = D by A2, RELAT_1:62;

then A6: dom ((F || D) . 0) = D by Def1;

assume A7: x in dom ((F || D) . 0) ; :: thesis: (F || D) # x is convergent

then F # x is convergent by A3, A6;

hence (F || D) # x is convergent by A1, A2, A7, A6, Th23; :: thesis: verum

(Re F) # x is convergent

proof

D c= dom ((Re F) . 0)
by A2, MESFUN7C:def 11;
let x be Element of X; :: thesis: ( x in D implies (Re F) # x is convergent )

assume A9: x in D ; :: thesis: (Re F) # x is convergent

then F # x is convergent Complex_Sequence by A3;

then Re (F # x) is convergent ;

hence (Re F) # x is convergent by A1, A2, A9, MESFUN7C:23; :: thesis: verum

end;assume A9: x in D ; :: thesis: (Re F) # x is convergent

then F # x is convergent Complex_Sequence by A3;

then Re (F # x) is convergent ;

hence (Re F) # x is convergent by A1, A2, A9, MESFUN7C:23; :: thesis: verum

then (lim (Re F)) | D = lim (Re (F || D)) by A4, A8, Th3;

then A10: (Re (lim F)) | D = lim (Re (F || D)) by A1, A2, A3, MESFUN7C:25;

A11: F || D is with_the_same_dom by A1, Th2;

then lim (Re (F || D)) = Re (lim (F || D)) by A5, MESFUN7C:25;

then A12: Re ((lim F) | D) = Re (lim (F || D)) by A10, Th20;

A13: for x being Element of X st x in D holds

(Im F) # x is convergent

proof

A15:
Im (F || D) = (Im F) || D
by Th22;
let x be Element of X; :: thesis: ( x in D implies (Im F) # x is convergent )

assume A14: x in D ; :: thesis: (Im F) # x is convergent

then F # x is convergent Complex_Sequence by A3;

then Im (F # x) is convergent ;

hence (Im F) # x is convergent by A1, A2, A14, MESFUN7C:23; :: thesis: verum

end;assume A14: x in D ; :: thesis: (Im F) # x is convergent

then F # x is convergent Complex_Sequence by A3;

then Im (F # x) is convergent ;

hence (Im F) # x is convergent by A1, A2, A14, MESFUN7C:23; :: thesis: verum

D c= dom ((Im F) . 0) by A2, MESFUN7C:def 12;

then (lim (Im F)) | D = lim (Im (F || D)) by A15, A13, Th3;

then A16: (Im (lim F)) | D = lim (Im (F || D)) by A1, A2, A3, MESFUN7C:25;

lim (Im (F || D)) = Im (lim (F || D)) by A11, A5, MESFUN7C:25;

then A17: Im ((lim F) | D) = Im (lim (F || D)) by A16, Th20;

thus lim (F || D) = (Re (lim (F || D))) + (<i> (#) (Im (lim (F || D)))) by MESFUN6C:8

.= (lim F) | D by A12, A17, MESFUN6C:8 ; :: thesis: verum