let F be strict Field; :: thesis:
thus ( not F is prime or F, F_Rat are_isomorphic or ex p being Prime st F, Z/ p are_isomorphic ) :: thesis:

assume A1: F is prime ; :: thesis:

per cases by Th85;

suppose Char F = 0 ; :: thesis:

then F is 0 -characteristic ;
then PrimeField F, F_Rat are_isomorphic by Th100;
hence ( F, F_Rat are_isomorphic or ex p being Prime st F, Z/ p are_isomorphic ) by EC_PF_1:def 2, A1; :: thesis:

end;

suppose Char F is prime ; :: thesis:

then consider p being Prime such that
A2: Char F = p ;
F is p -characteristic by A2;
then A3: PrimeField F, Z/ p are_isomorphic by Th107;
PrimeField F,F are_isomorphic by EC_PF_1:def 2, A1;
hence ( F, F_Rat are_isomorphic or ex p being Prime st F, Z/ p are_isomorphic ) by A3, Th43; :: thesis:

end;

end;

end;

assume A4: ( F, F_Rat are_isomorphic or ex p being Prime st F, Z/ p are_isomorphic ) ; :: thesis:

per cases by A4;

suppose F, F_Rat are_isomorphic ; :: thesis:

then consider f being Function of F,F_Rat such that
A5: f is RingIsomorphism ;
A6: F_Rat is F -isomorphic by A5;
then reconsider EK1 = F_Rat as F -homomorphic Field ;
reconsider f = f as Homomorphism of F,EK1 by A5;

let K be Field; :: thesis:
assume A7: K is strict Subfield of F ; :: thesis:
then reconsider EK = F_Rat as K -homomorphic Field by A6, Th56;
reconsider g = f | K as Homomorphism of K,EK by A7, Th57;
A8: Image g = F_Rat by EC_PF_1:def 2;
A9: the carrier of K c= the carrier of F by A7, EC_PF_1:def 1;

let x be object ; :: thesis:
assume x in the carrier of F ; :: thesis:
then reconsider a = x as Element of the carrier of F ;
f . a in Image g by A8;
then f . a in rng g by RING_2:def 6;
then consider y being object such that
A10: ( y in dom g & g . y = f . a ) by FUNCT_1:def 3;
reconsider y = y as Element of the carrier of K by A10;
A11: y in the carrier of F by A9;
(f | the carrier of K) . y = f . y by FUNCT_1:49;
then a = y by A10, A11, FUNCT_2:19;
hence x in the carrier of K ; :: thesis:

end;

then the carrier of F c= the carrier of K ;
then A12: the carrier of F = the carrier of K by A7, EC_PF_1:def 1;
( the addF of K = the addF of F || the carrier of K & the multF of K = the multF of F || the carrier of K & 1. F = 1. K & 0. F = 0. K ) by A7, EC_PF_1:def 1;
hence K = F by A7, A12; :: thesis:

end;

hence F is prime by EC_PF_1:def 2; :: thesis:

end;

suppose ex p being Prime st F, Z/ p are_isomorphic ; :: thesis:

then consider p being Prime such that
A13: F, Z/ p are_isomorphic ;
consider f being Function of F,(Z/ p) such that
A14: f is RingIsomorphism by A13;
A15: Z/ p is F -isomorphic by A14;
then reconsider EK1 = Z/ p as F -homomorphic Field ;
reconsider f = f as Homomorphism of F,EK1 by A14;

let K be Field; :: thesis:
assume A16: K is strict Subfield of F ; :: thesis:
then reconsider EK = Z/ p as K -homomorphic Field by A15, Th56;
reconsider g = f | K as Homomorphism of K,EK by A16, Th57;
A17: Image g = Z/ p by EC_PF_1:def 2;
A18: the carrier of K c= the carrier of F by A16, EC_PF_1:def 1;

let x be object ; :: thesis:
assume x in the carrier of F ; :: thesis:
then reconsider a = x as Element of the carrier of F ;
f . a in Image g by A17;
then f . a in rng g by RING_2:def 6;
then consider y being object such that
A19: ( y in dom g & g . y = f . a ) by FUNCT_1:def 3;
reconsider y = y as Element of the carrier of K by A19;
A20: y in the carrier of F by A18;
(f | the carrier of K) . y = f . y by FUNCT_1:49;
then a = y by A19, A20, FUNCT_2:19;
hence x in the carrier of K ; :: thesis:

end;

then the carrier of F c= the carrier of K ;
then A21: the carrier of F = the carrier of K by A16, EC_PF_1:def 1;
( the addF of K = the addF of F || the carrier of K & the multF of K = the multF of F || the carrier of K & 1. F = 1. K & 0. F = 0. K ) by A16, EC_PF_1:def 1;
hence K = F by A16, A21; :: thesis:

end;

hence F is prime by EC_PF_1:def 2; :: thesis:

end;

end;