theorem Th5: :: PRVECT_1:5

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