theorem Th15: :: REALSET3:15

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