for R, S2 being Ring
for S1 being RingExtension of R
for h being Function of S1,S2 holds
( h is R -fixing iff h | R = id R )