:: deftheorem defines 0FrFunctional ZMODLAT1:def 21 :
for V being ModuleStr over INT.Ring holds 0FrFunctional V = ([#] V) --> (0. F_Real);