let D be non empty set ; :: thesis: for Z being set
for Y being RealNormSpace
for H being Functional_Sequence of D, the carrier of Y
for X being set st Z c= X & Z <> {} & H is_point_conv_on X holds
( H is_point_conv_on Z & (lim (H,X)) | Z = lim (H,Z) )
let Z be set ; :: thesis: for Y being RealNormSpace
for H being Functional_Sequence of D, the carrier of Y
for X being set st Z c= X & Z <> {} & H is_point_conv_on X holds
( H is_point_conv_on Z & (lim (H,X)) | Z = lim (H,Z) )
let Y be RealNormSpace; :: thesis: for H being Functional_Sequence of D, the carrier of Y
for X being set st Z c= X & Z <> {} & H is_point_conv_on X holds
( H is_point_conv_on Z & (lim (H,X)) | Z = lim (H,Z) )
let H be Functional_Sequence of D, the carrier of Y; :: thesis: for X being set st Z c= X & Z <> {} & H is_point_conv_on X holds
( H is_point_conv_on Z & (lim (H,X)) | Z = lim (H,Z) )
let X be set ; :: thesis: ( Z c= X & Z <> {} & H is_point_conv_on X implies ( H is_point_conv_on Z & (lim (H,X)) | Z = lim (H,Z) ) )
assume that
A1: Z c= X and
A2: Z <> {} and
A3: H is_point_conv_on X ; :: thesis: ( H is_point_conv_on Z & (lim (H,X)) | Z = lim (H,Z) )
consider f being PartFunc of D, the carrier of Y 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;

now :: thesis: ex g being Element of K16(K17(D, the carrier of Y)) st
( Z = dom g & ( for x being Element of D st x in Z 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 | Z; :: thesis: ( Z = dom g & ( for x being Element of D st x in Z 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: Z = dom g by A1, A4, RELAT_1:62; :: thesis: for x being Element of D st x in Z 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 Z 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 Z ; :: 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
then X8: f /. x = f . x by A1, A4, PARTFUN1:def 6;
g /. x = g . x by A7, A8, PARTFUN1:def 6;
then X10: g /. x = f /. x by A7, A8, FUNCT_1:47, X8;
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
hence ||.(((H . n) /. x) - (g /. x)).|| < p by A9, X10; :: thesis: verum

end;

hence A10: H is_point_conv_on Z by A1, A2, A3, Th22; :: thesis: (lim (H,X)) | Z = lim (H,Z)

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

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

end;

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