:: deftheorem defines is_unif_conv_on SEQFUNC:def 12 :
for D being non empty set
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 & ex f being PartFunc of D,REAL st
( X = dom f & ( 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 ) ) ) );