take F_Real ; :: thesis: F_Real is well-unital
thus F_Real is well-unital ; :: thesis: verum