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