let D be non empty set ; :: thesis: for H being Functional_Sequence of D,REAL
for Y, X 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 Y, X 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 Y, X 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 A1: ( Y c= X & Y <> {} & H is_point_conv_on X ) ; :: thesis: ( H is_point_conv_on Y & (lim H,X) | Y = lim H,Y )
then X common_on_dom H by Def12;
then A2: Y common_on_dom H by A1, Th24;
consider f being PartFunc of D, REAL such that
A3: ( X = dom f & ( for x being Element of D st x in X holds
for p being Real st p > 0 holds
ex k being Element of NAT st
for n being Element of NAT st n >= k holds
abs (((H . n) . x) - (f . x)) < p ) ) by A1, Def12;

now

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 Element of NAT st
for n being Element of NAT st n >= k holds
abs (((H . n) . x) - (g . x)) < p ) )
thus A4: Y = dom g by A1, A3, RELAT_1:91; :: thesis: for x being Element of D st x in Y holds
for p being Real st p > 0 holds
ex k being Element of NAT st
for n being Element of NAT st n >= k holds
abs (((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 Element of NAT st
for n being Element of NAT st n >= k holds
abs (((H . n) . x) - (g . x)) < p )
assume A5: x in Y ; :: thesis: for p being Real st p > 0 holds
ex k being Element of NAT st
for n being Element of NAT st n >= k holds
abs (((H . n) . x) - (g . x)) < p
let p be Real; :: thesis: ( p > 0 implies ex k being Element of NAT st
for n being Element of NAT st n >= k holds
abs (((H . n) . x) - (g . x)) < p )
assume p > 0 ; :: thesis: ex k being Element of NAT st
for n being Element of NAT st n >= k holds
abs (((H . n) . x) - (g . x)) < p
then consider k being Element of NAT such that
A6: for n being Element of NAT st n >= k holds
abs (((H . n) . x) - (f . x)) < p by A1, A3, A5;
take k = k; :: thesis: for n being Element of NAT st n >= k holds
abs (((H . n) . x) - (g . x)) < p
let n be Element of NAT ; :: thesis: ( n >= k implies abs (((H . n) . x) - (g . x)) < p )
assume n >= k ; :: thesis: abs (((H . n) . x) - (g . x)) < p
then abs (((H . n) . x) - (f . x)) < p by A6;
hence abs (((H . n) . x) - (g . x)) < p by A4, A5, FUNCT_1:68; :: thesis: verum

end;

hence A7: H is_point_conv_on Y by A2, Def12; :: thesis: (lim H,X) | Y = lim H,Y
dom (lim H,X) = X by A1, Def14;
then (dom (lim H,X)) /\ Y = Y by A1, XBOOLE_1:28;
then dom ((lim H,X) | Y) = Y by RELAT_1:90;
then A8: dom ((lim H,X) | Y) = dom (lim H,Y) by A7, Def14;

now

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 A9: x in dom ((lim H,X) | Y) ; :: thesis: ((lim H,X) | Y) . x = (lim H,Y) . x
then x in (dom (lim H,X)) /\ Y by RELAT_1:90;
then A10: ( x in dom (lim H,X) & x in Y ) by XBOOLE_0:def 4;
then A11: x in dom (lim H,Y) by A7, Def14;
thus ((lim H,X) | Y) . x = (lim H,X) . x by A9, FUNCT_1:68
.= lim (H # x) by A1, A10, Def14
.= (lim H,Y) . x by A7, A11, Def14 ; :: thesis: verum

end;

hence (lim H,X) | Y = lim H,Y by A8, PARTFUN1:34; :: thesis: verum