let D be non empty set ; :: thesis:
let Y be RealNormSpace; :: thesis:
let H be Functional_Sequence of D, the carrier of Y; :: thesis:
let X be set ; :: thesis:
thus ( H is_point_conv_on X implies ( X common_on_dom H & ex f being PartFunc of D, the carrier of Y st
( X = dom f & ( for x being Element of D st x in X holds
( H # x is convergent & lim (H # x) = f . x ) ) ) ) ) :: thesis:

assume A1: H is_point_conv_on X ; :: thesis:
hence X common_on_dom H ; :: thesis:
consider f being PartFunc of D, the carrier of Y such that
A2: X = dom f and
A3: 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 A1;
take f ; :: thesis:
thus X = dom f by A2; :: thesis:
let x be Element of D; :: thesis:
assume A4: x in X ; :: thesis:
then X4: f /. x = f . x by A2, PARTFUN1:def 6;

let p be Real; :: thesis:
assume A6: p > 0 ; :: thesis:
consider k being Nat such that
A7: for n being Nat st n >= k holds
||.(((H . n) /. x) - (f /. x)).|| < p by A3, A4, A6;
take k = k; :: thesis:
let n be Nat; :: thesis:
assume n >= k ; :: thesis:
then ||.(((H . n) /. x) - (f /. x)).|| < p by A7;
hence ||.(((H # x) . n) - (f /. x)).|| < p by Def10; :: thesis:

end;

end;

assume A8: X common_on_dom H ; :: thesis:
given f being PartFunc of D, the carrier of Y such that A9: X = dom f and
A10: for x being Element of D st x in X holds
( H # x is convergent & lim (H # x) = f . x ) ; :: thesis:
ex f being PartFunc of D, the carrier of Y st
( 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 Nat st
for n being Nat st n >= k holds
||.(((H . n) /. x) - (f /. x)).|| < p ) )

take f ; :: thesis:
thus X = dom f by A9; :: thesis:
let x be Element of D; :: thesis:
assume X10: x in X ; :: thesis:
then A11: ( H # x is convergent & lim (H # x) = f . x ) by A10;
X11: f /. x = f . x by PARTFUN1:def 6, X10, A9;
let p be Real; :: thesis:
assume p > 0 ; :: thesis:
then consider k being Nat such that
A12: for n being Nat st n >= k holds
||.(((H # x) . n) - (f /. x)).|| < p by A11, NORMSP_1:def 7, X11;
take k ; :: thesis:
let n be Nat; :: thesis:
assume n >= k ; :: thesis:
then ||.(((H # x) . n) - (f /. x)).|| < p by A12;
hence ||.(((H . n) /. x) - (f /. x)).|| < p by Def10; :: thesis:

end;