let F be Field; :: thesis: for x being Element of NonZero F holds (ovf F) . x,x = 1. F
let x be Element of NonZero F; :: thesis: (ovf F) . x,x = 1. F
thus (ovf F) . x,x = (omf F) . x,((revf F) . x) by Def2
.= 1. F by REALSET2:def 18 ; :: thesis: verum