for F being Field holds PrimeField (PrimeField F) = PrimeField F by Th91;