let D be non empty set ; :: thesis: for H being Functional_Sequence of D,REAL
for X being set st H is_unif_conv_on X holds
H is_point_conv_on X
let H be Functional_Sequence of D,REAL; :: thesis: for X being set st H is_unif_conv_on X holds
H is_point_conv_on X
let X be set ; :: thesis: ( H is_unif_conv_on X implies H is_point_conv_on X )
assume A1: H is_unif_conv_on X ; :: thesis: H is_point_conv_on X

A2: now :: thesis: 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 ) )

consider f being PartFunc of D,REAL such that
A3: X = dom f and
A4: for p being Real st p > 0 holds
ex k being Nat st
for n being Nat
for x being Element of D st n >= k & x in X holds
|.(((H . n) . x) - (f . x)).| < p by A1;
take f = 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 Nat st
for n being Nat st n >= k holds
|.(((H . n) . x) - (f . x)).| < p ) )
thus X = dom f by A3; :: thesis: 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
let x be Element of D; :: thesis: ( x in X 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) - (f . x)).| < p )
assume A5: x in X ; :: 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) - (f . x)).| < p
let p be Real; :: thesis: ( p > 0 implies ex k being Nat st
for n being Nat st n >= k holds
|.(((H . n) . x) - (f . x)).| < p )
assume p > 0 ; :: thesis: ex k being Nat st
for n being Nat st n >= k holds
|.(((H . n) . x) - (f . x)).| < p
then consider k being Nat such that
A6: for n being Nat
for x being Element of D st n >= k & x in X holds
|.(((H . n) . x) - (f . x)).| < p by A4;
take k = k; :: thesis: for n being Nat st n >= k holds
|.(((H . n) . x) - (f . x)).| < p
let n be Nat; :: thesis: ( n >= k implies |.(((H . n) . x) - (f . x)).| < p )
assume n >= k ; :: thesis: |.(((H . n) . x) - (f . x)).| < p
hence |.(((H . n) . x) - (f . x)).| < p by A5, A6; :: thesis: verum

end;

X common_on_dom H by A1;
hence H is_point_conv_on X by A2; :: thesis: verum