theorem :: FIELD_16:23

for R being 0 -characteristic Ring holds Frob R = the carrier of R --> (1. R)