let F be Field; :: thesis: for a being Element of the carrier of F \ {(0. F)} holds (ovf F) . (1. F),a = (revf F) . a
let a be Element of the carrier of F \ {(0. F)}; :: thesis: (ovf F) . (1. F),a = (revf F) . a
reconsider revfa = (revf F) . a as Element of the carrier of F \ {(0. F)} ;
thus (ovf F) . (1. F),a = (omf F) . (1. F),((revf F) . a) by Def2
.= (1. F) * revfa
.= (revf F) . a by REALSET2:10 ; :: thesis: verum