:: deftheorem defines tohilbval HILBERT4:def 7 :
for v being Function holds v tohilbval = { [n,(dom ((v . n) tohilb))] where n is Element of NAT : verum } ;