theorem :: REALSET3:18

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