theorem :: REALSET2:14

for F being Field
for a being Element of F holds (0. F) * a = 0. F ;