theorem Th1: :: REALSET3:1

for F being Field holds (revf F) . (1. F) = 1. F