:: deftheorem defred defines @ REALALG3:def 4 :
for E being Field
for F being Subfield of E
for a being Element of E st a is F -membered holds
@ (F,a) = a;