:: deftheorem defines NulFrForm ZMODLAT1:def 10 :
for V, W being ModuleStr over INT.Ring holds NulFrForm (V,W) = [: the carrier of V, the carrier of W:] --> (0. F_Real);