theorem :: REALSET3:26

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