let X be non empty set ; :: thesis: for F being Functional_Sequence of X,REAL

for D being set st D c= 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,REAL; :: thesis: for D being set st D c= 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: ( D c= 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: D c= dom (F . 0) and

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

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

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

(R_EAL F) # x is convergent

hence (lim F) | D = lim (F || D) by A1, A3, MESFUNC9:19; :: thesis: verum

for D being set st D c= 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,REAL; :: thesis: for D being set st D c= 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: ( D c= 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: D c= dom (F . 0) and

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

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

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

(R_EAL F) # x is convergent

proof

for n being Nat holds (R_EAL (F || D)) . n = ((R_EAL F) . n) | D
by Def1;
let x be Element of X; :: thesis: ( x in D implies (R_EAL F) # x is convergent )

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

then A4: F # x is convergent by A2;

(R_EAL F) # x = F # x by MESFUN7C:1;

hence (R_EAL F) # x is convergent by A4, RINFSUP2:14; :: thesis: verum

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

then A4: F # x is convergent by A2;

(R_EAL F) # x = F # x by MESFUN7C:1;

hence (R_EAL F) # x is convergent by A4, RINFSUP2:14; :: thesis: verum

hence (lim F) | D = lim (F || D) by A1, A3, MESFUNC9:19; :: thesis: verum