theorem :: REALSET3:14

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