theorem Th20: :: REALSET3:20

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