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