let F be Field; :: thesis: for x being Element of the carrier of F \ {(0. F)} holds (ovf F) . x,x = 1. F
let x be Element of the carrier of F \ {(0. 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