:: deftheorem defines 0RFunctional HAHNBAN1:def 16 :
for K being 1-sorted
for V being ModuleStr over K holds 0RFunctional V = ([#] V) --> 0;