theorem Th36: :: NUMBER15:36
for n being Nat holds { k where k is Nat : k divides 5 |^ n } = divisors ((5 |^ n),4,1)