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) by Th10
.= (omf F) . (x,(1. F))
.= x * (rx * rrx) by Def18
.= (x * rx) * rrx by Th8
.= (omf F) . ((1. F),((revf F) . ((revf F) . x))) by Def18
.= (1. F) * rrx
.= (revf F) . ((revf F) . x) by Th10 ;
hence x = (revf F) . ((revf F) . x) ; :: thesis: verum