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