:: deftheorem defines indexp MOEBIUS3:def 5 :
for n being Nat holds indexp n = card (SetPrimes n);