let D be non empty set ; :: thesis: 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 ; :: thesis: 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 ; :: thesis: ( 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 ) ) ) ) ) :: thesis: ( 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 )

proof

assume A1: H is_point_conv_on X ; :: thesis: ( 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 ) ) ) )
hence X common_on_dom H by Def12; :: thesis: 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 ) ) )
consider f being PartFunc of D,REAL such that
A2: ( 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;
take f ; :: thesis: ( X = dom f & ( for x being Element of D st x in X holds
( H # x is convergent & lim (H # x) = f . x ) ) )
thus X = dom f by A2; :: thesis: for x being Element of D st x in X holds
( H # x is convergent & lim (H # x) = f . x )
let x be Element of D; :: thesis: ( x in X implies ( H # x is convergent & lim (H # x) = f . x ) )
assume A3: x in X ; :: thesis: ( H # x is convergent & lim (H # x) = f . x )

A4: now

let p be real number ; :: thesis: ( p > 0 implies ex k being Element of NAT st
for n being Element of NAT st n >= k holds
abs (((H # x) . n) - (f . x)) < p )
A5: p is Real by XREAL_0:def 1;
assume p > 0 ; :: thesis: ex k being Element of NAT st
for n being Element of NAT st n >= k holds
abs (((H # x) . n) - (f . 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 A2, A3, A5;
take k = k; :: thesis: for n being Element of NAT st n >= k holds
abs (((H # x) . n) - (f . x)) < p
let n be Element of NAT ; :: thesis: ( n >= k implies abs (((H # x) . n) - (f . x)) < p )
assume n >= k ; :: thesis: abs (((H # x) . n) - (f . x)) < p
then abs (((H . n) . x) - (f . x)) < p by A6;
hence abs (((H # x) . n) - (f . x)) < p by Def11; :: thesis: verum

end;

hence H # x is convergent by SEQ_2:def 6; :: thesis: lim (H # x) = f . x
hence lim (H # x) = f . x by A4, SEQ_2:def 7; :: thesis: verum

end;

assume A7: X common_on_dom H ; :: thesis: ( 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 A8: ( X = dom f & ( for x being Element of D st x in X holds
( H # x is convergent & lim (H # x) = f . x ) ) ) ; :: thesis: 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 Element of NAT st
for n being Element of NAT st n >= k holds
abs (((H . n) . x) - (f . x)) < p ) )

proof

take f ; :: thesis: ( 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 ) )
thus X = dom f by A8; :: thesis: 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
let x be Element of D; :: thesis: ( x in X 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) - (f . x)) < p )
assume x in X ; :: 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) - (f . x)) < p
then A9: ( H # x is convergent & lim (H # x) = f . x ) by A8;
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) - (f . 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) - (f . x)) < p
then consider k being Element of NAT such that
A10: for n being Element of NAT st n >= k holds
abs (((H # x) . n) - (f . x)) < p by A9, SEQ_2:def 7;
take k ; :: thesis: for n being Element of NAT st n >= k holds
abs (((H . n) . x) - (f . x)) < p
let n be Element of NAT ; :: thesis: ( n >= k implies abs (((H . n) . x) - (f . x)) < p )
assume n >= k ; :: thesis: abs (((H . n) . x) - (f . x)) < p
then abs (((H # x) . n) - (f . x)) < p by A10;
hence abs (((H . n) . x) - (f . x)) < p by Def11; :: thesis: verum

end;

hence H is_point_conv_on X by A7, Def12; :: thesis: verum