let R, S2 be Ring; :: thesis: for S1 being RingExtension of R
for h being Function of S1,S2 holds
( h is R -fixing iff h | R = id R )
let S1 be RingExtension of R; :: thesis: for h being Function of S1,S2 holds
( h is R -fixing iff h | R = id R )
let h be Function of S1,S2; :: thesis: ( h is R -fixing iff h | R = id R )
H: R is Subring of S1 by FIELD_4:def 1;
A: now :: thesis: ( h is R -fixing implies h | R = id R )
assume AS: h is R -fixing ; :: thesis: h | R = id R
A0: dom h = the carrier of S1 by FUNCT_2:def 1;
the carrier of R c= the carrier of S1 by H, C0SP1:def 3;
then A1: dom (id R) = (dom h) /\ the carrier of R by A0, XBOOLE_1:28;
now :: thesis: for x being object st x in dom (id R) holds
(id R) . x = h . x
let x be object ; :: thesis: ( x in dom (id R) implies (id R) . x = h . x )
assume x in dom (id R) ; :: thesis: (id R) . x = h . x
then reconsider a = x as Element of R ;
h . a = a by AS;
hence (id R) . x = h . x ; :: thesis: verum
end;
hence h | R = id R by A1, FUNCT_1:46; :: thesis: verum
end;
now :: thesis: ( h | R = id R implies h is R -fixing )
assume AS: h | R = id R ; :: 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
thus h . a = (h | the carrier of R) . a by FUNCT_1:49
.= a by AS ; :: thesis: verum
end;
hence h is R -fixing ; :: thesis: verum
end;
hence ( h is R -fixing iff h | R = id R ) by A; :: thesis: verum