theorem :: REALSET2:13

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