theorem Th27: :: REALSET3:27

for F being Field
for a being Element of F holds (ovf F) . (a,(1. F)) = a