theorem :: REALSET3:12

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