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 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 Element of NAT st
for n being Element of NAT st n >= k holds
abs (((H . n) . x) - (f . x)) < p by A3, Def12;

A6: 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 A7: Y = dom g by A1, A4, 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 A8: 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
A9: for n being Element of NAT st n >= k holds
abs (((H . n) . x) - (f . x)) < p by A1, A5, A8;
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 A9;
hence abs (((H . n) . x) - (g . x)) < p by A7, A8, FUNCT_1:70; :: thesis: verum

end;

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

A11: 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 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:90;
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, Def14;
thus ((lim H,X) | Y) . x = (lim H,X) . x by A12, FUNCT_1:70
.= lim (H # x) by A3, A14, Def14
.= (lim H,Y) . x by A10, A15, Def14 ; :: thesis: verum

end;

dom (lim H,X) = X by A3, 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 dom ((lim H,X) | Y) = dom (lim H,Y) by A10, Def14;
hence (lim H,X) | Y = lim H,Y by A11, PARTFUN1:34; :: thesis: verum