theorem thiso: :: FIELD_5:28

for F being Field
for Z being set
for r being Renaming of the carrier of F,Z holds
( r " is additive & r " is multiplicative & r " is unity-preserving & r " is one-to-one & r " is onto )