for F being Field
for x, y being Element of NonZero F st x * y = 1. F holds
y = (revf F) . x