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 6 ; :: thesis: verum