:: deftheorem Def4 defines F_dp1 DIOPHAN1:def 2 :
for t being 1 _greater Nat
for a being Real
for b₃ being FinSequence of Segm t holds
( b₃ = F_dp1 (t,a) iff ( len b₃ = t + 1 & ( for i being Nat st i in dom b₃ holds
b₃ . i = [\((frac ((i - 1) * a)) * t)/] ) ) );