H: ( dom f = the carrier of R & rng f = the carrier of R ) by FUNCT_2:def 1, FUNCT_2:def 3;

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

let a, b be Element of R; :: thesis: (f ") . (a + b) = ((f ") . a) + ((f ") . b)
f . (((f ") . a) + ((f ") . b)) = (f . ((f ") . a)) + (f . ((f ") . b)) by VECTSP_1:def 20
.= a + (f . ((f ") . b)) by H, FUNCT_1:35
.= a + b by H, FUNCT_1:35 ;
hence (f ") . (a + b) = ((f ") . a) + ((f ") . b) by H, FUNCT_1:34; :: thesis: verum

end;

then A: f " is additive ;

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

let a, b be Element of R; :: thesis: (f ") . (a * b) = ((f ") . a) * ((f ") . b)
f . (((f ") . a) * ((f ") . b)) = (f . ((f ") . a)) * (f . ((f ") . b)) by GROUP_6:def 6
.= a * (f . ((f ") . b)) by H, FUNCT_1:35
.= a * b by H, FUNCT_1:35 ;
hence (f ") . (a * b) = ((f ") . a) * ((f ") . b) by H, FUNCT_1:34; :: thesis: verum

end;

then B: f " is multiplicative ;
f . (1_ R) = 1_ R by GROUP_1:def 13;
then f " is unity-preserving by H, FUNCT_1:34;
hence for b₁ being Function of R,R st b₁ = f " holds
b₁ is RingIsomorphism by A, B; :: thesis: verum