theorem :: REALSET3:22

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