theorem :: HAHNBAN1:14

for K being non empty ZeroStr
for V being non empty ModuleStr over K
for x being Element of V holds (0Functional V) . x = 0. K by FUNCOP_1:7;