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;

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

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;

hence r " is additive ; :: thesis: ( r " is multiplicative & r " is unity-preserving & r " is one-to-one & r " is onto )

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

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;

hence r " is multiplicative ; :: thesis: ( r " is unity-preserving & r " is one-to-one & r " is onto )
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