let D be non empty set ; :: thesis: for Y being RealNormSpace
for H being Functional_Sequence of D, the carrier of Y
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 Nat st
for n being Nat
for x being Element of D st n >= k & x in X holds
||.(((H . n) /. x) - ((lim (H,X)) /. x)).|| < r ) ) )
let Y be RealNormSpace; :: thesis: for H being Functional_Sequence of D, the carrier of Y
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 Nat st
for n being Nat
for x being Element of D st n >= k & x in X holds
||.(((H . n) /. x) - ((lim (H,X)) /. x)).|| < r ) ) )
let H be Functional_Sequence of D, the carrier of Y; :: 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 Nat st
for n being Nat
for x being Element of D st n >= k & x in X holds
||.(((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 Nat st
for n being Nat
for x being Element of D st n >= k & x in X holds
||.(((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 Nat st
for n being Nat
for x being Element of D st n >= k & x in X holds
||.(((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 Nat st
for n being Nat
for x being Element of D st n >= k & x in X holds
||.(((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 Nat st
for n being Nat
for x being Element of D st n >= k & x in X holds
||.(((H . n) /. x) - ((lim (H,X)) /. x)).|| < r ) )
then consider f being PartFunc of D, the carrier of Y such that
A2: X = dom f and
A3: 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 ;
thus X common_on_dom H by A1; :: thesis: ( H is_point_conv_on X & ( for r being Real st 0 < r 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) - ((lim (H,X)) /. x)).|| < r ) )

A4: now :: 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 A3;
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;

thus H is_point_conv_on X by A1, Th21; :: thesis: for r being Real st 0 < r 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) - ((lim (H,X)) /. x)).|| < r
then A7: f = lim (H,X) by A2, A4, Th20;
let r be Real; :: thesis: ( 0 < r implies 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) - ((lim (H,X)) /. x)).|| < r )
assume r > 0 ; :: thesis: 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) - ((lim (H,X)) /. x)).|| < r
then consider k being Nat such that
A8: for n being Nat
for x being Element of D st n >= k & x in X holds
||.(((H . n) /. x) - (f /. x)).|| < r by A3;
take k ; :: thesis: for n being Nat
for x being Element of D st n >= k & x in X holds
||.(((H . n) /. x) - ((lim (H,X)) /. x)).|| < r
let n be Nat; :: thesis: for x being Element of D st n >= k & x in X holds
||.(((H . n) /. x) - ((lim (H,X)) /. x)).|| < r
let x be Element of D; :: thesis: ( n >= k & x in X implies ||.(((H . n) /. x) - ((lim (H,X)) /. x)).|| < r )
assume ( n >= k & x in X ) ; :: thesis: ||.(((H . n) /. x) - ((lim (H,X)) /. x)).|| < r
hence ||.(((H . n) /. x) - ((lim (H,X)) /. x)).|| < r by A7, A8; :: thesis: verum

end;

assume that
A9: X common_on_dom H and
A10: H is_point_conv_on X and
A11: for r being Real st 0 < r 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) - ((lim (H,X)) /. x)).|| < r ; :: thesis: H is_unif_conv_on X
dom (lim (H,X)) = X by A10, Def13;
hence H is_unif_conv_on X by A9, A11; :: thesis: verum