:: deftheorem MerDef defines Mersenne_sequence NUMBER18:def 9 :
for b₁ being sequence of NAT holds
( b₁ = Mersenne_sequence iff for n being Element of NAT holds b₁ . n = Mersenne n );