:: deftheorem defines 0Functional HAHNBAN1:def 7 :
for K being non empty ZeroStr
for V being ModuleStr over K holds 0Functional V = ([#] V) --> (0. K);