let D be non empty set ; :: thesis: for H being Functional_Sequence of D,REAL
for X being set holds
( H is_unif_conv_on X iff ( X common_on_dom H & H is_point_conv_on X & ( for r being Real st 0 < r holds
ex k being Element of NAT st
for n being Element of NAT
for x being Element of D st n >= k & x in X holds
abs (((H . n) . x) - ((lim H,X) . x)) < r ) ) )
let H be Functional_Sequence of D,REAL ; :: thesis: for X being set holds
( H is_unif_conv_on X iff ( X common_on_dom H & H is_point_conv_on X & ( for r being Real st 0 < r holds
ex k being Element of NAT st
for n being Element of NAT
for x being Element of D st n >= k & x in X holds
abs (((H . n) . x) - ((lim H,X) . x)) < r ) ) )
let X be set ; :: thesis: ( H is_unif_conv_on X iff ( X common_on_dom H & H is_point_conv_on X & ( for r being Real st 0 < r holds
ex k being Element of NAT st
for n being Element of NAT
for x being Element of D st n >= k & x in X holds
abs (((H . n) . x) - ((lim H,X) . x)) < r ) ) )
thus ( H is_unif_conv_on X implies ( X common_on_dom H & H is_point_conv_on X & ( for r being Real st 0 < r holds
ex k being Element of NAT st
for n being Element of NAT
for x being Element of D st n >= k & x in X holds
abs (((H . n) . x) - ((lim H,X) . x)) < r ) ) ) :: thesis: ( X common_on_dom H & H is_point_conv_on X & ( for r being Real st 0 < r holds
ex k being Element of NAT st
for n being Element of NAT
for x being Element of D st n >= k & x in X holds
abs (((H . n) . x) - ((lim H,X) . x)) < r ) implies H is_unif_conv_on X )

proof

assume A1: H is_unif_conv_on X ; :: thesis: ( X common_on_dom H & H is_point_conv_on X & ( for r being Real st 0 < r holds
ex k being Element of NAT st
for n being Element of NAT
for x being Element of D st n >= k & x in X holds
abs (((H . n) . x) - ((lim H,X) . x)) < r ) )
then consider f being PartFunc of D,REAL such that
A2: ( X = dom f & ( for p being Real st p > 0 holds
ex k being Element of NAT st
for n being Element of NAT
for x being Element of D st n >= k & x in X holds
abs (((H . n) . x) - (f . x)) < p ) ) by Def13;

A3: now

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 A4: 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
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
A5: for n being Element of NAT
for x being Element of D st n >= k & x in X holds
abs (((H . n) . x) - (f . x)) < p by A2;
take k = 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
hence abs (((H . n) . x) - (f . x)) < p by A4, A5; :: thesis: verum

end;

thus X common_on_dom H by A1, Def13; :: thesis: ( H is_point_conv_on X & ( for r being Real st 0 < r holds
ex k being Element of NAT st
for n being Element of NAT
for x being Element of D st n >= k & x in X holds
abs (((H . n) . x) - ((lim H,X) . x)) < r ) )
thus H is_point_conv_on X by A1, Th23; :: thesis: for r being Real st 0 < r holds
ex k being Element of NAT st
for n being Element of NAT
for x being Element of D st n >= k & x in X holds
abs (((H . n) . x) - ((lim H,X) . x)) < r
then A6: f = lim H,X by A2, A3, Th22;
let r be Real; :: thesis: ( 0 < r implies ex k being Element of NAT st
for n being Element of NAT
for x being Element of D st n >= k & x in X holds
abs (((H . n) . x) - ((lim H,X) . x)) < r )
assume r > 0 ; :: thesis: ex k being Element of NAT st
for n being Element of NAT
for x being Element of D st n >= k & x in X holds
abs (((H . n) . x) - ((lim H,X) . x)) < r
then consider k being Element of NAT such that
A7: for n being Element of NAT
for x being Element of D st n >= k & x in X holds
abs (((H . n) . x) - (f . x)) < r by A2;
take k ; :: thesis: for n being Element of NAT
for x being Element of D st n >= k & x in X holds
abs (((H . n) . x) - ((lim H,X) . x)) < r
let n be Element of NAT ; :: thesis: for x being Element of D st n >= k & x in X holds
abs (((H . n) . x) - ((lim H,X) . x)) < r
let x be Element of D; :: thesis: ( n >= k & x in X implies abs (((H . n) . x) - ((lim H,X) . x)) < r )
assume ( n >= k & x in X ) ; :: thesis: abs (((H . n) . x) - ((lim H,X) . x)) < r
hence abs (((H . n) . x) - ((lim H,X) . x)) < r by A6, A7; :: thesis: verum

end;

assume A8: ( X common_on_dom H & H is_point_conv_on X & ( for r being Real st 0 < r holds
ex k being Element of NAT st
for n being Element of NAT
for x being Element of D st n >= k & x in X holds
abs (((H . n) . x) - ((lim H,X) . x)) < r ) ) ; :: thesis: H is_unif_conv_on X
then dom (lim H,X) = X by Def14;
hence H is_unif_conv_on X by A8, Def13; :: thesis: verum