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 Th21
.= (ovf F) . (a,a) by REALSET2:21
.= 1. F by Th20 ; :: 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