theorem :: REALSET2:10

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