set K = PrimeField F;
thus the carrier of (PrimeField F) = the carrier of (Image (canHom_Rat (PrimeField F))) by EC_PF_1:def 2
.= rng (canHom_Rat (PrimeField F)) by RING_2:def 6 ; :: according to FUNCT_2:def 3 :: thesis: verum