theorem Krzys1: :: MOEBIUS3:42

for n being Nat holds indexp n <= n