:: deftheorem ds defines sequence FIELD_12:def 2 :
for b₁ being Function holds
( b₁ is sequence iff dom b₁ = NAT );