:: deftheorem Def11 defines Ser SUPINF_2:def 10 :
for N, b₂ being sequence of ExtREAL holds
( b₂ = Ser N iff ( b₂ . 0 = N . 0 & ( for n being Nat
for y being R_eal st y = b₂ . n holds
b₂ . (n + 1) = y + (N . (n + 1)) ) ) );