:: deftheorem defines - ZMODLAT1:def 15 :
for V, W being non empty ModuleStr over INT.Ring
for f, g being FrForm of V,W holds f - g = f + (- g);