theorem :: ZMODLAT1:48

for V being non empty ModuleStr over INT.Ring
for x being Element of V holds (0FrFunctional V) . x = 0. F_Real by FUNCOP_1:7;