:: deftheorem defines Sierp53Seq NUMBER18:def 5 :
for k being Nat holds Sierp53Seq k = ArProg ((2 |^ (k -' 1)),(2 |^ k));