:: deftheorem Def8 defines <* FINSEQ_1:def 8 :
for x being object
for b₂ being Function holds
( b₂ = <*x*> iff ( dom b₂ = Seg 1 & b₂ . 1 = x ) );