for F being Field holds 0. F is_a_unity_wrt the addF of F