theorem :: REALSET3:10

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