:: deftheorem defines uniformly_convergent_in_cod1 DBLSEQ_1:def 9 :
for Rseq being Function of [:NAT,NAT:],REAL holds
( Rseq is uniformly_convergent_in_cod1 iff ( Rseq is convergent_in_cod1 & ( for e being Real st e > 0 holds
ex M being Nat st
for m being Nat st m >= M holds
for n being Nat holds |.((Rseq . (n,m)) - ((lim_in_cod1 Rseq) . n)).| < e ) ) );