let X be non empty set ; :: thesis: for F, G being Functional_Sequence of X,ExtREAL
for D being set st D c= dom (F . 0 ) & ( for n being Nat holds G . n = (F . n) | D ) & ( for x being Element of X st x in D holds
F # x is convergent ) holds
(lim F) | D = lim G
let F, G be Functional_Sequence of X,ExtREAL ; :: thesis: for D being set st D c= dom (F . 0 ) & ( for n being Nat holds G . n = (F . n) | D ) & ( for x being Element of X st x in D holds
F # x is convergent ) holds
(lim F) | D = lim G
let D be set ; :: thesis: ( D c= dom (F . 0 ) & ( for n being Nat holds G . n = (F . n) | D ) & ( for x being Element of X st x in D holds
F # x is convergent ) implies (lim F) | D = lim G )
assume that
A4: D c= dom (F . 0 ) and
A2: for n being Nat holds G . n = (F . n) | D and
A3: for x being Element of X st x in D holds
F # x is convergent ; :: thesis: (lim F) | D = lim G
G . 0 = (F . 0 ) | D by A2;
then L2: dom (G . 0 ) = D by A4, RELAT_1:91;
L43: dom ((lim F) | D) = (dom (lim F)) /\ D by RELAT_1:90;
then dom ((lim F) | D) = (dom (F . 0 )) /\ D by MESFUNC8:def 10;
then dom ((lim F) | D) = D by A4, XBOOLE_1:28;
then L41: dom ((lim F) | D) = dom (lim G) by L2, MESFUNC8:def 10;

now

let x be Element of X; :: thesis: ( x in dom ((lim F) | D) implies (lim G) . b₁ = ((lim F) | D) . b₁ )
assume L42: x in dom ((lim F) | D) ; :: thesis: (lim G) . b₁ = ((lim F) | D) . b₁
then L44: x in dom (lim F) by L43, XBOOLE_0:def 4;
((lim F) | D) . x = (lim F) . x by L42, FUNCT_1:70;
then L47: ((lim F) | D) . x = lim (F # x) by L44, MESFUNC8:def 10;
L46: x in D by L42, RELAT_1:86;
then L45: F # x is convergent by A3;

per cases ( F # x is convergent_to_+infty or F # x is convergent_to_-infty or F # x is convergent_to_finite_number ) by L45, MESFUNC5:def 11;

suppose B0: F # x is convergent_to_+infty ; :: thesis: (lim G) . b₁ = ((lim F) | D) . b₁

then G # x is convergent_to_+infty by A2, L46, Lm16;
then lim (G # x) = +infty by LIM;
then (lim G) . x = +infty by L41, L42, MESFUNC8:def 10;
hence (lim G) . x = ((lim F) | D) . x by L47, B0, LIM; :: thesis: verum

end;

suppose B0: F # x is convergent_to_-infty ; :: thesis: (lim G) . b₁ = ((lim F) | D) . b₁

then G # x is convergent_to_-infty by A2, L46, Lm16;
then lim (G # x) = -infty by LIM;
then (lim G) . x = -infty by L41, L42, MESFUNC8:def 10;
hence (lim G) . x = ((lim F) | D) . x by L47, B0, LIM; :: thesis: verum

end;

suppose B0: F # x is convergent_to_finite_number ; :: thesis: (lim G) . b₁ = ((lim F) | D) . b₁

then consider g being real number such that
B4: ( lim (F # x) = g & ( for p being real number st 0 < p holds
ex n being Nat st
for m being Nat st n <= m holds
|.(((F # x) . m) - (lim (F # x))).| < p ) ) by LIM;

B6: now

let p be real number ; :: thesis: ( 0 < p implies ex n being Nat st
for m being Nat st n <= m holds
|.(((G # x) . m) - (R_EAL g)).| < p )
assume 0 < p ; :: thesis: ex n being Nat st
for m being Nat st n <= m holds
|.(((G # x) . m) - (R_EAL g)).| < p
then consider n being Nat such that
C1: for m being Nat st n <= m holds
|.(((F # x) . m) - (lim (F # x))).| < p by B4;
take n = n; :: thesis: for m being Nat st n <= m holds
|.(((G # x) . m) - (R_EAL g)).| < p
let m be Nat; :: thesis: ( n <= m implies |.(((G # x) . m) - (R_EAL g)).| < p )
assume n <= m ; :: thesis: |.(((G # x) . m) - (R_EAL g)).| < p
then C2: |.(((F # x) . m) - (lim (F # x))).| < p by C1;
(F # x) . m = (F . m) . x by MESFUNC5:def 13;
then (F # x) . m = ((F . m) | D) . x by L46, FUNCT_1:72;
then (F # x) . m = (G . m) . x by A2;
hence |.(((G # x) . m) - (R_EAL g)).| < p by C2, B4, MESFUNC5:def 13; :: thesis: verum

end;

B5: G # x is convergent_to_finite_number by A2, L46, B0, Lm16;
then G # x is convergent by MESFUNC5:def 11;
then lim (G # x) = R_EAL g by B5, B6, MESFUNC5:def 12;
hence (lim G) . x = ((lim F) | D) . x by B4, L47, L41, L42, MESFUNC8:def 10; :: thesis: verum

end;

end;

end;

hence (lim F) | D = lim G by L41, PARTFUN1:34; :: thesis: verum