let F be Field; :: thesis: 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 )

let Z be set ; :: thesis: 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 )

let r be Renaming of the carrier of F,Z; :: thesis: ( r " is additive & r " is multiplicative & r " is unity-preserving & r " is one-to-one & r " is onto )

set K = RenField r;

H0: dom r = the carrier of F by defr;

r . (1. F) = 1. (RenField r) by defrf;

hence r " is unity-preserving by H0, FUNCT_1:34; :: thesis: ( r " is one-to-one & r " is onto )

thus r " is one-to-one ; :: thesis: r " is onto

thus r " is onto by lemonto; :: thesis: verum

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 )

let Z be set ; :: thesis: 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 )

let r be Renaming of the carrier of F,Z; :: thesis: ( r " is additive & r " is multiplicative & r " is unity-preserving & r " is one-to-one & r " is onto )

set K = RenField r;

H0: dom r = the carrier of F by defr;

now :: thesis: for a, b being Element of (RenField r) holds (r ") . (a + b) = ((r ") . a) + ((r ") . b)

hence
r " is additive
; :: thesis: ( r " is multiplicative & r " is unity-preserving & r " is one-to-one & r " is onto )let a, b be Element of (RenField r); :: thesis: (r ") . (a + b) = ((r ") . a) + ((r ") . b)

reconsider a1 = a, b1 = b as Element of rng r by defrf;

thus (r ") . (a + b) = (r ") . ((ren_add r) . (a1,b1)) by defrf

.= (r ") . (r . (((r ") . a) + ((r ") . b))) by defra

.= ((r ") . a) + ((r ") . b) by H0, FUNCT_1:34 ; :: thesis: verum

end;reconsider a1 = a, b1 = b as Element of rng r by defrf;

thus (r ") . (a + b) = (r ") . ((ren_add r) . (a1,b1)) by defrf

.= (r ") . (r . (((r ") . a) + ((r ") . b))) by defra

.= ((r ") . a) + ((r ") . b) by H0, FUNCT_1:34 ; :: thesis: verum

now :: thesis: for a, b being Element of (RenField r) holds (r ") . (a * b) = ((r ") . a) * ((r ") . b)

hence
r " is multiplicative
; :: thesis: ( r " is unity-preserving & r " is one-to-one & r " is onto )let a, b be Element of (RenField r); :: thesis: (r ") . (a * b) = ((r ") . a) * ((r ") . b)

reconsider a1 = a, b1 = b as Element of rng r by defrf;

thus (r ") . (a * b) = (r ") . ((ren_mult r) . (a1,b1)) by defrf

.= (r ") . (r . (((r ") . a) * ((r ") . b))) by defrm

.= ((r ") . a) * ((r ") . b) by H0, FUNCT_1:34 ; :: thesis: verum

end;reconsider a1 = a, b1 = b as Element of rng r by defrf;

thus (r ") . (a * b) = (r ") . ((ren_mult r) . (a1,b1)) by defrf

.= (r ") . (r . (((r ") . a) * ((r ") . b))) by defrm

.= ((r ") . a) * ((r ") . b) by H0, FUNCT_1:34 ; :: thesis: verum

r . (1. F) = 1. (RenField r) by defrf;

hence r " is unity-preserving by H0, FUNCT_1:34; :: thesis: ( r " is one-to-one & r " is onto )

thus r " is one-to-one ; :: thesis: r " is onto

thus r " is onto by lemonto; :: thesis: verum