:: deftheorem Def1 defines osf REALSET3:def 1 :
for F being Field
for b₂ being BinOp of the carrier of F holds
( b₂ = osf F iff for x, y being Element of F holds b₂ . (x,y) = the addF of F . (x,((comp F) . y)) );