theorem :: REALSET2:16

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