:: deftheorem Def5 defines dblseq_ex_1 CARDFIL4:def 8 :
for b₁ being Function of [:NAT,NAT:],REAL holds
( b₁ = dblseq_ex_1 iff for m, n being Nat holds b₁ . (m,n) = 1 / (m + 1) );