H: S is Subring of T by FIELD_4:def 1;
then rng (id S) c= the carrier of T by C0SP1:def 3;
then reconsider h = id S as Function of the carrier of S, the carrier of T by FUNCT_2:6;
( h is additive & h is multiplicative & h is unity-preserving )

proof

now :: thesis: for a, b being Element of S holds h . (a + b) = (h . a) + (h . b)

let a, b be Element of S; :: thesis: h . (a + b) = (h . a) + (h . b)
I: [a,b] in [: the carrier of S, the carrier of S:] ;
thus h . (a + b) = ( the addF of T || the carrier of S) . (a,b) by H, C0SP1:def 3
.= (h . a) + (h . b) by I, FUNCT_1:49 ; :: thesis: verum

end;

hence h is additive ; :: thesis: ( h is multiplicative & h is unity-preserving )

now :: thesis: for a, b being Element of S holds h . (a * b) = (h . a) * (h . b)

let a, b be Element of S; :: thesis: h . (a * b) = (h . a) * (h . b)
I: [a,b] in [: the carrier of S, the carrier of S:] ;
thus h . (a * b) = ( the multF of T || the carrier of S) . (a,b) by H, C0SP1:def 3
.= (h . a) * (h . b) by I, FUNCT_1:49 ; :: thesis: verum

end;

hence h is multiplicative ; :: thesis: h is unity-preserving
thus h is unity-preserving by H, C0SP1:def 3; :: thesis: verum

end;

then reconsider h = h as Homomorphism of S,T ;

now :: thesis: for a being Element of R holds h . a = a

let a be Element of R; :: thesis: h . a = a
R is Subring of S by FIELD_4:def 1;
then the carrier of R c= the carrier of S by C0SP1:def 3;
hence h . a = a by FUNCT_1:18; :: thesis: verum

end;

then h is R -fixing by FIELD_8:def 2;
hence ex b₁ being Homomorphism of S,T st b₁ is R -fixing ; :: thesis: verum