theorem Th9: :: REALSET3:9

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