let p be Prime; :: thesis: for F being Field holds
( Char F = p iff PrimeField F, Z/ p are_isomorphic )
let F be Field; :: thesis: ( Char F = p iff PrimeField F, Z/ p are_isomorphic )

A1: now :: thesis: ( Char F = p implies PrimeField F, Z/ p are_isomorphic )

assume Char F = p ; :: thesis: PrimeField F, Z/ p are_isomorphic
then F is p -characteristic ;
hence PrimeField F, Z/ p are_isomorphic by Th107; :: thesis: verum

end;

now :: thesis: ( PrimeField F, Z/ p are_isomorphic implies Char F = p )

assume PrimeField F, Z/ p are_isomorphic ; :: thesis: Char F = p
then ex f being Function of (Z/ p),(PrimeField F) st f is RingIsomorphism by QUOFIELD:def 23;
then PrimeField F is Z/ p -isomorphic ;
then A2: PrimeField F is p -characteristic ;
PrimeField F is Subring of F by Lm1;
hence Char F = p by A2, Th88; :: thesis: verum

end;

hence ( Char F = p iff PrimeField F, Z/ p are_isomorphic ) by A1; :: thesis: verum