for n being non zero Nat holds Radical (Radical n) = Radical n by Th57;