now :: thesis: not Char F = 0

assume Char F = 0 ; :: thesis: contradiction
then F is 0 -characteristic by RING_3:def 6;
hence contradiction ; :: thesis: verum

end;

hence Char F is prime by RING_3:86; :: thesis: verum