:: deftheorem defines -extending FIELD_8:def 6 :
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 for a being Element of R1 holds h2 . a = h1 . a );