:: deftheorem DivsDef defines Divs NUMBER18:def 4 :
for b₁ being sequence of NAT holds
( b₁ = Divs iff for n being Element of NAT holds b₁ . n = #divs n );