let F be Field; :: thesis: for a being Element of the carrier of F holds (ovf F) . a,(1. F) = a
let a be Element of the carrier 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 Th2
.= a by REALSET2:25 ;
:: thesis: verum