let p be Prime; :: thesis: for F being p -characteristic Field holds Z/ p, PrimeField F are_isomorphic
let F be p -characteristic Field; :: thesis: Z/ p, PrimeField F are_isomorphic
take canHom_Z/ (p,(PrimeField F)) ; :: according to QUOFIELD:def 23 :: thesis: canHom_Z/ (p,(PrimeField F)) is isomorphism
thus canHom_Z/ (p,(PrimeField F)) is isomorphism ; :: thesis: verum