let F be Field; :: thesis: for a being Element of NonZero F holds
( (omf F) . a,((ovf F) . (1. F),a) = 1. F & (omf F) . ((ovf F) . (1. F),a),a = 1. F )
let a be Element of NonZero F; :: thesis: ( (omf F) . a,((ovf F) . (1. F),a) = 1. F & (omf F) . ((ovf F) . (1. F),a),a = 1. F )
thus A1: (omf F) . a,((ovf F) . (1. F),a) = (ovf F) . (a * (1. F)),a by Th31
.= (ovf F) . a,a by REALSET2:25
.= 1. F by Th29 ; :: thesis: (omf F) . ((ovf F) . (1. F),a),a = 1. F
thus (omf F) . ((ovf F) . (1. F),a),a = ((ovf F) . (1. F),a) * a
.= a * ((ovf F) . (1. F),a)
.= 1. F by A1 ; :: thesis: verum