:: deftheorem Def6 defines *--> FINSEQ_2:def 6 :
for a being set
for b₂ being sequence of ({a} *) holds
( b₂ = *--> a iff for n being Nat holds b₂ . n = n |-> a );