:: deftheorem Def4 defines <% AFINSQ_1:def 4 :
for x being object
for b₂ being Function holds
( b₂ = <%x%> iff ( dom b₂ = 1 & b₂ . 0 = x ) );