:: deftheorem defines FieldCover HILBERT4:def 2 :
for f being Function holds FieldCover f = { {x,(f . x)} where x is Element of dom f : x in dom f } ;