:: deftheorem defines @ FIELD_7:def 4 :
for R being Ring
for S being RingExtension of R
for a being Element of R holds @ (a,S) = a;