let R1, R2, S2 be Ring; :: thesis: for S1 being RingExtension of R1
for h1 being Function of R1,R2
for h2 being Function of S1,S2 holds
( h2 is h1 -extending iff h2 | R1 = h1 )
let S1 be RingExtension of R1; :: thesis: for h1 being Function of R1,R2
for h2 being Function of S1,S2 holds
( h2 is h1 -extending iff h2 | R1 = h1 )
let h1 be Function of R1,R2; :: thesis: for h2 being Function of S1,S2 holds
( h2 is h1 -extending iff h2 | R1 = h1 )
let h2 be Function of S1,S2; :: thesis: ( h2 is h1 -extending iff h2 | R1 = h1 )
H: R1 is Subring of S1 by FIELD_4:def 1;
now :: thesis: ( h2 is h1 -extending implies h2 | R1 = h1 )
assume AS: h2 is h1 -extending ; :: thesis: h2 | R1 = h1
A0: ( dom h2 = the carrier of S1 & dom h1 = the carrier of R1 ) by FUNCT_2:def 1;
the carrier of R1 c= the carrier of S1 by H, C0SP1:def 3;
then A1: dom h1 = (dom h2) /\ the carrier of R1 by A0, XBOOLE_1:28;
for x being object st x in dom h1 holds
h2 . x = h1 . x by AS;
hence h2 | R1 = h1 by A1, FUNCT_1:46; :: thesis: verum
end;
hence ( h2 is h1 -extending iff h2 | R1 = h1 ) by FUNCT_1:49; :: thesis: verum