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 8; :: thesis: verum