:: deftheorem Def1 defines Rascal NEWTON07:def 3 :
for n being natural Number
for b₂ being FinSequence holds
( b₂ = Rascal n iff ( dom b₂ = Seg (n + 1) & ( for i being Nat st i in dom b₂ holds
b₂ . i = ((i - 1) * ((n + 1) - i)) + 1 ) ) );