let F be Field; :: thesis: (revf F) . (1. F) = 1. F
A1: 1. F is Element of NonZero F by STRUCT_0:2;
then (1. F) * (1. F) = 1. F by REALSET2:6;
hence (revf F) . (1. F) = 1. F by A1, REALSET2:22; :: thesis: verum