let F be Field; :: thesis: for a being Element of F holds (ovf F) . (a,(1. F)) = a
let a be Element of F; :: thesis: (ovf F) . (a,(1. F)) = a
1. F is Element of NonZero F by STRUCT_0:2;
hence (ovf F) . (a,(1. F)) = (omf F) . (a,((revf F) . (1. F))) by Def2
.= a * (1. F) by Th1
.= a by REALSET2:21 ;
:: thesis: verum