let F be Field; :: thesis: for a, b being Element of NonZero F holds
( (omf F) . (a,b) is Element of NonZero F & (revf F) . a is Element of NonZero F )
let a, b be Element of NonZero F; :: thesis: ( (omf F) . (a,b) is Element of NonZero F & (revf F) . a is Element of NonZero F )
[a,b] in [:(NonZero F),(NonZero F):] ;
hence ( (omf F) . (a,b) is Element of NonZero F & (revf F) . a is Element of NonZero F ) by REALSET1:def 4; :: thesis: verum