theorem :: RING_3:95

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