let F be Field; 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; (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; verum