let F be Field; :: thesis: for a being Element of NonZero F holds (ovf F) . ((1. F),a) = (revf F) . a
let a be Element of NonZero F; :: thesis: (ovf F) . ((1. F),a) = (revf F) . a
reconsider revfa = (revf F) . a as Element of NonZero F ;
thus (ovf F) . ((1. F),a) = (omf F) . ((1. F),((revf F) . a)) by Def2
.= (1. F) * revfa
.= (revf F) . a by REALSET2:6 ; :: thesis: verum