theorem :: REALSET2:17

for F being Field holds (0. F) * (1. F) = 0. F ;