:: deftheorem defines is_uniformly_convergent_to MESFUN9C:def 7 :
for X being set
for F being Functional_Sequence of X,COMPLEX
for f being PartFunc of X,COMPLEX holds
( F is_uniformly_convergent_to f iff ( F is with_the_same_dom & dom (F . 0) = dom f & ( for e being Real st e > 0 holds
ex N being Nat st
for n being Nat
for x being Element of X st n >= N & x in dom (F . 0) holds
|.(((F . n) . x) - (f . x)).| < e ) ) );