:: deftheorem defines - ZMODLAT1:def 14 :
for V, W being non empty ModuleStr over INT.Ring
for f being FrForm of V,W holds - f = (- (1. F_Real)) * f;