theorem :: REALSET2:18

for F being Field
for a, b being Element of the carrier of F holds (omf F) . (a,b) is Element of the carrier of F ;