theorem :: NAT_5:40

for n0 being non zero Nat holds Sum (Euler_phi | (NatDivisors n0)) = n0