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
A1: 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 A4: dom (G . 0) = D by A1, RELAT_1:62;
A5: dom ((lim F) | D) = (dom (lim F)) /\ D by RELAT_1:61;
then dom ((lim F) | D) = (dom (F . 0)) /\ D by MESFUNC8:def 9;
then dom ((lim F) | D) = D by A1, XBOOLE_1:28;
then A6: dom ((lim F) | D) = dom (lim G) by A4, MESFUNC8:def 9;

now :: thesis: for x being Element of X st x in dom ((lim F) | D) holds
(lim G) . x = ((lim F) | D) . x

let x be Element of X; :: thesis: ( x in dom ((lim F) | D) implies (lim G) . b₁ = ((lim F) | D) . b₁ )
assume A7: x in dom ((lim F) | D) ; :: thesis: (lim G) . b₁ = ((lim F) | D) . b₁
then A8: ((lim F) | D) . x = (lim F) . x by FUNCT_1:47;
x in dom (lim F) by A5, A7, XBOOLE_0:def 4;
then A9: ((lim F) | D) . x = lim (F # x) by A8, MESFUNC8:def 9;
A10: x in D by A7, RELAT_1:57;
then A11: 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 A11;

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

then G # x is convergent_to_+infty by A2, A10, Th12;
then lim (G # x) = +infty by Th7;
then (lim G) . x = +infty by A6, A7, MESFUNC8:def 9;
hence (lim G) . x = ((lim F) | D) . x by A9, A12, Th7; :: thesis: verum

end;

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

then G # x is convergent_to_-infty by A2, A10, Th12;
then lim (G # x) = -infty by Th7;
then (lim G) . x = -infty by A6, A7, MESFUNC8:def 9;
hence (lim G) . x = ((lim F) | D) . x by A9, A13, Th7; :: thesis: verum

end;

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

then consider g being Real such that
A15: lim (F # x) = g and
A16: for p being Real 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 Th7;

A17: now :: thesis: for p being Real st 0 < p holds
ex n being Nat st
for m being Nat st n <= m holds
|.(((G # x) . m) - g).| < p

let p be Real; :: thesis: ( 0 < p implies ex n being Nat st
for m being Nat st n <= m holds
|.(((G # x) . m) - g).| < p )
assume 0 < p ; :: thesis: ex n being Nat st
for m being Nat st n <= m holds
|.(((G # x) . m) - g).| < p
then consider n being Nat such that
A18: for m being Nat st n <= m holds
|.(((F # x) . m) - (lim (F # x))).| < p by A16;
take n = n; :: thesis: for m being Nat st n <= m holds
|.(((G # x) . m) - g).| < p
let m be Nat; :: thesis: ( n <= m implies |.(((G # x) . m) - g).| < p )
(F # x) . m = (F . m) . x by MESFUNC5:def 13;
then (F # x) . m = ((F . m) | D) . x by A10, FUNCT_1:49;
then A19: (F # x) . m = (G . m) . x by A2;
assume n <= m ; :: thesis: |.(((G # x) . m) - g).| < p
then |.(((F # x) . m) - (lim (F # x))).| < p by A18;
hence |.(((G # x) . m) - g).| < p by A15, A19, MESFUNC5:def 13; :: thesis: verum

end;

reconsider g = g as R_eal by XXREAL_0:def 1;
A20: G # x is convergent_to_finite_number by A2, A10, A14, Th12;
then G # x is convergent ;
then lim (G # x) = g by A17, A20, MESFUNC5:def 12;
hence (lim G) . x = ((lim F) | D) . x by A6, A7, A9, A15, MESFUNC8:def 9; :: thesis: verum

end;

end;

end;

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