:: deftheorem Def3 defines der_seq CARDFIN2:def 3 :
for b₁ being sequence of INT holds
( b₁ = der_seq iff ( b₁ . 0 = 1 & b₁ . 1 = 0 & ( for n being Nat holds b₁ . (n + 2) = (n + 1) * ((b₁ . n) + (b₁ . (n + 1))) ) ) );