theorem :: PRVECT_1:4

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