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

proof

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;

for n being Nat holds (R_EAL (F || D)) . n = ((R_EAL F) . n) | D by Def1;
hence (lim F) | D = lim (F || D) by A1, A3, MESFUNC9:19; :: thesis: verum