:: deftheorem Def1 defines Ant CALCUL_1:def 1 :
for D being non empty set
for f, b₃ being FinSequence of D holds
( ( len f > 0 implies ( b₃ = Ant f iff for i being Nat st len f = i + 1 holds
b₃ = f | (Seg i) ) ) & ( not len f > 0 implies ( b₃ = Ant f iff b₃ = {} ) ) );