let F be Field; :: thesis: ( Char F = 0 iff PrimeField F, F_Rat are_isomorphic )

A1: now :: thesis: ( Char F = 0 implies PrimeField F, F_Rat are_isomorphic )

assume Char F = 0 ; :: thesis: PrimeField F, F_Rat are_isomorphic
then F is 0 -characteristic ;
hence PrimeField F, F_Rat are_isomorphic by Th100; :: thesis: verum

end;

now :: thesis: ( PrimeField F, F_Rat are_isomorphic implies Char F = 0 )

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

end;

hence ( Char F = 0 iff PrimeField F, F_Rat are_isomorphic ) by A1; :: thesis: verum