let F be Field; :: thesis: for a, b being Element of NonZero F holds (ovf F) . (a,b) = (revf F) . ((ovf F) . (b,a))
let a, b be Element of NonZero F; :: thesis: (ovf F) . (a,b) = (revf F) . ((ovf F) . (b,a))
(ovf F) . (a,b) = (omf F) . (a,((revf F) . b)) by Def2
.= (revf F) . ((omf F) . (b,((revf F) . a))) by Th2 ;
hence (ovf F) . (a,b) = (revf F) . ((ovf F) . (b,a)) by Def2; :: thesis: verum