:: deftheorem Def4 defines <% ALGSEQ_1:def 5 :
for R being non empty ZeroStr
for x being Element of R
for b₃ being AlgSequence of R holds
( b₃ = <%x%> iff ( len b₃ <= 1 & b₃ . 0 = x ) );