theorem :: REALSET3:11

for F being Field
for a, b being Element of F holds (osf F) . (a,b) = (comp F) . ((osf F) . (b,a))