let F be Field; :: thesis: for x, y being Element of NonZero F st x * y = 1. F holds
y = (revf F) . x
let x, y be Element of NonZero F; :: thesis: ( x * y = 1. F implies y = (revf F) . x )
assume A1: x * y = 1. F ; :: thesis: y = (revf F) . x
reconsider rx = (revf F) . x as Element of F by XBOOLE_0:def 5;
y = y * (1. F)
.= (omf F) . (y,(1. F))
.= y * (x * rx) by Def6
.= (1. F) * rx by A1, Th4
.= (revf F) . x ;
hence y = (revf F) . x ; :: thesis: verum