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

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