F_Real is Subring of F_Complex by Th47, Lm1;
hence F_Real is 0 -characteristic ; :: thesis: verum