reconsider h = id S as Monomorphism of S ;

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 Monomorphism of S st b₁ is R -fixing ; :: thesis: verum