let D be non empty set ; for H being Functional_Sequence of D,REAL
for X being set holds
( H is_point_conv_on X iff ( X common_on_dom H & ex f being PartFunc of D,REAL st
( X = dom f & ( for x being Element of D st x in X holds
( H # x is convergent & lim (H # x) = f . x ) ) ) ) )
let H be Functional_Sequence of D,REAL; for X being set holds
( H is_point_conv_on X iff ( X common_on_dom H & ex f being PartFunc of D,REAL st
( X = dom f & ( for x being Element of D st x in X holds
( H # x is convergent & lim (H # x) = f . x ) ) ) ) )
let X be set ; ( H is_point_conv_on X iff ( X common_on_dom H & ex f being PartFunc of D,REAL st
( X = dom f & ( for x being Element of D st x in X holds
( H # x is convergent & lim (H # x) = f . x ) ) ) ) )
thus
( H is_point_conv_on X implies ( X common_on_dom H & ex f being PartFunc of D,REAL st
( X = dom f & ( for x being Element of D st x in X holds
( H # x is convergent & lim (H # x) = f . x ) ) ) ) )
( X common_on_dom H & ex f being PartFunc of D,REAL st
( X = dom f & ( for x being Element of D st x in X holds
( H # x is convergent & lim (H # x) = f . x ) ) ) implies H is_point_conv_on X )
assume A8:
X common_on_dom H
; ( for f being PartFunc of D,REAL holds
( not X = dom f or ex x being Element of D st
( x in X & not ( H # x is convergent & lim (H # x) = f . x ) ) ) or H is_point_conv_on X )
given f being PartFunc of D,REAL 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 )
; H is_point_conv_on X
ex f being PartFunc of D,REAL 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 ) )
hence
H is_point_conv_on X
by A8; verum