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 Th4 ;
hence (ovf F) . a,b = (revf F) . ((ovf F) . b,a) by Def2; :: thesis: verum