theorem :: REALSET2:23

for F being Field
for x being Element of NonZero F holds x = (revf F) . ((revf F) . x)