:: deftheorem defines uniformly_convergent_in_cod2 DBLSEQ_1:def 10 :
for Rseq being Function of [:NAT,NAT:],REAL holds
( Rseq is uniformly_convergent_in_cod2 iff ( Rseq is convergent_in_cod2 & ( for e being Real st e > 0 holds
ex N being Nat st
for n being Nat st n >= N holds
for m being Nat holds |.((Rseq . (n,m)) - ((lim_in_cod2 Rseq) . m)).| < e ) ) );