reconsider h = id S as Automorphism of S ;
take h ; :: thesis: h is R -fixing
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;
then reconsider a1 = a as Element of S ;
h . a1 = a1 ;
hence h . a = a ; :: thesis: verum
end;
hence h is R -fixing ; :: thesis: verum