let D be non empty set ; :: thesis: for H being Functional_Sequence of D,REAL
for X, Y being set st Y c= X & Y <> {} & H is_point_conv_on X holds
( H is_point_conv_on Y & (lim (H,X)) | Y = lim (H,Y) )
let H be Functional_Sequence of D,REAL; :: thesis: for X, Y being set st Y c= X & Y <> {} & H is_point_conv_on X holds
( H is_point_conv_on Y & (lim (H,X)) | Y = lim (H,Y) )
let X, Y be set ; :: thesis: ( Y c= X & Y <> {} & H is_point_conv_on X implies ( H is_point_conv_on Y & (lim (H,X)) | Y = lim (H,Y) ) )
assume that
A1: Y c= X and
A2: Y <> {} and
A3: H is_point_conv_on X ; :: thesis: ( H is_point_conv_on Y & (lim (H,X)) | Y = lim (H,Y) )
consider f being PartFunc of D,REAL such that
A4: X = dom f and
A5: for x being Element of D st x in X holds
for p being Real st p > 0 holds
ex k being Nat st
for n being Nat st n >= k holds
|.(((H . n) . x) - (f . x)).| < p by A3;

A6: now :: thesis: ex g being Element of bool [:D,REAL:] st
( Y = dom g & ( for x being Element of D st x in Y holds
for p being Real st p > 0 holds
ex k being Nat st
for n being Nat st n >= k holds
|.(((H . n) . x) - (g . x)).| < p ) )

take g = f | Y; :: thesis: ( Y = dom g & ( for x being Element of D st x in Y holds
for p being Real st p > 0 holds
ex k being Nat st
for n being Nat st n >= k holds
|.(((H . n) . x) - (g . x)).| < p ) )
thus A7: Y = dom g by A1, A4, RELAT_1:62; :: thesis: for x being Element of D st x in Y holds
for p being Real st p > 0 holds
ex k being Nat st
for n being Nat st n >= k holds
|.(((H . n) . x) - (g . x)).| < p
let x be Element of D; :: thesis: ( x in Y implies for p being Real st p > 0 holds
ex k being Nat st
for n being Nat st n >= k holds
|.(((H . n) . x) - (g . x)).| < p )
assume A8: x in Y ; :: thesis: for p being Real st p > 0 holds
ex k being Nat st
for n being Nat st n >= k holds
|.(((H . n) . x) - (g . x)).| < p
let p be Real; :: thesis: ( p > 0 implies ex k being Nat st
for n being Nat st n >= k holds
|.(((H . n) . x) - (g . x)).| < p )
assume p > 0 ; :: thesis: ex k being Nat st
for n being Nat st n >= k holds
|.(((H . n) . x) - (g . x)).| < p
then consider k being Nat such that
A9: for n being Nat st n >= k holds
|.(((H . n) . x) - (f . x)).| < p by A1, A5, A8;
take k = k; :: thesis: for n being Nat st n >= k holds
|.(((H . n) . x) - (g . x)).| < p
let n be Nat; :: thesis: ( n >= k implies |.(((H . n) . x) - (g . x)).| < p )
assume n >= k ; :: thesis: |.(((H . n) . x) - (g . x)).| < p
then |.(((H . n) . x) - (f . x)).| < p by A9;
hence |.(((H . n) . x) - (g . x)).| < p by A7, A8, FUNCT_1:47; :: thesis: verum

end;

X common_on_dom H by A3;
then Y common_on_dom H by A1, A2, Th22;
hence A10: H is_point_conv_on Y by A6; :: thesis: (lim (H,X)) | Y = lim (H,Y)

A11: now :: thesis: for x being Element of D st x in dom ((lim (H,X)) | Y) holds
((lim (H,X)) | Y) . x = (lim (H,Y)) . x

let x be Element of D; :: thesis: ( x in dom ((lim (H,X)) | Y) implies ((lim (H,X)) | Y) . x = (lim (H,Y)) . x )
assume A12: x in dom ((lim (H,X)) | Y) ; :: thesis: ((lim (H,X)) | Y) . x = (lim (H,Y)) . x
then A13: x in (dom (lim (H,X))) /\ Y by RELAT_1:61;
then A14: x in dom (lim (H,X)) by XBOOLE_0:def 4;
x in Y by A13, XBOOLE_0:def 4;
then A15: x in dom (lim (H,Y)) by A10, Def13;
thus ((lim (H,X)) | Y) . x = (lim (H,X)) . x by A12, FUNCT_1:47
.= lim (H # x) by A3, A14, Def13
.= (lim (H,Y)) . x by A10, A15, Def13 ; :: thesis: verum

end;

dom (lim (H,X)) = X by A3, Def13;
then (dom (lim (H,X))) /\ Y = Y by A1, XBOOLE_1:28;
then dom ((lim (H,X)) | Y) = Y by RELAT_1:61;
then dom ((lim (H,X)) | Y) = dom (lim (H,Y)) by A10, Def13;
hence (lim (H,X)) | Y = lim (H,Y) by A11, PARTFUN1:5; :: thesis: verum