theorem :: REALSET2:2

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