:: deftheorem Def1 defines ,... WAYBEL17:def 1 :
for S being non empty set
for a, b being Element of S
for b₄ being sequence of S holds
( b₄ = (a,b) ,... iff for i being Element of NAT holds
( ( ex k being Element of NAT st i = 2 * k implies b₄ . i = a ) & ( ( for k being Element of NAT holds not i = 2 * k ) implies b₄ . i = b ) ) );