theorem e1: :: FIELD_8:40

for R1, R2, S2 being Ring
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 )