for F being Field holds 1_ F is_a_unity_wrt the multF of F